let s be State of SCM+FSA; :: thesis:
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis:
set A = NAT ;
let I be paraclosed Program of SCM+FSA; :: thesis:
assume that
A1: P +* I halts_on s +* I and
A2: Directed I c= s and
A3: Directed I c= P and
A4: Start-At (0,SCM+FSA) c= s ; :: thesis:
set sISA0 = s +* (Initialize I);
A5: s +* (Initialize I) = Initialize (s +* I) by FUNCT_4:15
.= (Initialize s) +* I by COMPOS_1:83
.= s +* I by A4, FUNCT_4:79 ;
set s1 = (s +* (Initialize I)) +* (I ';' I);
A6: I c= P +* I by FUNCT_4:26;
set s2 = (s +* (Initialize I)) +* (Directed I);
set IAt = Initialize I;
A7: dom (Directed I) = dom I by FUNCT_4:105;
(s +* (Initialize I)) +* (Directed I) = (Initialize (s +* I)) +* (Directed I) by FUNCT_4:15
.= ((Initialize s) +* I) +* (Directed I) by COMPOS_1:83
.= (s +* I) +* (Directed I) by A4, FUNCT_4:79
.= s +* (I +* (Directed I)) by FUNCT_4:15
.= s +* (Directed I) by A7, FUNCT_4:20 ;
then A8: (s +* (Initialize I)) +* (Directed I) = s by A2, FUNCT_4:79;
set m = LifeSpan ((P +* I),(s +* (Initialize I)));
set l1 = IC (Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I))))));
A9: Initialize I c= s +* (Initialize I) by FUNCT_4:26;
ProgramPart (Initialize I) = I by COMPOS_1:144;
then A10: ProgramPart (Initialize I) c= P +* I by FUNCT_4:26;
A11: ProgramPart (Initialize I) = I by COMPOS_1:144;
A12: IC (Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I)))))) in dom I by Def2, A9, A10, A11;

A13: now

let k be Element of NAT ; :: thesis:
defpred S₁[ Nat] means ( $1 <= k implies Comput (((P +* I) +* (I ';' I)),((s +* (Initialize I)) +* (I ';' I)),$1), Comput (P,s,$1) equal_outside NAT );
assume A14: k <= LifeSpan ((P +* I),(s +* (Initialize I))) ; :: thesis:
A15: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

A16: Directed I c= I ';' I by SCMFSA6A:55;
let n be Element of NAT ; :: thesis:
A17: dom I c= dom (I ';' I) by SCMFSA6A:56;
assume A18: ( n <= k implies Comput (((P +* I) +* (I ';' I)),((s +* (Initialize I)) +* (I ';' I)),n), Comput (P,s,n) equal_outside NAT ) ; :: thesis:
A19: Comput (P,s,(n + 1)) = Following (P,(Comput (P,s,n))) by EXTPRO_1:4
.= Exec ((CurInstr (P,(Comput (P,s,n)))),(Comput (P,s,n))) ;
A20: Comput (((P +* I) +* (I ';' I)),((s +* (Initialize I)) +* (I ';' I)),(n + 1)) = Following (((P +* I) +* (I ';' I)),(Comput (((P +* I) +* (I ';' I)),((s +* (Initialize I)) +* (I ';' I)),n))) by EXTPRO_1:4
.= Exec ((CurInstr (((P +* I) +* (I ';' I)),(Comput (((P +* I) +* (I ';' I)),((s +* (Initialize I)) +* (I ';' I)),n)))),(Comput (((P +* I) +* (I ';' I)),((s +* (Initialize I)) +* (I ';' I)),n))) ;
A21: n <= n + 1 by NAT_1:12;
assume A22: n + 1 <= k ; :: thesis:
then A23: IC (Comput (((P +* I) +* (I ';' I)),((s +* (Initialize I)) +* (I ';' I)),n)) = IC (Comput (P,s,n)) by A18, A21, COMPOS_1:24, XXREAL_0:2;
n <= k by A22, A21, XXREAL_0:2;
then Comput ((P +* I),(s +* (Initialize I)),n), Comput (((P +* I) +* (I ';' I)),((s +* (Initialize I)) +* (I ';' I)),n) equal_outside NAT by A1, Th36, A5, A9, A14, XXREAL_0:2, A6;
then IC (Comput ((P +* I),(s +* (Initialize I)),n)) = IC (Comput (((P +* I) +* (I ';' I)),((s +* (Initialize I)) +* (I ';' I)),n)) by COMPOS_1:24;
then A24: IC (Comput (((P +* I) +* (I ';' I)),((s +* (Initialize I)) +* (I ';' I)),n)) in dom I by Def2, A9, A10, A11;
then A25: IC (Comput (P,s,n)) in dom (Directed I) by A23, FUNCT_4:105;
A26: dom P = NAT by PARTFUN1:def 4;
A27: CurInstr (P,(Comput (P,s,n))) = P . (IC (Comput (P,s,n))) by A26, PARTFUN1:def 8
.= (Directed I) . (IC (Comput (P,s,n))) by A25, A3, GRFUNC_1:8 ;
A28: dom ((P +* I) +* (I ';' I)) = NAT by PARTFUN1:def 4;
CurInstr (((P +* I) +* (I ';' I)),(Comput (((P +* I) +* (I ';' I)),((s +* (Initialize I)) +* (I ';' I)),n))) = ((P +* I) +* (I ';' I)) . (IC (Comput (((P +* I) +* (I ';' I)),((s +* (Initialize I)) +* (I ';' I)),n))) by A28, PARTFUN1:def 8
.= (I ';' I) . (IC (Comput (((P +* I) +* (I ';' I)),((s +* (Initialize I)) +* (I ';' I)),n))) by A17, A24, FUNCT_4:14
.= (Directed I) . (IC (Comput (((P +* I) +* (I ';' I)),((s +* (Initialize I)) +* (I ';' I)),n))) by A16, A23, A25, GRFUNC_1:8 ;
hence Comput (((P +* I) +* (I ';' I)),((s +* (Initialize I)) +* (I ';' I)),(n + 1)), Comput (P,s,(n + 1)) equal_outside NAT by A18, A22, A21, A23, A27, A20, A19, AMISTD_2:def 20, XXREAL_0:2; :: thesis:

end;

( Comput (((P +* I) +* (I ';' I)),((s +* (Initialize I)) +* (I ';' I)),0) = (s +* (Initialize I)) +* (I ';' I) & Comput (P,s,0) = s ) by EXTPRO_1:3;
then Comput (P,s,0), Comput (((P +* I) +* (I ';' I)),((s +* (Initialize I)) +* (I ';' I)),0) equal_outside NAT by FUNCT_7:107, FUNCT_7:133, A8;
then A29: S₁[ 0 ] by FUNCT_7:28;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A29, A15);
then A30: Comput (((P +* I) +* (I ';' I)),((s +* (Initialize I)) +* (I ';' I)),k), Comput (P,s,k) equal_outside NAT ;
( I c= P +* I & Initialize I c= s +* (Initialize I) & P +* I halts_on s +* (Initialize I) implies for m being Element of NAT st m <= LifeSpan ((P +* I),(s +* (Initialize I))) holds
Comput ((P +* I),(s +* (Initialize I)),m), Comput (((P +* I) +* (I ';' I)),((s +* (Initialize I)) +* (I ';' I)),m) equal_outside NAT ) by Th36;
then Comput ((P +* I),(s +* (Initialize I)),k), Comput (((P +* I) +* (I ';' I)),((s +* (Initialize I)) +* (I ';' I)),k) equal_outside NAT by A1, A5, A14, FUNCT_4:26;
hence Comput ((P +* I),(s +* (Initialize I)),k), Comput (P,s,k) equal_outside NAT by A30, FUNCT_7:29; :: thesis:

end;