Mercurial > hg > Papers > 2020 > soto-midterm
view src/agda-hoare-while.agda @ 1:73127e0ab57c
(none)
author | soto@cr.ie.u-ryukyu.ac.jp |
---|---|
date | Tue, 08 Sep 2020 18:38:08 +0900 |
parents | |
children |
line wrap: on
line source
proof1 : HTProof initCond program termCond proof1 = SeqRule {λ e → true} ( PrimRule empty-case ) $ SeqRule {λ e → Equal (varn e) 10} ( PrimRule lemma1 ) $ WeakeningRule {λ e → (Equal (varn e) 10) ∧ (Equal (vari e) 0)} lemma2 ( WhileRule {_} {λ e → Equal ((varn e) + (vari e)) 10} $ SeqRule (PrimRule {λ e → whileInv e ∧ lt zero (varn e) } lemma3 ) $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5