set A = NAT ;
set D = Int-Locations \/ FinSeq-Locations ;
let s be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA st Directed I is_pseudo-closed_on s holds
( I ';' (Stop SCM+FSA ) is_closed_on s & I ';' (Stop SCM+FSA ) is_halting_on s & LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = pseudo-LifeSpan s,(Directed I) & ( for n being Element of NAT st n < pseudo-LifeSpan s,(Directed I) holds
IC (Computation (s +* (I +* (Start-At (insloc 0 )))),n) = IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) ) & ( for n being Element of NAT st n <= pseudo-LifeSpan s,(Directed I) holds
DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),n) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) ) )
let I be Program of SCM+FSA ; :: thesis: ( Directed I is_pseudo-closed_on s implies ( I ';' (Stop SCM+FSA ) is_closed_on s & I ';' (Stop SCM+FSA ) is_halting_on s & LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = pseudo-LifeSpan s,(Directed I) & ( for n being Element of NAT st n < pseudo-LifeSpan s,(Directed I) holds
IC (Computation (s +* (I +* (Start-At (insloc 0 )))),n) = IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) ) & ( for n being Element of NAT st n <= pseudo-LifeSpan s,(Directed I) holds
DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),n) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) ) ) )
set I0 = Directed I;
set I1 = I ';' (Stop SCM+FSA );
set s00 = s +* ((Directed I) +* (Start-At (insloc 0 )));
set s10 = s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )));
assume A1: Directed I is_pseudo-closed_on s ; :: thesis: ( I ';' (Stop SCM+FSA ) is_closed_on s & I ';' (Stop SCM+FSA ) is_halting_on s & LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = pseudo-LifeSpan s,(Directed I) & ( for n being Element of NAT st n < pseudo-LifeSpan s,(Directed I) holds
IC (Computation (s +* (I +* (Start-At (insloc 0 )))),n) = IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) ) & ( for n being Element of NAT st n <= pseudo-LifeSpan s,(Directed I) holds
DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),n) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) ) )
reconsider k = pseudo-LifeSpan (s +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I) as Element of NAT ;
A2: Directed I c= I ';' (Stop SCM+FSA ) by SCMFSA6A:55;
then A3: dom (Directed I) c= dom (I ';' (Stop SCM+FSA )) by GRFUNC_1:8;
card (I ';' (Stop SCM+FSA )) = (card I) + 1 by SCMFSA6A:61, SCMFSA8A:17;
then card I < card (I ';' (Stop SCM+FSA )) by NAT_1:13;
then A4: insloc (card I) in dom (I ';' (Stop SCM+FSA )) by SCMFSA6A:15;
A5: card I < (card I) + (card (Stop SCM+FSA )) by NAT_1:13, SCMFSA8A:17;
halt SCM+FSA = (Stop SCM+FSA ) . (insloc ((card I) -' (card I))) by SCMFSA8A:16, XREAL_1:234;
then (I ';' (Stop SCM+FSA )) . (insloc (card I)) = IncAddr (halt SCM+FSA ),(card I) by A5, Th13
.= halt SCM+FSA by SCMFSA_4:8 ;
then A6: (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) . (insloc (card I)) = halt SCM+FSA by A4, Th26;
A7: (Directed I) +* (Start-At (insloc 0 )) c= s +* ((Directed I) +* (Start-At (insloc 0 ))) by FUNCT_4:26;
A8: (s +* ((Directed I) +* (Start-At (insloc 0 )))) +* ((Directed I) +* (Start-At (insloc 0 ))) = s +* (((Directed I) +* (Start-At (insloc 0 ))) +* ((Directed I) +* (Start-At (insloc 0 )))) by FUNCT_4:15
.= s +* ((Directed I) +* (Start-At (insloc 0 ))) ;
A9: Directed I is_pseudo-closed_on s +* ((Directed I) +* (Start-At (insloc 0 ))) by A1, Th50;
A10: k = pseudo-LifeSpan s,(Directed I) by A1, Th50;
( I ';' (Stop SCM+FSA ) c= (I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )) & (I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )) c= s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) ) by FUNCT_4:26, SCMFSA8A:9;
then ( ProgramPart (Relocated (Directed I),0 ) c= I ';' (Stop SCM+FSA ) & I ';' (Stop SCM+FSA ) c= s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) ) by A2, Th9, XBOOLE_1:1;
then A11: ProgramPart (Relocated (Directed I),0 ) c= s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) by XBOOLE_1:1;
s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) = (s +* (I ';' (Stop SCM+FSA ))) +* (Start-At (insloc 0 )) by FUNCT_4:15;
then A12: IC (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = insloc 0 by AMI_1:111;
A13: DataPart (s +* ((Directed I) +* (Start-At (insloc 0 )))) = DataPart s by SCMFSA8A:11
.= DataPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) by SCMFSA8A:11 ;

A14: now

let n be Element of NAT ; :: thesis: ( n < pseudo-LifeSpan (s +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I) implies ( CurInstr (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),n) = CurInstr (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) & IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),n) in dom (Directed I) & CurInstr (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),n) <> halt SCM+FSA ) )
assume A15: n < pseudo-LifeSpan (s +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I) ; :: thesis: ( CurInstr (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),n) = CurInstr (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) & IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),n) in dom (Directed I) & CurInstr (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),n) <> halt SCM+FSA )
then IncAddr (CurInstr (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),n)),0 = CurInstr (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) by A7, A9, A11, A12, A13, Th51;
hence CurInstr (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),n) = CurInstr (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) by Th8; :: thesis: ( IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),n) in dom (Directed I) & CurInstr (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),n) <> halt SCM+FSA )
thus IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),n) in dom (Directed I) by A8, A9, A15, SCMFSA8A:31; :: thesis: CurInstr (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),n) <> halt SCM+FSA
thus CurInstr (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),n) <> halt SCM+FSA by A8, A9, A15, SCMFSA8A:31; :: thesis: verum

end;

A16: now

let n be Element of NAT ; :: thesis: ( n <= pseudo-LifeSpan (s +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I) implies ( IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),n) = IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) & DataPart (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),n) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) ) )
assume A17: n <= pseudo-LifeSpan (s +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I) ; :: thesis: ( IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),n) = IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) & DataPart (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),n) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) )
then (IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),n)) + 0 = IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) by A7, A9, A11, A12, A13, Th51;
hence IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),n) = IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) ; :: thesis: DataPart (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),n) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n)
thus DataPart (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),n) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) by A7, A9, A11, A12, A13, A17, Th51; :: thesis: verum

end;

defpred S₁[ Element of NAT ] means ( k <= $1 implies ( IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),$1) = insloc (card I) & CurInstr (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),$1) = halt SCM+FSA ) );
A18: S₁[ 0 ]

proof

assume k <= 0 ; :: thesis: ( IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),0 ) = insloc (card I) & CurInstr (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),0 ) = halt SCM+FSA )
then k = 0 ;
hence IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),0 ) = IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),k) by A16
.= insloc (card (ProgramPart (Directed I))) by A1, A10, SCMFSA8A:def 5
.= insloc (card (Directed I)) by AMI_1:105
.= insloc (card I) by SCMFSA8A:34 ;
:: thesis: CurInstr (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),0 ) = halt SCM+FSA
hence CurInstr (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),0 ) = halt SCM+FSA by A6, AMI_1:13; :: thesis: verum

end;

A19: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A20: S₁[n] ; :: thesis: S₁[n + 1]
assume A21: k <= n + 1 ; :: thesis: ( IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),(n + 1)) = insloc (card I) & CurInstr (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),(n + 1)) = halt SCM+FSA )

hereby :: thesis: CurInstr (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),(n + 1)) = halt SCM+FSA

per cases ( k = n + 1 or k <= n ) by A21, NAT_1:8;

suppose k = n + 1 ; :: thesis: IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),(n + 1)) = insloc (card I)

hence IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),(n + 1)) = IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),k) by A16
.= insloc (card (ProgramPart (Directed I))) by A1, A10, SCMFSA8A:def 5
.= insloc (card (Directed I)) by AMI_1:105
.= insloc (card I) by SCMFSA8A:34 ;
:: thesis: verum

end;

suppose A22: k <= n ; :: thesis: IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),(n + 1)) = insloc (card I)

Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),(n + 1) = Following (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) by AMI_1:14
.= Exec (CurInstr (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n)),(Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) ;
hence IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),(n + 1)) = insloc (card I) by A20, A22, AMI_1:def 8; :: thesis: verum

end;

end;

end;

hence CurInstr (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),(n + 1)) = halt SCM+FSA by A6, AMI_1:54; :: thesis: verum

end;

A23: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A18, A19);

now

let n be Element of NAT ; :: thesis: IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),b₁) in dom (I ';' (Stop SCM+FSA ))

per cases ( n < k or k <= n ) ;

suppose A24: n < k ; :: thesis: IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),b₁) in dom (I ';' (Stop SCM+FSA ))

then IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),n) = IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) by A16;
then IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) in dom (Directed I) by A1, A10, A24, SCMFSA8A:def 5;
hence IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) in dom (I ';' (Stop SCM+FSA )) by A3; :: thesis: verum

end;

suppose k <= n ; :: thesis: IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),b₁) in dom (I ';' (Stop SCM+FSA ))

hence IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) in dom (I ';' (Stop SCM+FSA )) by A4, A23; :: thesis: verum

end;

end;

end;

hence I ';' (Stop SCM+FSA ) is_closed_on s by SCMFSA7B:def 7; :: thesis: ( I ';' (Stop SCM+FSA ) is_halting_on s & LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = pseudo-LifeSpan s,(Directed I) & ( for n being Element of NAT st n < pseudo-LifeSpan s,(Directed I) holds
IC (Computation (s +* (I +* (Start-At (insloc 0 )))),n) = IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) ) & ( for n being Element of NAT st n <= pseudo-LifeSpan s,(Directed I) holds
DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),n) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) ) )
S₁[k] by A23;
then A25: s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) is halting by AMI_1:def 20;
hence I ';' (Stop SCM+FSA ) is_halting_on s by SCMFSA7B:def 8; :: thesis: ( LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = pseudo-LifeSpan s,(Directed I) & ( for n being Element of NAT st n < pseudo-LifeSpan s,(Directed I) holds
IC (Computation (s +* (I +* (Start-At (insloc 0 )))),n) = IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) ) & ( for n being Element of NAT st n <= pseudo-LifeSpan s,(Directed I) holds
DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),n) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) ) )
A26: CurInstr (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) = halt SCM+FSA by A23;

now

let n be Element of NAT ; :: thesis: ( CurInstr (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) = halt SCM+FSA implies not k > n )
assume A27: CurInstr (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) = halt SCM+FSA ; :: thesis: not k > n
assume A28: k > n ; :: thesis: contradiction
reconsider l = IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),n) as Instruction-Location of SCM+FSA ;
A29: l in dom (Directed I) by A1, A10, A28, SCMFSA8A:def 5;
CurInstr (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) = CurInstr (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),n) by A14, A28
.= (s +* ((Directed I) +* (Start-At (insloc 0 )))) . l by AMI_1:54
.= (Directed I) . l by A29, Th26 ;
then halt SCM+FSA in rng (Directed I) by A27, A29, FUNCT_1:def 5;
hence contradiction by AMI_1:def 52; :: thesis: verum

end;

then A30: LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = k by A25, A26, AMI_1:def 46;
IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) = insloc (card I) by A23;
then A31: IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),(LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))))) = insloc (card I) by A16, A30;
A32: card (ProgramPart (Directed I)) = card (Directed I) by AMI_1:105
.= card I by SCMFSA8A:34 ;
for n being Element of NAT st not IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),n) in dom (Directed I) holds
LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) <= n by A14, A30;
hence LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = pseudo-LifeSpan s,(Directed I) by A1, A31, A32, SCMFSA8A:def 5; :: thesis: ( ( for n being Element of NAT st n < pseudo-LifeSpan s,(Directed I) holds
IC (Computation (s +* (I +* (Start-At (insloc 0 )))),n) = IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) ) & ( for n being Element of NAT st n <= pseudo-LifeSpan s,(Directed I) holds
DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),n) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) ) )
set s1 = s +* (I +* (Start-At (insloc 0 )));
defpred S₂[ Element of NAT ] means ( $1 < pseudo-LifeSpan s,(Directed I) implies ( IC (Computation (s +* (I +* (Start-At (insloc 0 )))),$1) in dom I & IC (Computation (s +* (I +* (Start-At (insloc 0 )))),$1) = IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),$1) & DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),$1) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),$1) ) );
A33: S₂[ 0 ]

proof

assume 0 < pseudo-LifeSpan s,(Directed I) ; :: thesis: ( IC (Computation (s +* (I +* (Start-At (insloc 0 )))),0 ) in dom I & IC (Computation (s +* (I +* (Start-At (insloc 0 )))),0 ) = IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),0 ) & DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),0 ) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),0 ) )
then IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),0 ) in dom (Directed I) by A1, SCMFSA8A:31;
then IC (s +* ((Directed I) +* (Start-At (insloc 0 )))) in dom (Directed I) by AMI_1:13;
then A34: insloc 0 in dom (Directed I) by Th31;
A35: IC (Computation (s +* (I +* (Start-At (insloc 0 )))),0 ) = IC (s +* (I +* (Start-At (insloc 0 )))) by AMI_1:13
.= IC ((s +* I) +* (Start-At (insloc 0 ))) by FUNCT_4:15
.= insloc 0 by AMI_1:111 ;
hence IC (Computation (s +* (I +* (Start-At (insloc 0 )))),0 ) in dom I by A34, FUNCT_4:105; :: thesis: ( IC (Computation (s +* (I +* (Start-At (insloc 0 )))),0 ) = IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),0 ) & DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),0 ) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),0 ) )
thus IC (Computation (s +* (I +* (Start-At (insloc 0 )))),0 ) = IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),0 ) by A12, A35, AMI_1:13; :: thesis: DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),0 ) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),0 )
thus DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),0 ) = DataPart (s +* (I +* (Start-At (insloc 0 )))) by AMI_1:13
.= DataPart s by SCMFSA8A:11
.= DataPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) by SCMFSA8A:11
.= DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),0 ) by AMI_1:13 ; :: thesis: verum

end;

A36: for n being Element of NAT st S₂[n] holds
S₂[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₂[n] implies S₂[n + 1] )
set l = IC (Computation (s +* (I +* (Start-At (insloc 0 )))),n);
set l0 = IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n);
assume A37: S₂[n] ; :: thesis: S₂[n + 1]
assume A38: n + 1 < pseudo-LifeSpan s,(Directed I) ; :: thesis: ( IC (Computation (s +* (I +* (Start-At (insloc 0 )))),(n + 1)) in dom I & IC (Computation (s +* (I +* (Start-At (insloc 0 )))),(n + 1)) = IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),(n + 1)) & DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),(n + 1)) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),(n + 1)) )
A39: pseudo-LifeSpan s,(Directed I) = k by A1, Th50;
n < k by A10, A38, NAT_1:12;
then A40: ( IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),(n + 1)) = IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),(n + 1)) & DataPart (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),n) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) & IC (Computation (s +* (I +* (Start-At (insloc 0 )))),n) in dom I & IC (Computation (s +* (I +* (Start-At (insloc 0 )))),n) = IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) & DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),n) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) ) by A16, A37, A38, A39;
A41: IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) in dom (Directed I) by A37, A38, FUNCT_4:105, NAT_1:12;

A42: now

assume A43: I . (IC (Computation (s +* (I +* (Start-At (insloc 0 )))),n)) = halt SCM+FSA ; :: thesis: contradiction
A44: ( IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) in dom I & dom I = dom (Directed I) ) by A37, A38, FUNCT_4:105, NAT_1:12;
n < k by A10, A38, NAT_1:12;
then A45: CurInstr (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),n) = (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),n) . (IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n)) by A16
.= (s +* ((Directed I) +* (Start-At (insloc 0 )))) . (IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n)) by AMI_1:54
.= (Directed I) . (IC (Computation (s +* (I +* (Start-At (insloc 0 )))),n)) by A37, A38, A44, Th26, NAT_1:12
.= goto (insloc (card I)) by A37, A38, A43, NAT_1:12, SCMFSA8A:30 ;
A46: IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),(n + 1)) = IC (Following (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),n)) by AMI_1:14
.= insloc (card I) by A45, SCMFSA_2:95
.= insloc (card (Directed I)) by SCMFSA8A:34 ;
IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),(n + 1)) in dom (Directed I) by A1, A38, SCMFSA8A:31;
hence contradiction by A46, SCMFSA6A:15; :: thesis: verum

end;

A47: CurInstr (Computation (s +* (I +* (Start-At (insloc 0 )))),n) = (s +* (I +* (Start-At (insloc 0 )))) . (IC (Computation (s +* (I +* (Start-At (insloc 0 )))),n)) by AMI_1:54
.= I . (IC (Computation (s +* (I +* (Start-At (insloc 0 )))),n)) by A37, A38, Th26, NAT_1:12
.= (Directed I) . (IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n)) by A37, A38, A42, NAT_1:12, SCMFSA8A:30
.= (I ';' (Stop SCM+FSA )) . (IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n)) by A2, A41, GRFUNC_1:8
.= (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) . (IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n)) by A3, A41, Th26
.= CurInstr (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) by AMI_1:54 ;
A48: Computation (s +* (I +* (Start-At (insloc 0 )))),(n + 1) = Following (Computation (s +* (I +* (Start-At (insloc 0 )))),n) by AMI_1:14
.= Exec (CurInstr (Computation (s +* (I +* (Start-At (insloc 0 )))),n)),(Computation (s +* (I +* (Start-At (insloc 0 )))),n) ;
A49: Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),(n + 1) = Following (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) by AMI_1:14
.= Exec (CurInstr (Computation (s +* (I +* (Start-At (insloc 0 )))),n)),(Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) by A47 ;
( ( for a being Int-Location holds (Computation (s +* (I +* (Start-At (insloc 0 )))),n) . a = (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) . a ) & ( for f being FinSeq-Location holds (Computation (s +* (I +* (Start-At (insloc 0 )))),n) . f = (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) . f ) ) by A37, A38, NAT_1:12, SCMFSA6A:38;
then A50: Computation (s +* (I +* (Start-At (insloc 0 )))),n, Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n equal_outside NAT by A37, A38, NAT_1:12, SCMFSA6A:28;
then A51: Computation (s +* (I +* (Start-At (insloc 0 )))),(n + 1), Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),(n + 1) equal_outside NAT by A48, A49, SCMFSA6A:32;
( dom (Directed I) = dom I & IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),(n + 1)) in dom (Directed I) ) by A1, A38, FUNCT_4:105, SCMFSA8A:31;
hence IC (Computation (s +* (I +* (Start-At (insloc 0 )))),(n + 1)) in dom I by A40, A48, A49, A50, AMI_1:121, SCMFSA6A:32; :: thesis: ( IC (Computation (s +* (I +* (Start-At (insloc 0 )))),(n + 1)) = IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),(n + 1)) & DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),(n + 1)) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),(n + 1)) )
thus IC (Computation (s +* (I +* (Start-At (insloc 0 )))),(n + 1)) = IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),(n + 1)) by A48, A49, A50, AMI_1:121, SCMFSA6A:32; :: thesis: DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),(n + 1)) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),(n + 1))
( ( for a being Int-Location holds (Computation (s +* (I +* (Start-At (insloc 0 )))),(n + 1)) . a = (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),(n + 1)) . a ) & ( for f being FinSeq-Location holds (Computation (s +* (I +* (Start-At (insloc 0 )))),(n + 1)) . f = (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),(n + 1)) . f ) ) by A51, SCMFSA6A:30, SCMFSA6A:31;
hence DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),(n + 1)) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),(n + 1)) by SCMFSA6A:38; :: thesis: verum

end;

A52: for n being Element of NAT holds S₂[n] from NAT_1:sch 1(A33, A36);
hence for n being Element of NAT st n < pseudo-LifeSpan s,(Directed I) holds
IC (Computation (s +* (I +* (Start-At (insloc 0 )))),n) = IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) ; :: thesis: for n being Element of NAT st n <= pseudo-LifeSpan s,(Directed I) holds
DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),n) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n)
let n be Element of NAT ; :: thesis: ( n <= pseudo-LifeSpan s,(Directed I) implies DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),n) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) )
assume A53: n <= pseudo-LifeSpan s,(Directed I) ; :: thesis: DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),n) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n)

per cases ( n < pseudo-LifeSpan s,(Directed I) or n = pseudo-LifeSpan s,(Directed I) ) by A53, XXREAL_0:1;

suppose n < pseudo-LifeSpan s,(Directed I) ; :: thesis: DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),n) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n)

hence DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),n) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) by A52; :: thesis: verum

end;

suppose A54: n = pseudo-LifeSpan s,(Directed I) ; :: thesis: DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),n) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n)

hereby :: thesis: verum

per cases ( n = 0 or ex m being Nat st n = m + 1 ) by NAT_1:6;

suppose A55: n = 0 ; :: thesis: DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),n) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n)

hence DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),n) = DataPart (s +* (I +* (Start-At (insloc 0 )))) by AMI_1:13
.= DataPart s by SCMFSA8A:11
.= DataPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) by SCMFSA8A:11
.= DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) by A55, AMI_1:13 ;
:: thesis: verum

end;

suppose ex m being Nat st n = m + 1 ; :: thesis: DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),n) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n)

then consider m being Nat such that
A56: n = m + 1 ;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
A57: Computation (s +* (I +* (Start-At (insloc 0 )))),n = Following (Computation (s +* (I +* (Start-At (insloc 0 )))),m) by A56, AMI_1:14
.= Exec (CurInstr (Computation (s +* (I +* (Start-At (insloc 0 )))),m)),(Computation (s +* (I +* (Start-At (insloc 0 )))),m) ;
A58: Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n = Following (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),m) by A56, AMI_1:14
.= Exec (CurInstr (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),m)),(Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),m) ;
set i = CurInstr (Computation (s +* (I +* (Start-At (insloc 0 )))),m);
set l = IC (Computation (s +* (I +* (Start-At (insloc 0 )))),m);
set l0 = IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),m);
A59: m + 0 < pseudo-LifeSpan s,(Directed I) by A54, A56, XREAL_1:8;
then A60: ( DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),m) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),m) & IC (Computation (s +* (I +* (Start-At (insloc 0 )))),m) in dom I & IC (Computation (s +* (I +* (Start-At (insloc 0 )))),m) = IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),m) ) by A52;
then A61: IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),m) in dom (Directed I) by FUNCT_4:105;
A62: CurInstr (Computation (s +* (I +* (Start-At (insloc 0 )))),m) = (s +* (I +* (Start-At (insloc 0 )))) . (IC (Computation (s +* (I +* (Start-At (insloc 0 )))),m)) by AMI_1:54
.= I . (IC (Computation (s +* (I +* (Start-At (insloc 0 )))),m)) by A59, A52, Th26 ;
Directed I c= I ';' (Stop SCM+FSA ) by SCMFSA6A:55;
then A63: (Directed I) . (IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),m)) = (I ';' (Stop SCM+FSA )) . (IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),m)) by A61, GRFUNC_1:8
.= (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) . (IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),m)) by A3, A61, Th26
.= CurInstr (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),m) by AMI_1:54 ;

hereby :: thesis: verum

per cases ( CurInstr (Computation (s +* (I +* (Start-At (insloc 0 )))),m) = halt SCM+FSA or CurInstr (Computation (s +* (I +* (Start-At (insloc 0 )))),m) <> halt SCM+FSA ) ;

suppose A64: CurInstr (Computation (s +* (I +* (Start-At (insloc 0 )))),m) = halt SCM+FSA ; :: thesis: DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),n) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n)

then CurInstr (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),m) = goto (insloc (card I)) by A60, A62, A63, SCMFSA8A:30;
then InsCode (CurInstr (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),m)) = 6 by SCMFSA_2:47;
then A65: InsCode (CurInstr (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),m)) in {0 ,6,7,8} by ENUMSET1:def 2;
thus DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),n) = DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),m) by A57, A64, AMI_1:def 8
.= DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),m) by A52, A59
.= DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) by A58, A65, Th32 ; :: thesis: verum

end;

suppose CurInstr (Computation (s +* (I +* (Start-At (insloc 0 )))),m) <> halt SCM+FSA ; :: thesis: DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),n) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n)

then CurInstr (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),m) = CurInstr (Computation (s +* (I +* (Start-At (insloc 0 )))),m) by A60, A62, A63, SCMFSA8A:30;
hence DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),n) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) by A57, A58, A60, SCMFSA6C:5; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

end;