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) ) )
set D = Int-Locations \/ FinSeq-Locations ;
set A = NAT ;
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 )));
reconsider k = pseudo-LifeSpan (s +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I) as Element of NAT ;
A1: halt SCM+FSA = (Stop SCM+FSA ) . (insloc ((card I) -' (card I))) by SCMFSA8A:16, XREAL_1:234;
A2: 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 ;
assume A3: 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) ) )
then A4: Directed I is_pseudo-closed_on s +* ((Directed I) +* (Start-At (insloc 0 ))) by Th50;
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 ) );
A5: (I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )) c= s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) by FUNCT_4:26;
I ';' (Stop SCM+FSA ) c= (I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )) by SCMFSA8A:9;
then A6: I ';' (Stop SCM+FSA ) c= s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) by A5, XBOOLE_1:1;
A7: Directed I c= I ';' (Stop SCM+FSA ) by SCMFSA6A:55;
then A8: dom (Directed I) c= dom (I ';' (Stop SCM+FSA )) by GRFUNC_1:8;
ProgramPart (Relocated (Directed I),0 ) c= I ';' (Stop SCM+FSA ) by A7, Th9;
then A9: ProgramPart (Relocated (Directed I),0 ) c= s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) by A6, 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 A10: IC (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = insloc 0 by AMI_1:111;
A11: (Directed I) +* (Start-At (insloc 0 )) c= s +* ((Directed I) +* (Start-At (insloc 0 ))) by FUNCT_4:26;

A12: 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 A13: 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 A11, A4, A9, A10, A2, 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 A11, A4, A9, A10, A2, A13, Th51; :: thesis: verum

end;

A14: k = pseudo-LifeSpan s,(Directed I) by A3, Th50;
A15: (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 ))) ;

A16: 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 A17: 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 A11, A4, A9, A10, A2, 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 A15, A4, A17, 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 A15, A4, A17, SCMFSA8A:31; :: thesis: verum

end;

A18: 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 A19: CurInstr (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) = halt SCM+FSA ; :: thesis: not k > n
reconsider l = IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),n) as Instruction-Location of SCM+FSA ;
assume A20: k > n ; :: thesis: contradiction
then A21: l in dom (Directed I) by A3, A14, 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 A16, A20
.= (s +* ((Directed I) +* (Start-At (insloc 0 )))) . l by AMI_1:54
.= (Directed I) . l by A21, Th26 ;
then halt SCM+FSA in rng (Directed I) by A19, A21, FUNCT_1:def 5;
hence contradiction by AMI_1:def 53; :: thesis: verum

end;

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 A22: insloc (card I) in dom (I ';' (Stop SCM+FSA )) by SCMFSA6A:15;
card I < (card I) + (card (Stop SCM+FSA )) by NAT_1:13, SCMFSA8A:17;
then (I ';' (Stop SCM+FSA )) . (insloc (card I)) = IncAddr (halt SCM+FSA ),(card I) by A1, Th13
.= halt SCM+FSA by SCMFSA_4:8 ;
then A23: (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) . (insloc (card I)) = halt SCM+FSA by A22, Th26;
A24: 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 A25: S₁[n] ; :: thesis: S₁[n + 1]
assume A26: 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 A26, 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 A12
.= insloc (card (ProgramPart (Directed I))) by A3, A14, SCMFSA8A:def 5
.= insloc (card (Directed I)) by AMI_1:105
.= insloc (card I) by SCMFSA8A:34 ;
:: thesis: verum

end;

suppose A27: 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 A25, A27, 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 A23, AMI_1:54; :: thesis: verum

end;

A28: 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 A12
.= insloc (card (ProgramPart (Directed I))) by A3, A14, 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 A23, AMI_1:13; :: thesis: verum

end;

A29: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A28, A24);

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 A30: 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 A12;
then IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) in dom (Directed I) by A3, A14, A30, SCMFSA8A:def 5;
hence IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) in dom (I ';' (Stop SCM+FSA )) by A8; :: 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 A22, A29; :: 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) ) )
set s1 = s +* (I +* (Start-At (insloc 0 )));
A31: card (ProgramPart (Directed I)) = card (Directed I) by AMI_1:105
.= card I by SCMFSA8A:34 ;
S₁[k] by A29;
then A32: 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) ) )
CurInstr (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) = halt SCM+FSA by A29;
then A33: LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = k by A32, A18, AMI_1:def 46;
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) ) );
A34: 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 A35: S₂[n] ; :: thesis: S₂[n + 1]
assume A36: 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)) )
then A37: IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) in dom (Directed I) by A35, FUNCT_4:105, NAT_1:12;
A38: 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 A35, A36, NAT_1:12, SCMFSA6A:38;
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 by A35, A36, NAT_1:12, SCMFSA6A:38;
then A39: Computation (s +* (I +* (Start-At (insloc 0 )))),n, Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n equal_outside NAT by A35, A36, A38, NAT_1:12, SCMFSA6A:28;

A40: now

A41: dom I = dom (Directed I) by FUNCT_4:105;
assume A42: I . (IC (Computation (s +* (I +* (Start-At (insloc 0 )))),n)) = halt SCM+FSA ; :: thesis: contradiction
n < k by A14, A36, NAT_1:12;
then A43: 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 A12
.= (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 A35, A36, A41, Th26, NAT_1:12
.= goto (insloc (card I)) by A35, A36, A42, NAT_1:12, SCMFSA8A:30 ;
A44: 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 A43, 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 A3, A36, SCMFSA8A:31;
hence contradiction by A44, SCMFSA6A:15; :: thesis: verum

end;

A45: 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 A35, A36, Th26, NAT_1:12
.= (Directed I) . (IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n)) by A35, A36, A40, NAT_1:12, SCMFSA8A:30
.= (I ';' (Stop SCM+FSA )) . (IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n)) by A7, A37, 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 A8, A37, Th26
.= CurInstr (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) by AMI_1:54 ;
A46: 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 A45 ;
pseudo-LifeSpan s,(Directed I) = k by A3, Th50;
then A47: IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),(n + 1)) = IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),(n + 1)) by A12, A36;
A48: dom (Directed I) = dom I by FUNCT_4:105;
A49: 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) ;
then A50: 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 A46, A39, SCMFSA6A:31, SCMFSA6A:32;
IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),(n + 1)) in dom (Directed I) by A3, A36, SCMFSA8A:31;
hence IC (Computation (s +* (I +* (Start-At (insloc 0 )))),(n + 1)) in dom I by A47, A49, A46, A39, A48, 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 A49, A46, A39, 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 by A49, A46, A39, SCMFSA6A:30, SCMFSA6A:32;
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 A50, SCMFSA6A:38; :: thesis: verum

end;

IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) = insloc (card I) by A29;
then A51: IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),(LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))))) = insloc (card I) by A12, A33;
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 A16, A33;
hence LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = pseudo-LifeSpan s,(Directed I) by A3, A51, A31, 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) ) )
A52: S₂[ 0 ]

proof

A53: 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 ;
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 A3, SCMFSA8A:31;
then IC (s +* ((Directed I) +* (Start-At (insloc 0 )))) in dom (Directed I) by AMI_1:13;
then insloc 0 in dom (Directed I) by Th31;
hence IC (Computation (s +* (I +* (Start-At (insloc 0 )))),0 ) in dom I by A53, 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 A10, A53, 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;

A54: for n being Element of NAT holds S₂[n] from NAT_1:sch 1(A52, A34);
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 A55: 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 A55, 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 A54; :: thesis: verum

end;

suppose A56: 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 A57: 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 A57, 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
A58: n = m + 1 ;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
A59: Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n = Following (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),m) by A58, 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);
A60: Computation (s +* (I +* (Start-At (insloc 0 )))),n = Following (Computation (s +* (I +* (Start-At (insloc 0 )))),m) by A58, AMI_1:14
.= Exec (CurInstr (Computation (s +* (I +* (Start-At (insloc 0 )))),m)),(Computation (s +* (I +* (Start-At (insloc 0 )))),m) ;
set l0 = IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),m);
set l = IC (Computation (s +* (I +* (Start-At (insloc 0 )))),m);
A61: m + 0 < pseudo-LifeSpan s,(Directed I) by A56, A58, XREAL_1:8;
then A62: IC (Computation (s +* (I +* (Start-At (insloc 0 )))),m) = IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),m) by A54;
A63: IC (Computation (s +* (I +* (Start-At (insloc 0 )))),m) in dom I by A54, A61;
then A64: IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),m) in dom (Directed I) by A62, FUNCT_4:105;
A65: 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 A54, A61, Th26 ;
Directed I c= I ';' (Stop SCM+FSA ) by SCMFSA6A:55;
then A66: (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 A64, 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 A8, A64, Th26
.= CurInstr (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),m) by AMI_1:54 ;
A67: DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),m) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),m) by A54, A61;

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 A68: 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 A63, A62, A65, A66, SCMFSA8A:30;
then InsCode (CurInstr (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),m)) = 6 by SCMFSA_2:47;
then A69: 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 A60, A68, AMI_1:def 8
.= DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),m) by A54, A61
.= DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),n) by A59, A69, 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 A63, A62, A65, A66, 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 A60, A59, A67, SCMFSA6C:5; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

end;