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