# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1572683686 -32400
# Node ID 821d04c0770bf4203365105430cf1e7ad6947690
# Parent  7bacba8162776038fa3db748342ee315a7a9a08f
...

diff -r 7bacba816277 -r 821d04c0770b hoareRedBlackTree.agda
--- a/hoareRedBlackTree.agda	Sat Nov 02 16:37:27 2019 +0900
+++ b/hoareRedBlackTree.agda	Sat Nov 02 17:34:46 2019 +0900
@@ -12,6 +12,7 @@
 
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality
+open import logic
 
 
 record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
@@ -114,15 +115,17 @@
      ;  nodeStack = emptySingleLinkedStack
    }
 
-popAllnode : {n m  : Level } {a : Set n} → RedBlackTree {n} {m}  a  → Maybe (Node a)
-popAllnode {n} {m} {a} tree = popAllNode1 (nodeStack tree) where
-    popAllNode1 : SingleLinkedStack (Node a ) →  Maybe (Node a)
-    popAllNode1 [] = nothing
-    popAllNode1 (x ∷ t) = just {!!}
+popAllNode1 : {n : Level } {a : Set n} → SingleLinkedStack (Node a ) → Node a →  Maybe (Node a)
+popAllNode1 [] r = nothing
+popAllNode1 (x ∷ t) r with popAllNode1 t r
+... | ttt = {!!}
 
-record findNodeInvariant {n m  : Level } {a : Set n} {t : Set m} (ordinal now :  RedBlackTree {n} {m}  a ) : Set (m Level.⊔ n) where
+popAllnode : {n m  : Level } {a : Set n} → RedBlackTree {n} {m}  a  → RedBlackTree {n} {m}  a → Set
+popAllnode {n} {m} {a} now original = {!!}
+
+record findNodeInvariant {n m  : Level } {a : Set n} {t : Set m} (now original :  RedBlackTree {n} {m}  a ) : Set (m Level.⊔ n) where
    field
-     tree+stack : popAllnode now ≡ root ordinal
+     tree+stack : popAllnode now original
 
 
 
diff -r 7bacba816277 -r 821d04c0770b logic.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/logic.agda	Sat Nov 02 17:34:46 2019 +0900
@@ -0,0 +1,69 @@
+module logic where
+
+open import Level
+open import Relation.Nullary
+open import Relation.Binary
+open import Data.Empty
+
+
+data Bool : Set where
+    true : Bool
+    false : Bool
+
+record  _∧_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
+   field
+      proj1 : A
+      proj2 : B
+
+data  _∨_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
+   case1 : A → A ∨ B
+   case2 : B → A ∨ B
+
+_⇔_ : {n m : Level } → ( A : Set n ) ( B : Set m )  → Set (n ⊔ m)
+_⇔_ A B =  ( A → B ) ∧ ( B → A )
+
+contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A
+contra-position {n} {m} {A} {B}  f ¬b a = ¬b ( f a )
+
+double-neg : {n  : Level } {A : Set n} → A → ¬ ¬ A
+double-neg A notnot = notnot A
+
+double-neg2 : {n  : Level } {A : Set n} → ¬ ¬ ¬ A → ¬ A
+double-neg2 notnot A = notnot ( double-neg A )
+
+de-morgan : {n  : Level } {A B : Set n} →  A ∧ B  → ¬ ( (¬ A ) ∨ (¬ B ) )
+de-morgan {n} {A} {B} and (case1 ¬A) = ⊥-elim ( ¬A ( _∧_.proj1 and ))
+de-morgan {n} {A} {B} and (case2 ¬B) = ⊥-elim ( ¬B ( _∧_.proj2 and ))
+
+dont-or :　{n m : Level} {A  : Set n} { B : Set m } →  A ∨ B → ¬ A → B
+dont-or {A} {B} (case1 a) ¬A = ⊥-elim ( ¬A a )
+dont-or {A} {B} (case2 b) ¬A = b
+
+dont-orb :　{n m : Level} {A  : Set n} { B : Set m } →  A ∨ B → ¬ B → A
+dont-orb {A} {B} (case2 b) ¬B = ⊥-elim ( ¬B b )
+dont-orb {A} {B} (case1 a) ¬B = a
+
+
+infixr  130 _∧_
+infixr  140 _∨_
+infixr  150 _⇔_
+
+_/\_ : Bool → Bool → Bool 
+true /\ true = true
+_ /\ _ = false
+
+_\/_ : Bool → Bool → Bool 
+false \/ false = false
+_ \/ _ = true
+
+not_ : Bool → Bool 
+not true = false
+not false = true 
+
+_<=>_ : Bool → Bool → Bool  
+true <=> true = true
+false <=> false = true
+_ <=> _ = false
+
+infixr  130 _\/_
+infixr  140 _/\_