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 (ProgramPart (Comput (ProgramPart s1),s1,k)),(Comput (ProgramPart s1),s1,k) = Result (ProgramPart s1),s1
let k be Element of NAT ; :: thesis: ( ProgramPart s1 halts_on Comput (ProgramPart s1),s1,k implies Result (ProgramPart (Comput (ProgramPart s1),s1,k)),(Comput (ProgramPart s1),s1,k) = Result (ProgramPart s1),s1 )
set s2 = Comput (ProgramPart s1),s1,k;
assume A2: ProgramPart s1 halts_on Comput (ProgramPart s1),s1,k ; :: thesis: Result (ProgramPart (Comput (ProgramPart s1),s1,k)),(Comput (ProgramPart s1),s1,k) = Result (ProgramPart s1),s1
then ProgramPart (Comput (ProgramPart s1),s1,k) halts_on Comput (ProgramPart s1),s1,k by AMI_1:123;
then consider l being Element of NAT such that
A4: ( Result (ProgramPart (Comput (ProgramPart s1),s1,k)),(Comput (ProgramPart s1),s1,k) = Comput (ProgramPart (Comput (ProgramPart s1),s1,k)),(Comput (ProgramPart s1),s1,k),l & CurInstr (ProgramPart (Comput (ProgramPart s1),s1,k)),(Result (ProgramPart (Comput (ProgramPart s1),s1,k)),(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:123;
Comput (ProgramPart s1),(Comput (ProgramPart s1),s1,k),l = Comput (ProgramPart s1),s1,(k + l) by AMI_1:51;
hence Result (ProgramPart (Comput (ProgramPart s1),s1,k)),(Comput (ProgramPart s1),s1,k) = Result (ProgramPart s1),s1 by A3, A4, T, AMI_1:def 22; :: thesis: verum