Mercurial > hg > Members > ryokka > HoareLogic

changeset 95:4c93248d5ec6

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, 02 Nov 2021 07:30:50 +0900
parents c3b08293a72e
children e152d7afbb58
files whileTestGears.agda
diffstat 1 files changed, 2 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/whileTestGears.agda	Tue Nov 02 07:08:54 2021 +0900
+++ b/whileTestGears.agda	Tue Nov 02 07:30:50 2021 +0900
@@ -151,9 +151,7 @@
     TerminatingLoop1 zero env e1 n≤j eq lt = whileLoopSeg {_} {t} {c10} e1 eq (λ e2 eq lt1 → ⊥-elim (lemma5 n≤j lt1)) exit  
     TerminatingLoop1 (suc j) env e1 n≤j eq lt with <-cmp (varn e1) (suc j)
     ... | tri< a ¬b ¬c = TerminatingLoop1 j env e1 a eq lt 
-    ... | tri≈ ¬a refl ¬c = whileLoopSeg {_} {t} {c10} e1 eq lemma4 exit where
-       lemma4 : (e2 : Env) → varn e2 + vari e2 ≡ c10 → varn e2 < varn e1 → t
-       lemma4 e2 eq lt1 = TerminatingLoop1 j e1 e2 lt1 eq lt1 
+    ... | tri≈ ¬a refl ¬c = whileLoopSeg {_} {t} {c10} e1 eq (λ e2 eq lt1 → TerminatingLoop1 j e1 e2 lt1 eq lt1 ) exit 
     ... | tri> ¬a ¬b c =  ⊥-elim ( nat-≤> c n≤j )   
 
 proofGearsTerm : {c10 :  ℕ } → ⊤
@@ -169,9 +167,7 @@
     TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim (lemma5 n≤j lt1)) 
     TerminatingLoop1 (suc j) r r1  n≤j p1 lt with <-cmp (reduce r1) (suc j)
     ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt 
-    ... | tri≈ ¬a b ¬c = loop r1 p1 lemma4 where
-       lemma4 : (r2 : Index) → Invraiant r2 → reduce r2 < reduce r1  → t
-       lemma4 r2 p2 lt1 = TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1  
+    ... | tri≈ ¬a b ¬c = loop r1 p1 (λ r2 p2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1 )
     ... | tri> ¬a ¬b c =  ⊥-elim ( nat-≤> c n≤j )   
 
 proofGearsTermS : {c10 :  ℕ } → ⊤