let s be State of SCM+FSA; :: thesis: for P being initial FinPartState of SCM+FSA st P is_pseudo-closed_on s holds
for n being Element of NAT st n < pseudo-LifeSpan (s,P) holds
( IC (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),n)) in dom P & CurInstr ((ProgramPart (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),n))),(Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),n))) <> halt SCM+FSA )
let P be initial FinPartState of SCM+FSA; :: thesis: ( P is_pseudo-closed_on s implies for n being Element of NAT st n < pseudo-LifeSpan (s,P) holds
( IC (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),n)) in dom P & CurInstr ((ProgramPart (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),n))),(Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),n))) <> halt SCM+FSA ) )
set k = pseudo-LifeSpan (s,P);
assume A1: P is_pseudo-closed_on s ; :: thesis: for n being Element of NAT st n < pseudo-LifeSpan (s,P) holds
( IC (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),n)) in dom P & CurInstr ((ProgramPart (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),n))),(Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),n))) <> halt SCM+FSA )
then A2: IC (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),(pseudo-LifeSpan (s,P)))) = card (ProgramPart P) by Def5;

hereby :: thesis: verum

let n be Element of NAT ; :: thesis: ( n < pseudo-LifeSpan (s,P) implies ( IC (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),n)) in dom P & not CurInstr ((ProgramPart (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),n))),(Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),n))) = halt SCM+FSA ) )
assume A3: n < pseudo-LifeSpan (s,P) ; :: thesis: ( IC (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),n)) in dom P & not CurInstr ((ProgramPart (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),n))),(Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),n))) = halt SCM+FSA )
hence IC (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),n)) in dom P by A1, Def5; :: thesis: not CurInstr ((ProgramPart (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),n))),(Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),n))) = halt SCM+FSA
then A4: IC (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),n)) in dom (ProgramPart P) by COMPOS_1:16;
T: ProgramPart (s +* (P +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),n)) by AMI_1:123;
assume CurInstr ((ProgramPart (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),n))),(Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),n))) = halt SCM+FSA ; :: thesis: contradiction
then IC (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),(pseudo-LifeSpan (s,P)))) = IC (Comput ((ProgramPart (s +* (P +* (Start-At (0,SCM+FSA))))),(s +* (P +* (Start-At (0,SCM+FSA)))),n)) by A3, T, EXTPRO_1:6;
hence contradiction by A2, A4; :: thesis: verum

end;