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