AbeKarplus 22 State Transitions

abekarplus22_state_transitions.md

Rule Matched	Premise State(s)	New State(s)
6	s?=•; x=0; k*=[if e s1 else s2, print]	s?=if e s1 else s2; x=0; k*=[print]
[true]: 2 [false]: 3	s?=if e s1 else s2; x=0; k*=[print] s?=if e s1 else s2; x=0; k*=[print]	s?=•; x=0; k*=[while(e, s+), print] s?=•; x=0; k*=[x=2, x=x, x=x, x=x, print]
[true]: 6 [false]: 6	s?=•; x=0; k*=[while(e, s+), print] s?=•; x=0; k*=[x=2, x=x, x=x, x=x, print]	s?=while(e, s+); x=0; k*=[print] s?="x=2"; x=0; k*=[x=x, x=x, x=x, print]
[true]: 4 [false]: 1	s?=while(e, s+); x=0; k*=[print] s?="x=2"; x=0; k*=[x=x, x=x, x=x, print]	s?=•; x=0; k*=[x+=1, whileK(e, s+), print] s?=•; x=2; k*=[x=x, x=x, x=x, print]
[true]: 6 [false]: 6	s?=•; x=0; k*=[x+=1, whileK(e, s+), print] s?=•; x=2; k*=[x=x, x=x, x=x, print]	s?="x+=1"; x=0; k*=[whileK(e, s+), print] s?="x=x"; x=2; k*=[x=x, x=x, print]
[true]: 1 [false]: 1	s?="x+=1"; x=0; k*=[whileK(e, s+), print] s?="x=x"; x=2; k*=[x=x, x=x, print]	s?=•; x=1; k*=[whileK(e, s+), print] s?=•; x=2; k*=[x=x, x=x, print]
[true]: 7 [false]: 6	s?=•; x=1; k*=[whileK(e, s+), print] s?=•; x=2; k*=[x=x, x=x, print]	s?=•; x=1; k*=[x+=1, whileK(e, s+), print] s?="x=x"; x=2; k*=[x=x, print]
[true]: 6 [false]: 1	s?=•; x=1; k*=[x+=1, whileK(e, s+), print] s?="x=x"; x=2; k*=[x=x, print]	s?="x+=1"; x=1; k*=[whileK(e, s+), print] s?=•; x=2; k*=[x=x, print]
[true]: 1 [false]: 6	s?="x+=1"; x=1; k*=[whileK(e, s+), print] s?=•; x=2; k*=[x=x, print]	s?=•; x=2; k*=[whileK(e, s+), print] s?="x=x"; x=2; k*=[print]
[true]: 8 [false]: 1	s?=•; x=2; k*=[whileK(e, s+), print] s?="x=x"; x=2; k*=[print]	s?=•; x=2; k*=[print] s?=•; x=2; k*=[print]
6	s?=•; x=2; k*=[print]	s?="print"; x=2; k*=[]
execPrint	s?="print"; x=2; k*=[]	s?=•; x=2; k*=[]