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, AMI_1:52;
hence contradiction by A2, A4; :: thesis: verum

end;