From 660e4920354ad2f1803ff891762565f72c0ec041 Mon Sep 17 00:00:00 2001
From: minjaesong <alswo9628@gmail.com>
Date: Wed, 22 Nov 2023 17:46:48 +0900
Subject: [PATCH] more on the verum-nimply logic

---
 work_files/verum-nimply_logic.md | 16 ++++++++++++----
 1 file changed, 12 insertions(+), 4 deletions(-)

diff --git a/work_files/verum-nimply_logic.md b/work_files/verum-nimply_logic.md
index b84729e11..b3f27a9d4 100644
--- a/work_files/verum-nimply_logic.md
+++ b/work_files/verum-nimply_logic.md
@@ -31,8 +31,13 @@ This document will use the convention where the Collector is placed on the lefth
 
 ## Derivations
 
-### Diode
-= (p ↛ ⊥)
+### Falsum
+⊥ = (⊤ ↛ ⊤)
+
+### Buffer
+p = (p ↛ ⊥)
+= NOT (NOT p)
+= (⊤ ↛ (⊤ ↛ p))
 
 ### NOT p
 = (⊤ ↛ p)
@@ -43,6 +48,7 @@ This document will use the convention where the Collector is placed on the lefth
 
 ### p NAND q
 = NOT (p AND q)
+= NOT (p ↛ (NOT q))
 = NOT (p ↛ (⊤ ↛ q))
 = (⊤ ↛ (p ↛ (⊤ ↛ q)))
 
@@ -51,9 +57,11 @@ Method 1:
 = NOT (NOT(p) AND NOT(q))
 = NOT ((⊤ ↛ p) AND (⊤ ↛ q))
 = NOT ((⊤ ↛ p) ↛ (⊤ ↛ (⊤ ↛ q)))
-= (⊤ ↛ ((⊤ ↛ p) ↛ (⊤ ↛ (⊤ ↛ q))))
+= NOT ((⊤ ↛ p) ↛ q)
+= (⊤ ↛ ((⊤ ↛ p) ↛ q))
 Method 2:
 = (NOT p) NAND (NOT q)
 = (⊤ ↛ ((NOT p) ↛ (⊤ ↛ (NOT p))))
 = (⊤ ↛ ((⊤ ↛ p) ↛ (⊤ ↛ (⊤ ↛ q))))
-Note: For the most cases, an OR gate can be substituted using merging wires and diodes.
+= (⊤ ↛ ((⊤ ↛ p) ↛ q))
+Note: For the most cases, an OR gate can be substituted using merging wires and buffers.