let s be State of ; :: thesis:
set A = NAT ;
let I be InitClosed Program of ; :: thesis:
assume that
A1: ProgramPart (s +* I) halts_on s +* I and
A2: Directed I c= s and
A3: ((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )) c= s ; :: thesis:
set sISA0 = s +* (I +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))));
A4: Initialized I c= s +* (I +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )))) by A3, Th20;
set IAt = I +* (Start-At (insloc 0 ));
dom I misses dom (Start-At (insloc 0 )) by SF_MASTR:64;
then I c= I +* (Start-At (insloc 0 )) by FUNCT_4:33;
then A5: dom I c= dom (I +* (Start-At (insloc 0 ))) by GRFUNC_1:8;
A6: s +* (I +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )))) = s +* I by A3, Th20;
reconsider sISA0 = s +* (I +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )))) as State of ;
set m = LifeSpan sISA0;
set l1 = IC (Computation sISA0,(LifeSpan sISA0));
A7: IC (Computation sISA0,(LifeSpan sISA0)) in dom I by A4, Def1;
set s2 = sISA0 +* (Directed I);

A8: now

set s1 = sISA0 +* (I ';' I);
let k be Element of NAT ; :: thesis:
defpred S₁[ Element of NAT ] means ( $1 <= k implies Computation (sISA0 +* (I ';' I)),$1, Computation (sISA0 +* (Directed I)),$1 equal_outside NAT );
assume A9: k <= LifeSpan sISA0 ; :: thesis:
A10: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

A11: Directed I c= I ';' I by SCMFSA6A:55;
let n be Element of NAT ; :: thesis:
A12: dom I c= dom (I ';' I) by SCMFSA6A:56;
assume A13: ( n <= k implies Computation (sISA0 +* (I ';' I)),n, Computation (sISA0 +* (Directed I)),n equal_outside NAT ) ; :: thesis:
A14: Computation (sISA0 +* (Directed I)),(n + 1) = Following (Computation (sISA0 +* (Directed I)),n) by AMI_1:14
.= Exec (CurInstr (Computation (sISA0 +* (Directed I)),n)),(Computation (sISA0 +* (Directed I)),n) ;
A15: Computation (sISA0 +* (I ';' I)),(n + 1) = Following (Computation (sISA0 +* (I ';' I)),n) by AMI_1:14
.= Exec (CurInstr (Computation (sISA0 +* (I ';' I)),n)),(Computation (sISA0 +* (I ';' I)),n) ;
A16: n <= n + 1 by NAT_1:12;
assume A17: n + 1 <= k ; :: thesis:
then A18: IC (Computation (sISA0 +* (I ';' I)),n) = IC (Computation (sISA0 +* (Directed I)),n) by A13, A16, AMI_1:121, XXREAL_0:2;
n <= k by A17, A16, XXREAL_0:2;
then n <= LifeSpan sISA0 by A9, XXREAL_0:2;
then IC (Computation sISA0,n) = IC (Computation (sISA0 +* (I ';' I)),n) by A1, A4, A6, Th18, AMI_1:121;
then A19: IC (Computation (sISA0 +* (I ';' I)),n) in dom I by A4, Def1;
then A20: IC (Computation (sISA0 +* (Directed I)),n) in dom (Directed I) by A18, FUNCT_4:105;
A21: CurInstr (Computation (sISA0 +* (Directed I)),n) = (sISA0 +* (Directed I)) . (IC (Computation (sISA0 +* (Directed I)),n)) by AMI_1:54
.= (Directed I) . (IC (Computation (sISA0 +* (Directed I)),n)) by A20, FUNCT_4:14 ;
CurInstr (Computation (sISA0 +* (I ';' I)),n) = (sISA0 +* (I ';' I)) . (IC (Computation (sISA0 +* (I ';' I)),n)) by AMI_1:54
.= (I ';' I) . (IC (Computation (sISA0 +* (I ';' I)),n)) by A12, A19, FUNCT_4:14
.= (Directed I) . (IC (Computation (sISA0 +* (I ';' I)),n)) by A11, A18, A20, GRFUNC_1:8 ;
hence Computation (sISA0 +* (I ';' I)),(n + 1), Computation (sISA0 +* (Directed I)),(n + 1) equal_outside NAT by A13, A17, A16, A18, A21, A15, A14, SCMFSA6A:32, XXREAL_0:2; :: thesis:

end;

( Computation (sISA0 +* (I ';' I)),0 = sISA0 +* (I ';' I) & Computation (sISA0 +* (Directed I)),0 = sISA0 +* (Directed I) ) by AMI_1:13;
then Computation (sISA0 +* (Directed I)),0 , Computation (sISA0 +* (I ';' I)),0 equal_outside NAT by FUNCT_7:107, SCMFSA6A:42;
then A22: S₁[ 0 ] by FUNCT_7:28;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A22, A10);
then A23: Computation (sISA0 +* (I ';' I)),k, Computation (sISA0 +* (Directed I)),k equal_outside NAT ;
Computation sISA0,k, Computation (sISA0 +* (I ';' I)),k equal_outside NAT by A1, A4, A6, A9, Th18;
hence Computation sISA0,k, Computation (sISA0 +* (Directed I)),k equal_outside NAT by A23, FUNCT_7:29; :: thesis:

end;

then A24: IC (Computation sISA0,(LifeSpan sISA0)) = IC (Computation (sISA0 +* (Directed I)),(LifeSpan sISA0)) by AMI_1:121;
I +* (Start-At (insloc 0 )) c= Initialized I by Th6;
then I +* (Start-At (insloc 0 )) c= sISA0 by A4, XBOOLE_1:1;
then sISA0 . (IC (Computation sISA0,(LifeSpan sISA0))) = (I +* (Start-At (insloc 0 ))) . (IC (Computation sISA0,(LifeSpan sISA0))) by A7, A5, GRFUNC_1:8;
then A25: I . (IC (Computation sISA0,(LifeSpan sISA0))) = sISA0 . (IC (Computation sISA0,(LifeSpan sISA0))) by A7, SCMFSA6B:7
.= CurInstr (Computation sISA0,(LifeSpan sISA0)) by AMI_1:54
.= halt SCM+FSA by A1, A6, AMI_1:def 46 ;
IC (Computation (sISA0 +* (Directed I)),(LifeSpan sISA0)) in dom I by A8, A7, AMI_1:121;
then IC (Computation (sISA0 +* (Directed I)),(LifeSpan sISA0)) in dom (Directed I) by FUNCT_4:105;
then A26: (sISA0 +* (Directed I)) . (IC (Computation sISA0,(LifeSpan sISA0))) = (Directed I) . (IC (Computation sISA0,(LifeSpan sISA0))) by A24, FUNCT_4:14
.= goto (insloc (card I)) by A7, A25, FUNCT_4:112 ;
Computation (sISA0 +* (Directed I)),((LifeSpan sISA0) + 1) = Following (Computation (sISA0 +* (Directed I)),(LifeSpan sISA0)) by AMI_1:14
.= Exec (goto (insloc (card I))),(Computation (sISA0 +* (Directed I)),(LifeSpan sISA0)) by A24, A26, AMI_1:54 ;
then A27: ( ( for a being Int-Location holds (Computation (sISA0 +* (Directed I)),((LifeSpan sISA0) + 1)) . a = (Computation (sISA0 +* (Directed I)),(LifeSpan sISA0)) . a ) & ( for f being FinSeq-Location holds (Computation (sISA0 +* (Directed I)),((LifeSpan sISA0) + 1)) . f = (Computation (sISA0 +* (Directed I)),(LifeSpan sISA0)) . f ) ) by SCMFSA_2:95;
sISA0 +* (Directed I) = s +* (Directed I) by A3, Th20
.= s by A2, FUNCT_4:79 ;
hence DataPart (Computation s,(LifeSpan (s +* I))) = DataPart (Computation s,((LifeSpan (s +* I)) + 1)) by A6, A27, SCMFSA6A:38; :: thesis: