Mercurial > hg > Gears > GearsAgda

changeset 771:feb3553ef88c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 08 May 2023 13:32:42 +0900
parents a4bc901bba36
children a8af918e7fd9
files hoareBinaryTree1.agda
diffstat 1 files changed, 37 insertions(+), 35 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Mon May 08 12:59:13 2023 +0900
+++ b/hoareBinaryTree1.agda	Mon May 08 13:32:42 2023 +0900
@@ -58,9 +58,9 @@
 --
 data stackInvariant {n : Level} {A : Set n}  (key : ℕ) : (top orig : bt A) → (stack  : List (bt A)) → Set n where
     s-nil :  {tree0 : bt A} → stackInvariant key tree0 tree0 (tree0 ∷ [])
-    s-right :  {tree tree0 tree₁ : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)} 
+    s-right :  (tree tree0 tree₁ : bt A) → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)} 
         → key₁ < key  →  stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → stackInvariant key tree tree0 (tree ∷ st)
-    s-left :  {tree₁ tree0 tree : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)} 
+    s-left :  (tree₁ tree0 tree : bt A) → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)} 
         → key  < key₁ →  stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → stackInvariant key tree₁ tree0 (tree₁ ∷ st)
 
 data replacedTree  {n : Level} {A : Set n} (key : ℕ) (value : A)  : (before after : bt A ) → Set n where
@@ -94,25 +94,25 @@
 stack-last (x ∷ s) = stack-last s
 
 stackInvariantTest1 : stackInvariant 4 treeTest2 treeTest1 ( treeTest2 ∷ treeTest1 ∷ [] )
-stackInvariantTest1 = s-right (add< 3) (s-nil  )
+stackInvariantTest1 = s-right _ _ _ (add< 3) (s-nil  )
 
 si-property0 :  {n : Level} {A : Set n} {key : ℕ} {tree tree0 : bt A} → {stack  : List (bt A)} →  stackInvariant key tree tree0 stack → ¬ ( stack ≡ [] )
 si-property0  (s-nil  ) ()
-si-property0  (s-right x si) ()
-si-property0  (s-left x si) ()
+si-property0  (s-right _ _ _ x si) ()
+si-property0  (s-left _ _ _ x si) ()
 
 si-property1 :  {n : Level} {A : Set n} {key : ℕ} {tree tree0 tree1 : bt A} → {stack  : List (bt A)} →  stackInvariant key tree tree0 (tree1 ∷ stack)
    → tree1 ≡ tree
 si-property1 (s-nil   ) = refl
-si-property1 (s-right _  si) = refl
-si-property1 (s-left _  si) = refl
+si-property1 (s-right _ _ _ _  si) = refl
+si-property1 (s-left _ _ _ _  si) = refl
 
 si-property-last :  {n : Level} {A : Set n}  (key : ℕ) (tree tree0 : bt A) → (stack  : List (bt A)) →  stackInvariant key tree tree0 stack
    → stack-last stack ≡ just tree0
 si-property-last key t t0 (t ∷ [])  (s-nil )  = refl
-si-property-last key t t0 (.t ∷ x ∷ st) (s-right _ si ) with  si-property1 si
+si-property-last key t t0 (.t ∷ x ∷ st) (s-right _ _ _ _ si ) with  si-property1 si
 ... | refl = si-property-last key x t0 (x ∷ st)   si
-si-property-last key t t0 (.t ∷ x ∷ st) (s-left _ si ) with  si-property1  si
+si-property-last key t t0 (.t ∷ x ∷ st) (s-left _ _ _ _ si ) with  si-property1  si
 ... | refl = si-property-last key x t0 (x ∷ st)   si
 
 rt-property1 :  {n : Level} {A : Set n} (key : ℕ) (value : A) (tree tree1 : bt A ) → replacedTree key value tree tree1 → ¬ ( tree1 ≡ leaf )
@@ -179,8 +179,8 @@
 findP {n} {_} {A} key (node key₁ v1 tree tree₁) tree0 st  Pre next _ | tri< a ¬b ¬c = next tree (tree ∷ st)
        ⟪ treeLeftDown tree tree₁ (proj1 Pre)  , findP1 a st (proj2 Pre) ⟫ depth-1< where
    findP1 : key < key₁ → (st : List (bt A)) →  stackInvariant key (node key₁ v1 tree tree₁) tree0 st → stackInvariant key tree tree0 (tree ∷ st)
-   findP1 a (x ∷ st) si = s-left a si
-findP key n@(node key₁ v1 tree tree₁) tree0 st Pre next _ | tri> ¬a ¬b c = next tree₁ (tree₁ ∷ st) ⟪ treeRightDown tree tree₁ (proj1 Pre) , s-right c (proj2 Pre) ⟫ depth-2<
+   findP1 a (x ∷ st) si = s-left _ _ _ a si
+findP key n@(node key₁ v1 tree tree₁) tree0 st Pre next _ | tri> ¬a ¬b c = next tree₁ (tree₁ ∷ st) ⟪ treeRightDown tree tree₁ (proj1 Pre) , s-right _ _ _ c (proj2 Pre) ⟫ depth-2<
 
 replaceTree1 : {n  : Level} {A : Set n} {t t₁ : bt A } → ( k : ℕ ) → (v1 value : A ) →  treeInvariant (node k v1 t t₁) → treeInvariant (node k value t t₁)
 replaceTree1 k v1 value (t-single .k .v1) = t-single k value
@@ -268,7 +268,7 @@
 replaceP {n} {_} {A} key value  {tree}  repl (leaf ∷ st@(tree1 ∷ st1)) Pre next exit = next key value repl st Post ≤-refl where
     Post :  replacePR key value tree1 repl (tree1 ∷ st1) (λ _ _ _ → Lift n ⊤)
     Post with replacePR.si Pre 
-    ... | s-right  {_} {_} {tree₁} {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
+    ... | s-right  _ _ tree₁ {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
         repl09 : tree1 ≡ node key₂ v1 tree₁ leaf
         repl09 = si-property1 si
         repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
@@ -281,7 +281,7 @@
         ... |  tri> ¬a ¬b c = refl
         repl12 : replacedTree key value (child-replaced key  tree1  ) repl
         repl12 = subst₂ (λ j k → replacedTree key value j k ) (sym (subst (λ k → child-replaced key k ≡ leaf) (sym repl09) repl07 ) ) (sym (rt-property-leaf (replacePR.ri Pre))) r-leaf
-    ... | s-left  {_} {_} {tree₁} {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
+    ... | s-left  _ _ tree₁ {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
         repl09 : tree1 ≡ node key₂ v1 leaf tree₁ 
         repl09 = si-property1 si
         repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
@@ -298,7 +298,7 @@
 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) st Post ≤-refl where
     Post : replacePR key value tree1 (node key₁ value₁ repl right ) st (λ _ _ _ → Lift n ⊤) 
     Post with replacePR.si Pre 
-    ... | s-right {_} {_} {tree₁} {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
+    ... | s-right _ _ tree₁ {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
         repl09 : tree1 ≡ node key₂ v1 tree₁ (node key₁ value₁ left right) 
         repl09 = si-property1 si
         repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
@@ -322,7 +322,7 @@
             child-replaced key tree1 ∎  where open ≡-Reasoning
         repl12 : replacedTree key value (child-replaced key  tree1  ) (node key₁ value₁ repl right)
         repl12 = subst (λ k → replacedTree key value k (node key₁ value₁ repl right) ) repl04  (r-left a (replacePR.ri Pre)) 
-    ... | s-left {_} {_} {tree₁} {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
+    ... | s-left _ _ tree₁ {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
         repl09 : tree1 ≡ node key₂ v1 (node key₁ value₁ left right) tree₁  
         repl09 = si-property1 si
         repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
@@ -349,7 +349,7 @@
 ... | tri≈ ¬a b ¬c = next key value (node key₁ value  left right ) st Post ≤-refl where 
     Post :  replacePR key value tree1 (node key₁ value left right ) (tree1 ∷ st1) (λ _ _ _ → Lift n ⊤)
     Post with replacePR.si Pre 
-    ... | s-right  {_} {_} {tree₁} {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 b ; ci = lift tt } where
+    ... | s-right  _ _ tree₁ {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 b ; ci = lift tt } where
         repl09 : tree1 ≡ node key₂ v1 tree₁ tree -- (node key₁ value₁  left right)
         repl09 = si-property1 si
         repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
@@ -363,7 +363,7 @@
         repl12 : (key ≡ key₁) → replacedTree key value (child-replaced key  tree1  ) (node key₁ value left right )
         repl12 refl with repl09 
         ... | refl = subst (λ k → replacedTree key value k (node key₁ value left right )) (sym repl07) r-node
-    ... | s-left  {_} {_} {tree₁} {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 b ; ci = lift tt } where
+    ... | s-left  _ _ tree₁ {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 b ; ci = lift tt } where
         repl09 : tree1 ≡ node key₂ v1 tree tree₁ 
         repl09 = si-property1 si
         repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
@@ -380,7 +380,7 @@
 ... | tri> ¬a ¬b c = next key value (node key₁ value₁ left repl ) st Post ≤-refl where
     Post : replacePR key value tree1 (node key₁ value₁ left repl ) st (λ _ _ _ → Lift n ⊤) 
     Post with replacePR.si Pre 
-    ... | s-right {_} {_} {tree₁} {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
+    ... | s-right _ _ tree₁ {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
         repl09 : tree1 ≡ node key₂ v1 tree₁ (node key₁ value₁ left right) 
         repl09 = si-property1 si
         repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
@@ -404,7 +404,7 @@
             child-replaced key tree1 ∎  where open ≡-Reasoning
         repl12 : replacedTree key value (child-replaced key  tree1  ) (node key₁ value₁ left repl)
         repl12 = subst (λ k → replacedTree key value k (node key₁ value₁ left repl) ) repl04 (r-right c (replacePR.ri Pre)) 
-    ... | s-left {_} {_} {tree₁} {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
+    ... | s-left _ _ tree₁ {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
         repl09 : tree1 ≡ node key₂ v1 (node key₁ value₁ left right) tree₁  
         repl09 = si-property1 si
         repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
@@ -613,8 +613,9 @@
 
 record RBI {n : Level} {A : Set n} (key : ℕ) (value : A) (orig : bt (Color ∧ A) ) (stack : List (bt (Color ∧ A)))  : Set n where
    field
-     d rd : ℕ
+     od d rd : ℕ
      tree rot repl : bt (Color ∧ A)
+     origrb : RBtreeInvariant orig od
      treerb : RBtreeInvariant tree d
      replrb : RBtreeInvariant repl rd
      d=rd : ( d ≡ rd ) ∨ ( suc d ≡ rd )
@@ -625,37 +626,38 @@
 rbi-case1 : {n : Level} {A : Set n} → {key : ℕ} → {value : A} → (tree orig : bt (Color ∧ A) )
            →  (stack : List (bt (Color ∧ A))) 
            →  stack ≡ tree ∷ orig ∷ [] → RBI key value orig stack → RBI key value orig (orig ∷ [])
-rbi-case1 {n} {A} {key} {value} tree orig stack eq rbi = ?
+rbi-case1 {n} {A} {key} {value} tree₁ .(node _ _ t1 tree₁) (tree₁ ∷ .(node _ _ t1 tree₁) ∷ []) refl record { od = od ; d = d ; rd = rd ; tree = .tree₁ ; rot = rot ; repl = repl ; origrb = origrb ; treerb = treerb ; replrb = replrb ; d=rd = d=rd ; si = (s-right .tree₁ .(node _ _ t1 tree₁) t1 x s-nil) ; rotated = rotated ; ri = ri } = ?
+rbi-case1 {n} {A} {key} {value} tree₁ orig (tree₁ ∷ orig ∷ []) refl record { od = od ; d = d ; rd = rd ; tree = .tree₁ ; rot = rot ; repl = repl ; origrb = origrb ; treerb = treerb ; replrb = replrb ; d=rd = d=rd ; si = (s-left _ _ _ x si) ; rotated = rotated ; ri = ri } = ?
 
 stackToPG : {n : Level} {A : Set n} → {key : ℕ } → (tree orig : bt A )
            →  (stack : List (bt A)) → stackInvariant key tree orig stack
            → ( stack ≡ orig ∷ [] ) ∨ ( stack ≡ tree ∷ orig ∷ [] ) ∨ PG A tree stack
 stackToPG {n} {A} {key} tree .tree .(tree ∷ []) s-nil = case1 refl
-stackToPG {n} {A} {key} tree .(node _ _ _ tree) .(tree ∷ node _ _ _ tree ∷ []) (s-right x s-nil) = case2 (case1 refl)
-stackToPG {n} {A} {key} tree .(node k2 v2 t5 (node k1 v1 t2 tree)) (tree ∷ node _ _ _ tree ∷ .(node k2 v2 t5 (node k1 v1 t2 tree) ∷ [])) (s-right {.tree} {.(node k2 v2 t5 (node k1 v1 t2 tree))} {t2} {k1} {v1} x (s-right {.(node k1 v1 t2 tree)} {.(node k2 v2 t5 (node k1 v1 t2 tree))} {t5} {k2} {v2} x₁ s-nil)) = case2 (case2 
+stackToPG {n} {A} {key} tree .(node _ _ _ tree) .(tree ∷ node _ _ _ tree ∷ []) (s-right _ _ _ x s-nil) = case2 (case1 refl)
+stackToPG {n} {A} {key} tree .(node k2 v2 t5 (node k1 v1 t2 tree)) (tree ∷ node _ _ _ tree ∷ .(node k2 v2 t5 (node k1 v1 t2 tree) ∷ [])) (s-right tree (node k2 v2 t5 (node k1 v1 t2 tree)) t2 {k1} {v1} x (s-right (node k1 v1 t2 tree) (node k2 v2 t5 (node k1 v1 t2 tree)) t5 {k2} {v2} x₁ s-nil)) = case2 (case2 
     record {  parent = node k1 v1 t2 tree ;  grand = _ ; pg = s2-1s2p  refl refl  ; rest = _ ; stack=gp = refl } )
-stackToPG {n} {A} {key} tree orig (tree ∷ node _ _ _ tree ∷ .(node k2 v2 t5 (node k1 v1 t2 tree) ∷ _)) (s-right {.tree} {.orig} {t2} {k1} {v1} x (s-right {.(node k1 v1 t2 tree)} {.orig} {t5} {k2} {v2} x₁ (s-right x₂ si))) = case2 (case2 
+stackToPG {n} {A} {key} tree orig (tree ∷ node _ _ _ tree ∷ .(node k2 v2 t5 (node k1 v1 t2 tree) ∷ _)) (s-right tree orig t2 {k1} {v1} x (s-right (node k1 v1 t2 tree) orig t5 {k2} {v2} x₁ (s-right _ _ _ x₂ si))) = case2 (case2 
     record {  parent = node k1 v1 t2 tree ;  grand = _ ; pg = s2-1s2p  refl refl  ; rest = _ ; stack=gp = refl } )
-stackToPG {n} {A} {key} tree orig (tree ∷ node _ _ _ tree ∷ .(node k2 v2 t5 (node k1 v1 t2 tree) ∷ _)) (s-right {.tree} {.orig} {t2} {k1} {v1} x (s-right {.(node k1 v1 t2 tree)} {.orig} {t5} {k2} {v2} x₁ (s-left x₂ si))) = case2 (case2
+stackToPG {n} {A} {key} tree orig (tree ∷ node _ _ _ tree ∷ .(node k2 v2 t5 (node k1 v1 t2 tree) ∷ _)) (s-right tree orig t2 {k1} {v1} x (s-right (node k1 v1 t2 tree) orig t5 {k2} {v2} x₁ (s-left _ _ _ x₂ si))) = case2 (case2
     record {  parent = node k1 v1 t2 tree ;  grand = _ ; pg = s2-1s2p  refl refl  ; rest = _ ; stack=gp = refl } )
-stackToPG {n} {A} {key} tree .(node k2 v2 (node k1 v1 t1 tree) t2) .(tree ∷ node k1 v1 t1 tree ∷ node k2 v2 (node k1 v1 t1 tree) t2 ∷ []) (s-right {_} {_} {t1} {k1} {v1} x (s-left {_} {_} {t2} {k2} {v2} x₁ s-nil)) = case2 (case2
+stackToPG {n} {A} {key} tree .(node k2 v2 (node k1 v1 t1 tree) t2) .(tree ∷ node k1 v1 t1 tree ∷ node k2 v2 (node k1 v1 t1 tree) t2 ∷ []) (s-right _ _ t1 {k1} {v1} x (s-left _ _ t2 {k2} {v2} x₁ s-nil)) = case2 (case2
     record {  parent = node k1 v1 t1 tree ;  grand = _ ; pg = s2-1sp2 refl refl ; rest = _ ; stack=gp = refl } )
-stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 t1 tree ∷ node k2 v2 (node k1 v1 t1 tree) t2 ∷ _) (s-right {_} {_} {t1} {k1} {v1} x (s-left {_} {_} {t2} {k2} {v2} x₁ (s-right x₂ si))) = case2 (case2
+stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 t1 tree ∷ node k2 v2 (node k1 v1 t1 tree) t2 ∷ _) (s-right _ _ t1 {k1} {v1} x (s-left _ _ t2 {k2} {v2} x₁ (s-right _ _ _ x₂ si))) = case2 (case2
     record {  parent = node k1 v1 t1 tree ;  grand = _ ; pg = s2-1sp2 refl refl ; rest = _ ; stack=gp = refl } )
-stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 t1 tree ∷ node k2 v2 (node k1 v1 t1 tree) t2 ∷ _) (s-right {_} {_} {t1} {k1} {v1} x (s-left {_} {_} {t2} {k2} {v2} x₁ (s-left x₂ si))) = case2 (case2
+stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 t1 tree ∷ node k2 v2 (node k1 v1 t1 tree) t2 ∷ _) (s-right _ _ t1 {k1} {v1} x (s-left _ _ t2 {k2} {v2} x₁ (s-left _ _ _ x₂ si))) = case2 (case2
     record {  parent = node k1 v1 t1 tree ;  grand = _ ; pg = s2-1sp2 refl refl ; rest = _ ; stack=gp = refl } )
-stackToPG {n} {A} {key} tree .(node _ _ tree _) .(tree ∷ node _ _ tree _ ∷ []) (s-left {_} {_} {t1} {k1} {v1} x s-nil) = case2 (case1 refl)
-stackToPG {n} {A} {key} tree .(node _ _ _ (node k1 v1 tree t1)) .(tree ∷ node k1 v1 tree t1 ∷ node _ _ _ (node k1 v1 tree t1) ∷ []) (s-left {_} {_} {t1} {k1} {v1} x (s-right x₁ s-nil)) = case2 (case2
+stackToPG {n} {A} {key} tree .(node _ _ tree _) .(tree ∷ node _ _ tree _ ∷ []) (s-left _ _ t1 {k1} {v1} x s-nil) = case2 (case1 refl)
+stackToPG {n} {A} {key} tree .(node _ _ _ (node k1 v1 tree t1)) .(tree ∷ node k1 v1 tree t1 ∷ node _ _ _ (node k1 v1 tree t1) ∷ []) (s-left _ _ t1 {k1} {v1} x (s-right _ _ _ x₁ s-nil)) = case2 (case2
     record {  parent = node k1 v1 tree t1 ;  grand = _ ; pg =  s2-s12p refl refl ; rest = _ ; stack=gp = refl } )
-stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ _ (node k1 v1 tree t1) ∷ _) (s-left {_} {_} {t1} {k1} {v1} x (s-right x₁ (s-right x₂ si))) = case2 (case2
+stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ _ (node k1 v1 tree t1) ∷ _) (s-left _ _ t1 {k1} {v1} x (s-right _ _ _ x₁ (s-right _ _ _ x₂ si))) = case2 (case2
     record {  parent = node k1 v1 tree t1 ;  grand = _ ; pg =  s2-s12p refl refl ; rest = _ ; stack=gp = refl } )
-stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ _ (node k1 v1 tree t1) ∷ _) (s-left {_} {_} {t1} {k1} {v1} x (s-right x₁ (s-left x₂ si))) = case2 (case2
+stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ _ (node k1 v1 tree t1) ∷ _) (s-left _ _ t1 {k1} {v1} x (s-right _ _ _ x₁ (s-left _ _ _ x₂ si))) = case2 (case2
     record {  parent = node k1 v1 tree t1 ;  grand = _ ; pg =  s2-s12p refl refl ; rest = _ ; stack=gp = refl } )
-stackToPG {n} {A} {key} tree .(node _ _ (node k1 v1 tree t1) _) .(tree ∷ node k1 v1 tree t1 ∷ node _ _ (node k1 v1 tree t1) _ ∷ []) (s-left {_} {_} {t1} {k1} {v1} x (s-left x₁ s-nil)) = case2 (case2
+stackToPG {n} {A} {key} tree .(node _ _ (node k1 v1 tree t1) _) .(tree ∷ node k1 v1 tree t1 ∷ node _ _ (node k1 v1 tree t1) _ ∷ []) (s-left _ _ t1 {k1} {v1} x (s-left _ _ _ x₁ s-nil)) = case2 (case2
     record {  parent = node k1 v1 tree t1 ;  grand = _ ; pg =  s2-s1p2 refl refl ; rest = _ ; stack=gp = refl } )
-stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ (node k1 v1 tree t1) _ ∷ _) (s-left {_} {_} {t1} {k1} {v1} x (s-left x₁ (s-right x₂ si))) = case2 (case2
+stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ (node k1 v1 tree t1) _ ∷ _) (s-left _ _ t1 {k1} {v1} x (s-left _ _ _ x₁ (s-right _ _ _ x₂ si))) = case2 (case2
     record {  parent = node k1 v1 tree t1 ;  grand = _ ; pg =  s2-s1p2 refl refl ; rest = _ ; stack=gp = refl } )
-stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ (node k1 v1 tree t1) _ ∷ _) (s-left {_} {_} {t1} {k1} {v1} x (s-left x₁ (s-left x₂ si))) = case2 (case2
+stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ (node k1 v1 tree t1) _ ∷ _) (s-left _ _ t1 {k1} {v1} x (s-left _ _ _ x₁ (s-left _ _ _ x₂ si))) = case2 (case2
     record {  parent = node k1 v1 tree t1 ;  grand = _ ; pg =  s2-s1p2 refl refl ; rest = _ ; stack=gp = refl } )
 
 stackCase1 : {n : Level} {A : Set n} → {key : ℕ } → {tree orig : bt A }