Mercurial > hg > Papers > 2020 > soto-midterm

annotate src/agda-hoare-while.agda.replaced @ 1:73127e0ab57c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
(none)
author soto@cr.ie.u-ryukyu.ac.jp
date Tue, 08 Sep 2020 18:38:08 +0900
parents
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
1
soto@cr.ie.u-ryukyu.ac.jp
parents:
diff changeset
1 proof1 : HTProof initCond program termCond
soto@cr.ie.u-ryukyu.ac.jp
parents:
diff changeset
2 proof1 =
soto@cr.ie.u-ryukyu.ac.jp
parents:
diff changeset
3 SeqRule {@$\lambda$@ e @$\rightarrow$@ true} ( PrimRule empty-case )
soto@cr.ie.u-ryukyu.ac.jp
parents:
diff changeset
4 $ SeqRule {@$\lambda$@ e @$\rightarrow$@ Equal (varn e) 10} ( PrimRule lemma1 )
soto@cr.ie.u-ryukyu.ac.jp
parents:
diff changeset
5 $ WeakeningRule {@$\lambda$@ e @$\rightarrow$@ (Equal (varn e) 10) @$\wedge$@ (Equal (vari e) 0)} lemma2 (
soto@cr.ie.u-ryukyu.ac.jp
parents:
diff changeset
6 WhileRule {_} {@$\lambda$@ e @$\rightarrow$@ Equal ((varn e) + (vari e)) 10}
soto@cr.ie.u-ryukyu.ac.jp
parents:
diff changeset
7 $ SeqRule (PrimRule {@$\lambda$@ e @$\rightarrow$@ whileInv e @$\wedge$@ lt zero (varn e) } lemma3 )
soto@cr.ie.u-ryukyu.ac.jp
parents:
diff changeset
8 $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5