Mercurial > hg > Members > Moririn

comparison hoareBinaryTree.agda @ 707:d0eafb67bf8d

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 Tue, 07 Dec 2021 18:28:06 +0900
parents 2eedafdd95a6
children c588b77bc197
comparison
equal deleted inserted replaced
706:2eedafdd95a6 707:d0eafb67bf8d
531 TerminatingLoop1 (suc j) r r1 n≤j p1 lt with <-cmp (reduce r1) (suc j) 531 TerminatingLoop1 (suc j) r r1 n≤j p1 lt with <-cmp (reduce r1) (suc j)
532 ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt 532 ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt
533 ... | tri≈ ¬a b ¬c = loop r1 p1 (λ r2 p2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1 ) 533 ... | tri≈ ¬a b ¬c = loop r1 p1 (λ r2 p2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1 )
534 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n≤j ) 534 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n≤j )
535 535
536 record LoopTermination {n : Level} {Index : Set n } { reduce : Index → ℕ }
537 (r : Index ) (C : Set n) : Set (Level.suc n) where
538 field
539 rd : (r1 : Index) → reduce r1 < reduce r
540 ci : C -- data continuation
541
542 TerminatingLoopC : {l n : Level} {t : Set l} (Index : Set n ) → {C : Set n } → ( reduce : Index → ℕ)
543 → (r : Index) → (P : LoopTermination r C )
544 → (loop : (r : Index) → LoopTermination {_} {_} {reduce} r C → (next : (r1 : Index) → LoopTermination r1 C → t ) → t) → t
545 TerminatingLoopC {_} {_} {t} Index {C} reduce r P loop with <-cmp 0 (reduce r)
546 ... | tri≈ ¬a b ¬c = loop r P (λ r1 p1 → ⊥-elim (lemma3 b (LoopTermination.rd P r1)))
547 ... | tri< a ¬b ¬c = loop r P (λ r1 p1 → TerminatingLoop1 (reduce r) r r1 (≤-step (LoopTermination.rd P r1)) p1 (LoopTermination.rd P r1)) where
548 TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j → {!!} → reduce r1 < reduce r → t
549 TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 {!!} (λ r2 P1 → ⊥-elim (lemma5 n≤j (LoopTermination.rd P1 r2)))
550 TerminatingLoop1 (suc j) r r1 n≤j p1 lt with <-cmp (reduce r1) (suc j)
551 ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt
552 ... | tri≈ ¬a b ¬c = loop r1 {!!} (λ r2 p2 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b {!!} ) p2 {!!} )
553 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n≤j )
554
536 record ReplCond {n : Level} {A : Set n} (C : ℕ → bt A → List (bt A) → Set n) : Set (Level.suc n) where 555 record ReplCond {n : Level} {A : Set n} (C : ℕ → bt A → List (bt A) → Set n) : Set (Level.suc n) where
537 field 556 field
538 c1 : (key : ℕ) → (repl : bt A) → (stack : List (bt A)) → C key repl stack 557 c1 : (key : ℕ) → (repl : bt A) → (stack : List (bt A)) → C key repl stack
539 558
540 replaceP0 : {n m : Level} {A : Set n} {t : Set m} 559 replaceP0 : {n m : Level} {A : Set n} {t : Set m}