let s1, s2 be State of SCM ; :: thesis: for k being Element of NAT st s2 = Computation s1,k & s2 is halting holds
Result s2 = Result s1
let k be Element of NAT ; :: thesis: ( s2 = Computation s1,k & s2 is halting implies Result s2 = Result s1 )
assume that
A1: s2 = Computation s1,k and
A2: s2 is halting ; :: thesis: Result s2 = Result s1
A3: s1 is halting by A1, A2, AMI_1:93;
consider l being Element of NAT such that
A4: ( Result s2 = Computation s2,l & CurInstr (Result s2) = halt SCM ) by A2, AMI_1:def 22;
Computation (Computation s1,k),l = Computation s1,(k + l) by AMI_1:51;
hence Result s2 = Result s1 by A1, A3, A4, AMI_1:def 22; :: thesis: verum