DISP	nat_evolves_skip_df	nat_evolves_skip(<cmm':cmm':*>)== nat_evolves_skip(<cmm'>)
ABS	nat_evolves_skip	nat_evolves_skip(cmm') == cmm'.2.1 = cmm'.2.2
THM	nat_evolves_skip_wf	cmm': (Atom ) (Atom ). nat_evolves_skip(cmm')
DISP	nat_evolves_seq_df	nat_evolves_seq(<ev:ev:*><cmm':cmm':*><c1:c1:*><c2:c2:*>) == nat_evolves_seq(<ev><cmm'><c1><c2>)
ABS	nat_evolves_seq	nat_evolves_seq(ev;cmm';c1;c2) == m1:Atom . ev <c1, cmm'.2.1, m1> ev <c2, m1, cmm'.2.2>
THM	nat_evolves_seq_wf	ev:( (Atom ) (Atom )) . cmm': (Atom ) (Atom ). c1,c2:. nat_evolves_seq(ev;cmm';c1;c2)
DISP	nat_evolves_assig_df	nat_evolves_assig(<cmm':cmm':*><i:i:*><e:e:*>) == nat_evolves_assig(<cmm'><i><e>)
ABS	nat_evolves_assig	nat_evolves_assig(cmm';i;e) == a:Atom. cmm'.2.2 a = if a=i then [e] else (cmm'.2.1 a)
THM	nat_evolves_assig_wf	cmm': (Atom ) (Atom ). i:Atom. e:Exp. nat_evolves_assig(cmm';i;e)
DISP	nat_evolves_if_df	nat_evolves_if(<ev:ev:*><cmm':cmm':*><b1:b1:*><c3:c3:*><c4:c4:*>) == nat_evolves_if(<ev><cmm'><b1><c3><c4>)
ABS	nat_evolves_if	nat_evolves_if(ev;cmm';b1;c3;c4) == if [b1](cmm'.2.1) then ev <c3, cmm'.2> else ev <c4, cmm'.2> fi
THM	nat_evolves_if_wf	ev:( (Atom ) (Atom )) . cmm': (Atom ) (Atom ). b1:exp. c3,c4:. nat_evolves_if(ev;cmm';b1;c3;c4)
DISP	nat_evolves_while_df	nat_evolves_while(<ev:ev:*><cmm':cmm':*><b2:b2:*><c5:c5:*>) == nat_evolves_while(<ev><cmm'><b2><c5>)
ABS	nat_evolves_while	nat_evolves_while(ev;cmm';b2;c5) == if [b2](cmm'.2.1) then m1:Atom ev <c5, cmm'.2.1, m1> ev <WHILE b2 DO c5 OD, m1, cmm'.2.2> else cmm'.2.1 = cmm'.2.2 fi
THM	nat_evolves_while_wf	ev:( (Atom ) (Atom )) . cmm': (Atom ) (Atom ). b2:exp. c5:. nat_evolves_while(ev;cmm';b2;c5)
DISP	nat_evolves_df	<<c:c:*><m:m:*>> <m':m':*>== <<c><m>> <m'>
ABS	nat_evolves	<c;m> m' == parec(ev,cmm'.case cmm'.1 of SKIP nat_evolves_skip(cmm') c1;c2 nat_evolves_seq(ev;cmm';c1;c2) i := e nat_evolves_assig(cmm';i;e) IF (b1) c3 ELSE c4 nat_evolves_if(ev;cmm';b1;c3; c4) WHILE (b2) c5 nat_evolves_while(ev;cmm';b2;c5) @ <c, m, m'>)
THM	nat_evolves_wf	c:. m,m':Atom . <c;m> m'

the other theories