Mercurial > hg > Gears > GearsAgda

comparison hoareBinaryTree1.agda @ 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
comparison
equal deleted inserted replaced
741:c44edea35126 742:0e0a30f942ca
636 record { self = tree ; parent = node k1 v1 t2 tree ; grand = _ ; pg = s2-1s2p refl refl ; rest = _ ; stack=gp = refl } ) 636 record { self = tree ; parent = node k1 v1 t2 tree ; grand = _ ; pg = s2-1s2p refl refl ; rest = _ ; stack=gp = refl } )
637 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 637 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
638 record { self = tree ; parent = node k1 v1 t2 tree ; grand = _ ; pg = s2-1s2p refl refl ; rest = _ ; stack=gp = refl } ) 638 record { self = tree ; parent = node k1 v1 t2 tree ; grand = _ ; pg = s2-1s2p refl refl ; rest = _ ; stack=gp = refl } )
639 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 639 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
640 record { self = tree ; parent = node k1 v1 t2 tree ; grand = _ ; pg = s2-1s2p refl refl ; rest = _ ; stack=gp = refl } ) 640 record { self = tree ; parent = node k1 v1 t2 tree ; grand = _ ; pg = s2-1s2p refl refl ; rest = _ ; stack=gp = refl } )
641 stackToPG {n} {A} {key} tree orig .(tree ∷ node _ _ _ tree ∷ _) (s-right x (s-left x₁ si)) = ? 641 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
642 stackToPG {n} {A} {key} tree orig .(tree ∷ _) (s-left x si) = ? 642 record { self = tree ; parent = node k1 v1 t1 tree ; grand = _ ; pg = s2-1sp2 refl refl ; rest = _ ; stack=gp = refl } )
643 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
644 record { self = tree ; parent = node k1 v1 t1 tree ; grand = _ ; pg = s2-1sp2 refl refl ; rest = _ ; stack=gp = refl } )
645 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
646 record { self = tree ; parent = node k1 v1 t1 tree ; grand = _ ; pg = s2-1sp2 refl refl ; rest = _ ; stack=gp = refl } )
647 stackToPG {n} {A} {key} tree .(node _ _ tree _) .(tree ∷ node _ _ tree _ ∷ []) (s-left {_} {_} {t1} {k1} {v1} x s-nil) = case2 (case1 refl)
648 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
649 record { self = tree ; parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s12p refl refl ; rest = _ ; stack=gp = refl } )
650 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
651 record { self = tree ; parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s12p refl refl ; rest = _ ; stack=gp = refl } )
652 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
653 record { self = tree ; parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s12p refl refl ; rest = _ ; stack=gp = refl } )
654 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
655 record { self = tree ; parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s1p2 refl refl ; rest = _ ; stack=gp = refl } )
656 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
657 record { self = tree ; parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s1p2 refl refl ; rest = _ ; stack=gp = refl } )
658 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
659 record { self = tree ; parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s1p2 refl refl ; rest = _ ; stack=gp = refl } )
643 660
644 661
645 rbsi-len : {n : Level} {A : Set n} {orig parent grand : bt A} 662 rbsi-len : {n : Level} {A : Set n} {orig parent grand : bt A}
646 → ParentGrand orig parent grand → ℕ 663 → ParentGrand orig parent grand → ℕ
647 rbsi-len {n} {A} {s} {p} {g} st = ? 664 rbsi-len {n} {A} {s} {p} {g} st = ?