let s be 0 -started State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA
for I being paraclosed Program of st P +* I halts_on s & Directed I c= P holds
DataPart (Comput (P,s,(LifeSpan ((P +* I),s)))) = DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1)))
let P be Instruction-Sequence of SCM+FSA; :: thesis: for I being paraclosed Program of st P +* I halts_on s & Directed I c= P holds
DataPart (Comput (P,s,(LifeSpan ((P +* I),s)))) = DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1)))
let I be paraclosed Program of ; :: thesis: ( P +* I halts_on s & Directed I c= P implies DataPart (Comput (P,s,(LifeSpan ((P +* I),s)))) = DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) )
assume that
A1: P +* I halts_on s and
A3: Directed I c= P ; :: thesis: DataPart (Comput (P,s,(LifeSpan ((P +* I),s)))) = DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1)))
A6: I c= P +* I by FUNCT_4:25;
set m = LifeSpan ((P +* I),s);
set l1 = IC (Comput ((P +* I),s,(LifeSpan ((P +* I),s))));
A12: IC (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) in dom I by A6, AMISTD_1:def 10;

now

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

proof

A16: Directed I c= I ';' I by SCMFSA6A:16;
let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
A17: dom I c= dom (I ';' I) by SCMFSA6A:17;
assume A18: ( n <= k implies Comput (((P +* I) +* (I ';' I)),s,n) = Comput (P,s,n) ) ; :: thesis: S₁[n + 1]
A19: Comput (P,s,(n + 1)) = Following (P,(Comput (P,s,n))) by EXTPRO_1:3
.= Exec ((CurInstr (P,(Comput (P,s,n)))),(Comput (P,s,n))) ;
A20: Comput (((P +* I) +* (I ';' I)),s,(n + 1)) = Following (((P +* I) +* (I ';' I)),(Comput (((P +* I) +* (I ';' I)),s,n))) by EXTPRO_1:3
.= Exec ((CurInstr (((P +* I) +* (I ';' I)),(Comput (((P +* I) +* (I ';' I)),s,n)))),(Comput (((P +* I) +* (I ';' I)),s,n))) ;
A21: n <= n + 1 by NAT_1:12;
assume A22: n + 1 <= k ; :: thesis: Comput (((P +* I) +* (I ';' I)),s,(n + 1)) = Comput (P,s,(n + 1))
n <= k by A22, A21, XXREAL_0:2;
then Comput ((P +* I),s,n) = Comput (((P +* I) +* (I ';' I)),s,n) by Th36, A14, A6, A1, XXREAL_0:2;
then A24: IC (Comput (((P +* I) +* (I ';' I)),s,n)) in dom I by A6, AMISTD_1:def 10;
then A25: IC (Comput (P,s,n)) in dom (Directed I) by A22, A18, A21, FUNCT_4:99, XXREAL_0:2;
A26: dom P = NAT by PARTFUN1:def 2;
A27: CurInstr (P,(Comput (P,s,n))) = P . (IC (Comput (P,s,n))) by A26, PARTFUN1:def 6
.= (Directed I) . (IC (Comput (P,s,n))) by A25, A3, GRFUNC_1:2 ;
A28: dom ((P +* I) +* (I ';' I)) = NAT by PARTFUN1:def 2;
CurInstr (((P +* I) +* (I ';' I)),(Comput (((P +* I) +* (I ';' I)),s,n))) = ((P +* I) +* (I ';' I)) . (IC (Comput (((P +* I) +* (I ';' I)),s,n))) by A28, PARTFUN1:def 6
.= (I ';' I) . (IC (Comput (((P +* I) +* (I ';' I)),s,n))) by A17, A24, FUNCT_4:13
.= (Directed I) . (IC (Comput (((P +* I) +* (I ';' I)),s,n))) by A16, A22, A25, A18, A21, GRFUNC_1:2, XXREAL_0:2 ;
hence Comput (((P +* I) +* (I ';' I)),s,(n + 1)) = Comput (P,s,(n + 1)) by A18, A22, A21, A27, A20, A19, XXREAL_0:2; :: thesis: verum

end;

( Comput (((P +* I) +* (I ';' I)),s,0) = s & Comput (P,s,0) = s ) by EXTPRO_1:2;
then A29: S₁[ 0 ] ;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A29, A15);
then Comput (((P +* I) +* (I ';' I)),s,k) = Comput (P,s,k) ;
hence Comput ((P +* I),s,k) = Comput (P,s,k) by A14, A1, Th36, FUNCT_4:25; :: thesis: verum

end;

then B31: Comput ((P +* I),s,(LifeSpan ((P +* I),s))) = Comput (P,s,(LifeSpan ((P +* I),s))) ;
A32: dom (P +* I) = NAT by PARTFUN1:def 2;
I c= P +* I by FUNCT_4:25;
then A33: I . (IC (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) = (P +* I) . (IC (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) by A12, GRFUNC_1:2
.= CurInstr ((P +* I),(Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) by A32, PARTFUN1:def 6
.= halt SCM+FSA by A1, EXTPRO_1:def 15 ;
IC (Comput (P,s,(LifeSpan ((P +* I),s)))) in dom (Directed I) by A12, B31, FUNCT_4:99;
then A34: P . (IC (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) = (Directed I) . (IC (Comput ((P +* I),s,(LifeSpan ((P +* I),s))))) by B31, A3, GRFUNC_1:2
.= goto (card I) by A12, A33, FUNCT_4:106 ;
A35: dom P = NAT by PARTFUN1:def 2;
Comput (P,s,((LifeSpan ((P +* I),s)) + 1)) = Following (P,(Comput (P,s,(LifeSpan ((P +* I),s))))) by EXTPRO_1:3
.= Exec ((goto (card I)),(Comput (P,s,(LifeSpan ((P +* I),s))))) by B31, A34, A35, PARTFUN1:def 6 ;
then ( ( for a being Int-Location holds (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) . a = (Comput (P,s,(LifeSpan ((P +* I),s)))) . a ) & ( for f being FinSeq-Location holds (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) . f = (Comput (P,s,(LifeSpan ((P +* I),s)))) . f ) ) by SCMFSA_2:69;
hence DataPart (Comput (P,s,(LifeSpan ((P +* I),s)))) = DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) by SCMFSA6A:7; :: thesis: verum