Binary file fig/tree-invariant.graffle has changed

--- a/hoareBinaryTree.agda	Wed Nov 03 10:32:56 2021 +0900
+++ b/hoareBinaryTree.agda	Wed Nov 03 15:58:10 2021 +0900
@@ -24,7 +24,6 @@
 iso-intro : {n : Level} {a : Set n} {x y : ℕ} → ¬ (suc x ≤ y) → ¬ (suc y ≤ x) → _iso_ {n} {a} x y
 iso-intro = λ z z₁ → record { proj1 = z ; proj2 = z₁ }
 
-
 --
 --
 --  no children , having left node , having right node , having both
@@ -67,3 +66,25 @@
 
 insertTest1 = insertTree leaf 1 1 (λ x → x )
 
+open import Data.Unit hiding ( _≟_ ;  _≤?_ ; _≤_)
+
+treeInvariant : {n : Level} {A : Set n} → (tree : bt A) → Set
+treeInvariant leaf = ⊤
+treeInvariant (node key value leaf leaf) = ⊤
+treeInvariant (node key value leaf n@(node key₁ value₁ t₁ t₂)) =  (key < key₁) ∧ treeInvariant n 
+treeInvariant (node key value n@(node key₁ value₁ t t₁) leaf) =  treeInvariant n ∧ (key < key₁) 
+treeInvariant (node key value n@(node key₁ value₁ t t₁) m@(node key₂ value₂ t₂ t₃)) = treeInvariant n ∧  (key < key₁) ∧ (key₁ < key₂) ∧ treeInvariant m
+
+treeInvariantTest1  = treeInvariant (node 3 0 leaf (node 1 1 leaf (node 3 5 leaf leaf)))
+
+stackInvariant : {n : Level} {A : Set n} → (stack  : List (bt A)) → Set n
+stackInvariant {_} {A} [] = Lift _ ⊤
+stackInvariant {_} {A} (leaf ∷ stack) = Lift _ ⊤
+stackInvariant {_} {A} (node key value leaf leaf ∷ []) = Lift _ ⊤
+stackInvariant {_} {A} (node key value _ (node _ _ _ _) ∷ []) = Lift _ ⊥
+stackInvariant {_} {A} (node key value (node _ _ _ _) _ ∷ []) = Lift _ ⊥
+stackInvariant {_} {A} (x ∷ node key value leaf leaf ∷ tail ) = Lift _ ⊥
+stackInvariant {_} {A} (x ∷ tail @ (node key value leaf tree ∷ _) ) = (tree ≡ x) ∧ stackInvariant tail
+stackInvariant {_} {A} (x ∷ tail @ (node key value tree leaf ∷ _) ) = (tree ≡ x) ∧ stackInvariant tail
+stackInvariant {_} {A} (x ∷ tail @ (node key value left right ∷ _  )) = ( (left ≡ x) ∧ stackInvariant tail) ∨ ( (right ≡ x) ∧ stackInvariant tail)
+stackInvariant {_} {A} s = Lift _ ⊥