DISP	conf_df	Conf== Conf
ABS	conf	Conf == (Atom )
ML	conf_soft	add_soft_abs ``conf``;;
ML	compare_conf	let SkipCompareConf n = ApFunToHypEquands `z' if is_skip(z.1) then 1 else 0 fi n THENM Reduce (-1);;
DISP	next_df	<cf:cf:*>== <cf>
ML	next_ml	cf ==r let <c,m> = cf in case c of SKIP <SKIP, m> c1;c2 if is_skip(c1) then <c2, m> else <<c1, m>.1; c2, <c1, m>.2> fi v := e <SKIP, a.if a=v then [e] else (m a)> IF (b) c1 ELSE c2 <if [b](m) then c1 else c2 fi , m> WHILE (b) c <if [b](m) then c; WHILE b DO c OD else SKIP fi , m >
THM	next_wf	cf:Conf. cf Conf
ML	next_eval	let nextC = RecUnfoldC `next` ANDTHENC RedexC ANDTHENC com_casesC ;; add_AbReduce_conv `next` nextC ;;
THM	next_seq_nonskip	c1,c2:. m:Atom . is_skip(c1) <c1; c2, m> = <<c1, m>.1; c2, <c1, m>.2>
DISP	nth_df	<cf:conf:*>[<n:nat:*>]== <cf>[<n>]
ML	nth_ml	cf[n]==r if (n = 0) then cf else cf[n - 1] fi
THM	nth_wf	n:. cf:Conf. cf[n] Conf
THM	nth_zero	cf:Conf. cf[0] = cf
THM	nth_pos	n:{1...}. cf:Conf. cf[n] = cf[n - 1]
THM	nth_plus_one	cf:Conf. n:. cf[n + 1] = cf[n]
THM	next_nth	n:. cf:Conf. cf[n] = cf[n + 1]
THM	nth_skip	m:Atom . n:. <SKIP, m>[n] = <SKIP, m>
THM	nth_ivt_aux	n:. c1,c2:. m,m':Atom . <c1; c2, m>[n] = <SKIP, m'> (k:n m'':Atom <c1; c2, m>[k] = <SKIP; c2, m''> <c1, m>[k] = <SKIP, m''>)
THM	nth_compose	cf:Conf. k,n:. cf[n][k] = cf[n + k]
THM	nth_inv	n,k:. cf:Conf. m,m':Atom . cf[n] = <SKIP, m> cf[n + k] = <SKIP, m'> m = m'
THM	nth_ivt	n:. c1,c2:. m,m':Atom . <c1; c2, m>[n] = <SKIP, m'> (k1,k2:n m'':Atom <c1, m>[k1] = <SKIP, m''> <c2, m''>[k2] = <SKIP, m'>)
DISP	evolves_df	[<c:c:*>](<m:m:*>) <m':m':*>== [<c>](<m>) <m'>
ABS	evolves	[c](m) m' == n:. <c, m>[n] = <SKIP, m'>
THM	evolves_wf	c:. m,m':Atom . [c](m) m'
THM	evolves_skip	m:Atom . [SKIP](m) m
THM	evolves_assig	v:Atom. e:Exp. m:Atom . [v := e](m) a.if a=v then [e] else (m a)
THM	evolves_if_true	b:exp. c1,c2:. m,m':Atom . [b](m) [IF b THEN c1 ELSE c2 ](m) m' [c1](m) m'
THM	evolves_if_false	b:exp. c1,c2:. m,m':Atom . [b](m) [IF b THEN c1 ELSE c2 ](m) m' [c2](m) m'
THM	evolves_ivt	c1,c2:. m1,m2:Atom . [c1; c2](m1) m2 (m':Atom . [c1](m1) m' [c2](m') m2)
THM	evolves_inv	c:. m,m',m'':Atom . [c](m) m' [c](m) m'' m' = m''
THM	evolves_skip_cor	m,m':Atom . [SKIP](m) m' m = m'
THM	evolves_assig_cor	v:Atom. e:Exp. m,m':Atom . [v := e](m) m' m' = (a.if a=v then [e] else (m a))

the other theories