view src/agda-hoare-while.agda.replaced @ 11:a8bc8c6b48bd default tip

fix
author soto@cr.ie.u-ryukyu.ac.jp
date Tue, 15 Sep 2020 07:06:29 +0900 (2020-09-14)
parents 73127e0ab57c
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'} {_} {whileInv}  lemma4 ) lemma5