Mercurial > hg > Members > Moririn

changeset 742:0e0a30f942ca

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, 24 Apr 2023 13:44:44 +0900
parents c44edea35126
children 80f027be2c68
files hoareBinaryTree1.agda
diffstat 1 files changed, 19 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- 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}