Mercurial > hg > Papers > 2021 > soto-prosym

comparison Paper/src/term1.agda.replaced @ 5:339fb67b4375

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
INIT rbt.agda
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Sun, 07 Nov 2021 00:51:16 +0900
parents c59202657321
children
comparison
equal deleted inserted replaced
4:72667e8198e2 5:339fb67b4375
1 stmt2Cond : {c10 :@$\mathbb{N}$@} @$\rightarrow$@ Cond 1 stmt2Cond : {c10 :!$\mathbb{N}$!} !$\rightarrow$! Cond
2 stmt2Cond {c10} env = (Equal (varn env) c10) @$\wedge$@ (Equal (vari env) 0) 2 stmt2Cond {c10} env = (Equal (varn env) c10) !$\wedge$! (Equal (vari env) 0)
3 3
4 lemma1 : {c10 :@$\mathbb{N}$@} @$\rightarrow$@ Axiom (stmt1Cond {c10}) 4 lemma1 : {c10 :!$\mathbb{N}$!} !$\rightarrow$! Axiom (stmt1Cond {c10})
5 (@$\lambda$@ env @$\rightarrow$@ record { varn = varn env ; vari = 0 }) (stmt2Cond {c10}) 5 (!$\lambda$! env !$\rightarrow$! record { varn = varn env ; vari = 0 }) (stmt2Cond {c10})
6 lemma1 {c10} env = impl@$\Rightarrow$@ ( @$\lambda$@ cond @$\rightarrow$@ let open @$\equiv$@-Reasoning in 6 lemma1 {c10} env = impl!$\Rightarrow$! ( !$\lambda$! cond !$\rightarrow$! let open !$\equiv$!-Reasoning in
7 begin 7 begin
8 ? -- ?0 8 ? -- ?0
9 @$\equiv$@@$\langle$@ ? @$\rangle$@ -- ?1 9 !$\equiv$!!$\langle$! ? !$\rangle$! -- ?1
10 ? -- ?2 10 ? -- ?2
11 @$\blacksquare$@ ) 11 !$\blacksquare$! )
12 12
13 -- ?0 : Bool 13 -- ?0 : Bool
14 -- ?1 : stmt2Cond (record { varn = varn env ; vari = 0 }) @$\equiv$@ true 14 -- ?1 : stmt2Cond (record { varn = varn env ; vari = 0 }) !$\equiv$! true
15 -- ?2 : Bool 15 -- ?2 : Bool