# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1682311484 -32400
# Node ID 0e0a30f942ca4f66fdeb7572c70ea82803738d66
# Parent  c44edea35126b1d17c6ead7354c6e1ca612cddda
...

diff -r c44edea35126 -r 0e0a30f942ca hoareBinaryTree1.agda
--- a/hoareBinaryTree1.agda	Sun Apr 23 17:47:27 2023 +0900
+++ b/hoareBinaryTree1.agda	Mon Apr 24 13:44:44 2023 +0900
@@ -638,8 +638,25 @@
     record { self = tree ; 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
     record { self = tree ; 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 ∷ _) (s-right x (s-left x₁ si)) = ?
-stackToPG {n} {A} {key} tree orig .(tree ∷ _) (s-left x si) = ?
+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 { self = tree ; 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
+    record { self = tree ; 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
+    record { self = tree ; 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
+    record { self = tree ; 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
+    record { self = tree ; 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
+    record { self = tree ; 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
+    record { self = tree ; 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
+    record { self = tree ; 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
+    record { self = tree ; parent = node k1 v1 tree t1 ;  grand = _ ; pg =  s2-s1p2 refl refl ; rest = _ ; stack=gp = refl } )
 
 
 rbsi-len :  {n : Level} {A : Set n} {orig parent grand : bt A}