Mercurial > hg > Papers > 2020 > ryokka-master
view paper/src/agda-hoare-while.agda @ 19:046b2b20d6c7 default tip
fix
author | ryokka |
---|---|
date | Mon, 09 Mar 2020 11:25:49 +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