--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/agda-hoare-while.agda.replaced	Tue Sep 08 18:38:08 2020 +0900
@@ -0,0 +1,8 @@
+proof1 : HTProof initCond program termCond
+proof1 =
+  SeqRule {@$\lambda$@ e @$\rightarrow$@ true} ( PrimRule empty-case )
+    $ SeqRule {@$\lambda$@ e @$\rightarrow$@  Equal (varn e) 10} ( PrimRule lemma1   )
+    $ WeakeningRule {@$\lambda$@ e @$\rightarrow$@ (Equal (varn e) 10) @$\wedge$@ (Equal (vari e) 0)}  lemma2 (
+      WhileRule {_} {@$\lambda$@ e @$\rightarrow$@ Equal ((varn e) + (vari e)) 10}
+        $ SeqRule (PrimRule {@$\lambda$@ e @$\rightarrow$@  whileInv e  @$\wedge$@ lt zero (varn e) } lemma3 )
+        $ PrimRule {whileInv'} {_} {whileInv}  lemma4 ) lemma5