Mercurial > hg > Papers > 2022 > soto-sigos

view Paper/src/agda-hoare-while.agda.replaced @ 14:ba98083f9853 default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
FIX
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Fri, 27 May 2022 12:31:39 +0900
parents 14a0e409d574
children
line wrap: on
line source

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!$\prime$!} {_} {whileInv}  lemma4 ) lemma5