let s be State of SCM+FSA ; :: thesis: ( ProgramPart s halts_on s implies for k being Element of NAT st LifeSpan s <= k holds
CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) = halt SCM+FSA )
assume ProgramPart s halts_on s ; :: thesis: for k being Element of NAT st LifeSpan s <= k holds
CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) = halt SCM+FSA
then A1: CurInstr (ProgramPart (Comput (ProgramPart s),s,(LifeSpan s))),(Comput (ProgramPart s),s,(LifeSpan s)) = halt SCM+FSA by AMI_1:def 46;
let k be Element of NAT ; :: thesis: ( LifeSpan s <= k implies CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) = halt SCM+FSA )
set i = LifeSpan s;
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,(LifeSpan s)) by AMI_1:144;
assume LifeSpan s <= k ; :: thesis: CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) = halt SCM+FSA
then Comput (ProgramPart s),s,k = Comput (ProgramPart s),s,(LifeSpan s) by A1, AMI_1:52, T;
hence CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) = halt SCM+FSA by A1; :: thesis: verum