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 A1: ( s2 = Computation s1,k & s2 is halting ) ; :: thesis: Result s2 = Result s1
then A2: s1 is halting by AMI_1:93;
consider l being Element of NAT such that
A3: ( Result s2 = Computation s2,l & CurInstr (Result s2) = halt SCM ) by A1, AMI_1:def 22;
Computation (Computation s1,k),l = Computation s1,(k + l) by AMI_1:51;
hence Result s2 = Result s1 by A1, A2, A3, AMI_1:def 22; :: thesis: verum