Mercurial > hg > Gears > GearsAgda

changeset 882:9f62da6d787c

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 Sat, 04 May 2024 21:48:04 +0900
parents 749e59e3c569
children 9ec8c2f6b92d
files hoareBinaryTree1.agda
diffstat 1 files changed, 16 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Sat May 04 15:30:11 2024 +0900
+++ b/hoareBinaryTree1.agda	Sat May 04 21:48:04 2024 +0900
@@ -1312,8 +1312,22 @@
         rr01 = RB-repl→ti< _ _ _ _ _ trb lt2 x₃
         rr03 = proj1 (proj2 rr01)
         rr04 = proj2 (proj2 rr01)
-RB-repl→ti .(node kg ⟪ Black , _ ⟫ _ (node kp ⟪ Red , _ ⟫ _ _)) .(node kn ⟪ Black , _ ⟫ (node kg ⟪ Red , _ ⟫ _ t₂) (node kp ⟪ Red , _ ⟫ leaf _)) key value ti (rbr-rotate-rl t₂ leaf kg kp kn lt1 lt2 trb) = ?
-RB-repl→ti .(node kg ⟪ Black , _ ⟫ _ (node kp ⟪ Red , _ ⟫ _ _)) .(node kn ⟪ Black , _ ⟫ (node kg ⟪ Red , _ ⟫ _ t₂) (node kp ⟪ Red , _ ⟫ (node key₁ value₁ t₃ t₄) _)) key value ti (rbr-rotate-rl t₂ (node key₁ value₁ t₃ t₄) kg kp kn lt1 lt2 trb) = ?
+RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ t₁ leaf)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .leaf leaf) (node kp ⟪ Red , _ ⟫ leaf _)) key value (t-right .kg .kp x x₁ x₂ ti) (rbr-rotate-rl .leaf .leaf kg kp kn lt1 lt2 trb) = t-node _ _ _ ? ? ? ? ? ? ? ?
+RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ t₁ (node key₁ value₁ t₅ t₆))) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .leaf leaf) (node kp ⟪ Red , _ ⟫ leaf _)) key value (t-right .kg .kp x x₁ x₂ ti) (rbr-rotate-rl .leaf .leaf kg kp kn lt1 lt2 trb) = t-node _ _ _ ? ? ? ? ? ? ? ?
+RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ t₁ leaf)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .leaf (node key₁ value₁ t₂ t₃)) (node kp ⟪ Red , _ ⟫ leaf _)) key value (t-right .kg .kp x x₁ x₂ ti) (rbr-rotate-rl .(node key₁ value₁ t₂ t₃) .leaf kg kp kn lt1 lt2 trb) = t-node _ _ _ ? ? ? ? ? ? ? ?
+RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ t₁ (node key₂ value₂ t₅ t₆))) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .leaf (node key₁ value₁ t₂ t₃)) (node kp ⟪ Red , _ ⟫ leaf _)) key value (t-right .kg .kp x x₁ x₂ ti) (rbr-rotate-rl .(node key₁ value₁ t₂ t₃) .leaf kg kp kn lt1 lt2 trb) = t-node _ _ _ ? ? ? ? ? ? ? ?
+RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ t₁ leaf)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .(node key₁ _ _ _) leaf) (node kp ⟪ Red , _ ⟫ leaf _)) key value (t-node key₁ .kg .kp x x₁ x₂ x₃ x₄ x₅ ti ti₁) (rbr-rotate-rl .leaf .leaf kg kp kn lt1 lt2 trb) = ?
+RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ t₁ (node key₂ value₁ t₅ t₆))) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .(node key₁ _ _ _) leaf) (node kp ⟪ Red , _ ⟫ leaf _)) key value (t-node key₁ .kg .kp x x₁ x₂ x₃ x₄ x₅ ti ti₁) (rbr-rotate-rl .leaf .leaf kg kp kn lt1 lt2 trb) = ?
+RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ t₁ leaf)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .(node key₁ _ _ _) (node key₂ value₁ t₂ t₃)) (node kp ⟪ Red , _ ⟫ leaf _)) key value (t-node key₁ .kg .kp x x₁ x₂ x₃ x₄ x₅ ti ti₁) (rbr-rotate-rl .(node key₂ value₁ t₂ t₃) .leaf kg kp kn lt1 lt2 trb) = ?
+RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ t₁ (node key₃ value₂ t₅ t₆))) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .(node key₁ _ _ _) (node key₂ value₁ t₂ t₃)) (node kp ⟪ Red , _ ⟫ leaf _)) key value (t-node key₁ .kg .kp x x₁ x₂ x₃ x₄ x₅ ti ti₁) (rbr-rotate-rl .(node key₂ value₁ t₂ t₃) .leaf kg kp kn lt1 lt2 trb) = ?
+RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ t₁ leaf)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .leaf leaf) (node kp ⟪ Red , _ ⟫ (node key₁ value₁ t₃ t₄) _)) key value (t-right .kg .kp x x₁ x₂ ti) (rbr-rotate-rl .leaf .(node key₁ value₁ t₃ t₄) kg kp kn lt1 lt2 trb) = ?
+RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ t₁ (node key₂ value₂ t₅ t₆))) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .leaf leaf) (node kp ⟪ Red , _ ⟫ (node key₁ value₁ t₃ t₄) _)) key value (t-right .kg .kp x x₁ x₂ ti) (rbr-rotate-rl .leaf .(node key₁ value₁ t₃ t₄) kg kp kn lt1 lt2 trb) = ?
+RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ t₁ leaf)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .leaf (node key₂ value₂ t₂ t₆)) (node kp ⟪ Red , _ ⟫ (node key₁ value₁ t₃ t₄) _)) key value (t-right .kg .kp x x₁ x₂ ti) (rbr-rotate-rl .(node key₂ value₂ t₂ t₆) .(node key₁ value₁ t₃ t₄) kg kp kn lt1 lt2 trb) = ?
+RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ t₁ (node key₃ value₃ t₅ t₇))) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .leaf (node key₂ value₂ t₂ t₆)) (node kp ⟪ Red , _ ⟫ (node key₁ value₁ t₃ t₄) _)) key value (t-right .kg .kp x x₁ x₂ ti) (rbr-rotate-rl .(node key₂ value₂ t₂ t₆) .(node key₁ value₁ t₃ t₄) kg kp kn lt1 lt2 trb) = ?
+RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ t₁ leaf)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .(node key₂ _ _ _) leaf) (node kp ⟪ Red , _ ⟫ (node key₁ value₁ t₃ t₄) _)) key value (t-node key₂ .kg .kp x x₁ x₂ x₃ x₄ x₅ ti ti₁) (rbr-rotate-rl .leaf .(node key₁ value₁ t₃ t₄) kg kp kn lt1 lt2 trb) = ?
+RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ t₁ (node key₃ value₂ t₅ t₆))) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .(node key₂ _ _ _) leaf) (node kp ⟪ Red , _ ⟫ (node key₁ value₁ t₃ t₄) _)) key value (t-node key₂ .kg .kp x x₁ x₂ x₃ x₄ x₅ ti ti₁) (rbr-rotate-rl .leaf .(node key₁ value₁ t₃ t₄) kg kp kn lt1 lt2 trb) = ?
+RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ t₁ leaf)) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .(node key₂ _ _ _) (node key₃ value₂ t₂ t₆)) (node kp ⟪ Red , _ ⟫ (node key₁ value₁ t₃ t₄) _)) key value (t-node key₂ .kg .kp x x₁ x₂ x₃ x₄ x₅ ti ti₁) (rbr-rotate-rl .(node key₃ value₂ t₂ t₆) .(node key₁ value₁ t₃ t₄) kg kp kn lt1 lt2 trb) = ?
+RB-repl→ti (node kg ⟪ Black , vg ⟫ _ (node kp ⟪ Red , vp ⟫ t₁ (node key₄ value₃ t₅ t₇))) (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , _ ⟫ .(node key₂ _ _ _) (node key₃ value₂ t₂ t₆)) (node kp ⟪ Red , _ ⟫ (node key₁ value₁ t₃ t₄) _)) key value (t-node key₂ .kg .kp x x₁ x₂ x₃ x₄ x₅ ti ti₁) (rbr-rotate-rl .(node key₃ value₂ t₂ t₆) .(node key₁ value₁ t₃ t₄) kg kp kn lt1 lt2 trb) = ?
 
 --
 -- if we consider tree invariant, this may be much simpler and faster