let P be Instruction-Sequence of SCM+FSA; :: thesis:
let s be State of SCM+FSA; :: thesis:
set D = Data-Locations ;
let I be Program of SCM+FSA; :: thesis:
set I0 = Directed I;
set I1 = I ";" (Stop SCM+FSA);
set s00 = Initialize s;
set P00 = P +* (Directed I);
set s10 = Initialize s;
set P10 = P +* (I ";" (Stop SCM+FSA));
reconsider k = pseudo-LifeSpan ((Initialize s),(P +* (Directed I)),(Directed I)) as Element of NAT ;
(Stop SCM+FSA) . 0 = halt SCM+FSA by AFINSQ_1:34;
then A1: halt SCM+FSA = (Stop SCM+FSA) . ((card I) -' (card I)) by XREAL_1:232;
A2: DataPart (Initialize s) = DataPart (Initialize s) ;
assume A3: Directed I is_pseudo-closed_on s,P ; :: thesis:
then A4: Directed I is_pseudo-closed_on Initialize s,P +* (Directed I) by Th21;
defpred S₁[ Nat] means ( k <= $1 implies ( IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),$1)) = card I & CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),$1))) = halt SCM+FSA ) );
A5: I ";" (Stop SCM+FSA) c= P +* (I ";" (Stop SCM+FSA)) by FUNCT_4:25;
A6: I ";" (Stop SCM+FSA) c= P +* (I ";" (Stop SCM+FSA)) by FUNCT_4:25;
A7: Directed I c= I ";" (Stop SCM+FSA) by SCMFSA6A:16;
then A8: dom (Directed I) c= dom (I ";" (Stop SCM+FSA)) by GRFUNC_1:2;
A9: Directed I c= P +* (I ";" (Stop SCM+FSA)) by A7, A5, XBOOLE_1:1;
Reloc ((Directed I),0) c= I ";" (Stop SCM+FSA) by A7;
then A10: Reloc ((Directed I),0) c= P +* (I ";" (Stop SCM+FSA)) by A6, XBOOLE_1:1;
A11: IC (Initialize s) = 0 by FUNCT_4:113;
A12: Directed I c= P +* (Directed I) by FUNCT_4:25;

A13: now :: thesis:

let n be Element of NAT ; :: thesis:
assume A14: n <= pseudo-LifeSpan ((Initialize s),(P +* (Directed I)),(Directed I)) ; :: thesis:
then (IC (Comput ((P +* (Directed I)),(Initialize s),n))) + 0 = IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) by A4, A10, A11, A2, Th22, A12;
hence IC (Comput ((P +* (Directed I)),(Initialize s),n)) = IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) ; :: thesis:
thus DataPart (Comput ((P +* (Directed I)),(Initialize s),n)) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) by A4, A10, A11, A2, A14, Th22, A12; :: thesis:

end;

A15: k = pseudo-LifeSpan (s,P,(Directed I)) by A3, Th21;
A16: Initialize (Initialize s) = Initialize s ;
A17: (P +* (Directed I)) +* (Directed I) = P +* ((Directed I) +* (Directed I))
.= P +* (Directed I) ;

A18: now :: thesis:

let n be Element of NAT ; :: thesis:
assume A19: n < pseudo-LifeSpan ((Initialize s),(P +* (Directed I)),(Directed I)) ; :: thesis:
then IncAddr ((CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),n)))),0) = CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n))) by A4, A10, A11, A2, Th22, A12;
hence CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),n))) = CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n))) by COMPOS_0:3; :: thesis:
thus IC (Comput ((P +* (Directed I)),(Initialize s),n)) in dom (Directed I) by A16, A4, A19, A17, SCMFSA8A:17; :: thesis:
thus CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),n))) <> halt SCM+FSA by A16, A4, A19, A17, SCMFSA8A:17; :: thesis:

end;

A20: now :: thesis:

let n be Element of NAT ; :: thesis:
assume A21: CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n))) = halt SCM+FSA ; :: thesis:
reconsider l = IC (Comput ((P +* (Directed I)),(Initialize s),n)) as Element of NAT ;
assume A22: k > n ; :: thesis:
then A23: l in dom (Directed I) by A3, A15, SCMFSA8A:def 4;
CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n))) = CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),n))) by A18, A22
.= (P +* (Directed I)) . l by PBOOLE:143
.= (Directed I) . l by A23, A12, GRFUNC_1:2 ;
then halt SCM+FSA in rng (Directed I) by A21, A23, FUNCT_1:def 3;
hence contradiction by COMPOS_1:def 11; :: thesis:

end;

A24: card (Stop SCM+FSA) = 1 by AFINSQ_1:33;
then card (I ";" (Stop SCM+FSA)) = (card I) + 1 by SCMFSA6A:21;
then card I < card (I ";" (Stop SCM+FSA)) by NAT_1:13;
then A25: card I in dom (I ";" (Stop SCM+FSA)) by AFINSQ_1:66;
card I < (card I) + (card (Stop SCM+FSA)) by A24, NAT_1:13;
then A26: (I ";" (Stop SCM+FSA)) . (card I) = IncAddr ((halt SCM+FSA),(card I)) by A1, Th2
.= halt SCM+FSA by COMPOS_0:4 ;
then A27: (P +* (I ";" (Stop SCM+FSA))) . (card I) = halt SCM+FSA by A25, A5, GRFUNC_1:2;
A28: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis:
assume A29: S₁[n] ; :: thesis:
assume A30: k <= n + 1 ; :: thesis:

hereby :: thesis:

per cases by A30, NAT_1:8;

suppose k = n + 1 ; :: thesis:

hence IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),(n + 1))) = IC (Comput ((P +* (Directed I)),(Initialize s),k)) by A13
.= card (Directed I) by A3, A15, SCMFSA8A:def 4
.= card I by SCMFSA8A:20 ;
:: thesis:

end;

suppose A31: k <= n ; :: thesis:

Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),(n + 1)) = Following ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n))) by EXTPRO_1:3;
hence IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),(n + 1))) = card I by A29, A31, EXTPRO_1:def 3; :: thesis:

end;

end;

end;

hence CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),(n + 1)))) = halt SCM+FSA by A27, PBOOLE:143; :: thesis:

end;

A32: S₁[ 0 ]

proof

assume k <= 0 ; :: thesis:
then k = 0 ;
hence IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),0)) = IC (Comput ((P +* (Directed I)),(Initialize s),k)) by A13
.= card (Directed I) by A3, A15, SCMFSA8A:def 4
.= card I by SCMFSA8A:20 ;
:: thesis:
hence CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),0))) = (P +* (I ";" (Stop SCM+FSA))) . (card I) by PBOOLE:143
.= halt SCM+FSA by A26, A25, A5, GRFUNC_1:2 ;
:: thesis:

end;

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

now :: thesis:

let n be Element of NAT ; :: thesis:

per cases ;

suppose A34: n < k ; :: thesis:

then IC (Comput ((P +* (Directed I)),(Initialize s),n)) = IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) by A13;
then IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) in dom (Directed I) by A3, A15, A34, SCMFSA8A:def 4;
hence IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) in dom (I ";" (Stop SCM+FSA)) by A8; :: thesis:

end;

suppose k <= n ; :: thesis:

hence IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) in dom (I ";" (Stop SCM+FSA)) by A25, A33; :: thesis:

end;

end;

end;

hence I ";" (Stop SCM+FSA) is_closed_on s,P by SCMFSA7B:def 6; :: thesis:
set s1 = Initialize s;
set P1 = P +* I;
A35: I c= P +* I by FUNCT_4:25;
A36: card (Directed I) = card I by SCMFSA8A:20;
S₁[k] by A33;
then A37: P +* (I ";" (Stop SCM+FSA)) halts_on Initialize s by EXTPRO_1:29;
hence I ";" (Stop SCM+FSA) is_halting_on s,P by SCMFSA7B:def 7; :: thesis:
CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),k))) = halt SCM+FSA by A33;
then A38: LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s)) = k by A37, A20, EXTPRO_1:def 15;
defpred S₂[ Nat] means ( $1 < pseudo-LifeSpan (s,P,(Directed I)) implies ( IC (Comput ((P +* I),(Initialize s),$1)) in dom I & IC (Comput ((P +* I),(Initialize s),$1)) = IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),$1)) & DataPart (Comput ((P +* I),(Initialize s),$1)) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),$1)) ) );
A39: for n being Element of NAT st S₂[n] holds
S₂[n + 1]

proof

let n be Element of NAT ; :: thesis:
set l = IC (Comput ((P +* I),(Initialize s),n));
set l0 = IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n));
assume A40: S₂[n] ; :: thesis:
assume A41: n + 1 < pseudo-LifeSpan (s,P,(Directed I)) ; :: thesis:
then A42: IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) in dom (Directed I) by A40, FUNCT_4:99, NAT_1:12;
A43: for f being FinSeq-Location holds (Comput ((P +* I),(Initialize s),n)) . f = (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) . f by A40, A41, NAT_1:12, SCMFSA_M:2;
for a being Int-Location holds (Comput ((P +* I),(Initialize s),n)) . a = (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) . a by A40, A41, NAT_1:12, SCMFSA_M:2;
then A44: Comput ((P +* I),(Initialize s),n) = Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n) by A40, A41, A43, NAT_1:12, SCMFSA_2:61;

A45: now :: thesis:

assume A46: I . (IC (Comput ((P +* I),(Initialize s),n))) = halt SCM+FSA ; :: thesis:
A47: (P +* (Directed I)) /. (IC (Comput ((P +* (Directed I)),(Initialize s),n))) = (P +* (Directed I)) . (IC (Comput ((P +* (Directed I)),(Initialize s),n))) by PBOOLE:143;
n < k by A15, A41, NAT_1:12;
then A48: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),n))) = (P +* (Directed I)) . (IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n))) by A13, A47
.= (Directed I) . (IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n))) by A42, A12, GRFUNC_1:2
.= goto (card I) by A40, A41, A46, NAT_1:12, SCMFSA8A:16 ;
A49: IC (Comput ((P +* (Directed I)),(Initialize s),(n + 1))) = IC (Following ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),n)))) by EXTPRO_1:3
.= card I by A48, SCMFSA_2:69
.= card (Directed I) by SCMFSA8A:20 ;
IC (Comput ((P +* (Directed I)),(Initialize s),(n + 1))) in dom (Directed I) by A3, A41, SCMFSA8A:17;
hence contradiction by A49; :: thesis:

end;

A50: CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),n))) = (P +* I) . (IC (Comput ((P +* I),(Initialize s),n))) by PBOOLE:143
.= I . (IC (Comput ((P +* I),(Initialize s),n))) by A35, A40, A41, GRFUNC_1:2, NAT_1:12
.= (Directed I) . (IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n))) by A40, A41, A45, NAT_1:12, SCMFSA8A:16
.= (P +* (I ";" (Stop SCM+FSA))) . (IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n))) by A42, A9, GRFUNC_1:2
.= CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n))) by PBOOLE:143 ;
A51: Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),(n + 1)) = Following ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n))) by EXTPRO_1:3
.= Exec ((CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),n)))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n))) by A50 ;
pseudo-LifeSpan (s,P,(Directed I)) = k by A3, Th21;
then A52: IC (Comput ((P +* (Directed I)),(Initialize s),(n + 1))) = IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),(n + 1))) by A13, A41;
A53: dom (Directed I) = dom I by FUNCT_4:99;
Comput ((P +* I),(Initialize s),(n + 1)) = Following ((P +* I),(Comput ((P +* I),(Initialize s),n))) by EXTPRO_1:3;
then A54: Comput ((P +* I),(Initialize s),(n + 1)) = Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),(n + 1)) by A51, A44;
A55: for f being FinSeq-Location holds (Comput ((P +* I),(Initialize s),(n + 1))) . f = (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),(n + 1))) . f by A54;
IC (Comput ((P +* (Directed I)),(Initialize s),(n + 1))) in dom (Directed I) by A3, A41, SCMFSA8A:17;
hence IC (Comput ((P +* I),(Initialize s),(n + 1))) in dom I by A52, A53, A54; :: thesis:
thus IC (Comput ((P +* I),(Initialize s),(n + 1))) = IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),(n + 1))) by A54; :: thesis:
for a being Int-Location holds (Comput ((P +* I),(Initialize s),(n + 1))) . a = (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),(n + 1))) . a by A54;
hence DataPart (Comput ((P +* I),(Initialize s),(n + 1))) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),(n + 1))) by A55, SCMFSA_M:2; :: thesis:

end;

IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),k)) = card I by A33;
then A56: IC (Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s))))) = card I by A13, A38;
for n being Element of NAT st not IC (Comput ((P +* (Directed I)),(Initialize s),n)) in dom (Directed I) holds
LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s)) <= n by A18, A38;
hence LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s)) = pseudo-LifeSpan (s,P,(Directed I)) by A3, A56, A36, SCMFSA8A:def 4; :: thesis:
A57: S₂[ 0 ]

proof

A58: IC (Comput ((P +* I),(Initialize s),0)) = IC (Initialize s)
.= IC (Initialize s)
.= 0 by FUNCT_4:113 ;
assume 0 < pseudo-LifeSpan (s,P,(Directed I)) ; :: thesis:
then IC (Comput ((P +* (Directed I)),(Initialize s),0)) in dom (Directed I) by A3, SCMFSA8A:17;
then IC (Initialize s) in dom (Directed I) ;
then 0 in dom (Directed I) by MEMSTR_0:16;
hence IC (Comput ((P +* I),(Initialize s),0)) in dom I by A58, FUNCT_4:99; :: thesis:
thus IC (Comput ((P +* I),(Initialize s),0)) = IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),0)) ; :: thesis:
thus DataPart (Comput ((P +* I),(Initialize s),0)) = DataPart (Initialize s)
.= DataPart (Initialize s)
.= DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),0)) ; :: thesis:

end;

A59: for n being Element of NAT holds S₂[n] from NAT_1:sch 1(A57, A39);
hence for n being Element of NAT st n < pseudo-LifeSpan (s,P,(Directed I)) holds
IC (Comput ((P +* I),(Initialize s),n)) = IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) ; :: thesis:
let n be Element of NAT ; :: thesis:
assume A60: n <= pseudo-LifeSpan (s,P,(Directed I)) ; :: thesis:

per cases by A60, XXREAL_0:1;

suppose n < pseudo-LifeSpan (s,P,(Directed I)) ; :: thesis:

hence DataPart (Comput ((P +* I),(Initialize s),n)) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) by A59; :: thesis:

end;

suppose A61: n = pseudo-LifeSpan (s,P,(Directed I)) ; :: thesis:

per cases by NAT_1:6;

suppose A62: n = 0 ; :: thesis:

hence DataPart (Comput ((P +* I),(Initialize s),n)) = DataPart (Initialize s) by EXTPRO_1:2
.= DataPart (Initialize s)
.= DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) by A62, EXTPRO_1:2 ;
:: thesis:

end;

suppose ex m being Nat st n = m + 1 ; :: thesis:

then consider m being Nat such that
A63: n = m + 1 ;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
A64: Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n) = Following ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),m))) by A63, EXTPRO_1:3;
set i = CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),m)));
A65: Comput ((P +* I),(Initialize s),n) = Following ((P +* I),(Comput ((P +* I),(Initialize s),m))) by A63, EXTPRO_1:3;
set l0 = IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),m));
set l = IC (Comput ((P +* I),(Initialize s),m));
A66: m + 0 < pseudo-LifeSpan (s,P,(Directed I)) by A61, A63, XREAL_1:6;
then A67: IC (Comput ((P +* I),(Initialize s),m)) = IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),m)) by A59;
A68: IC (Comput ((P +* I),(Initialize s),m)) in dom I by A59, A66;
then A69: IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),m)) in dom (Directed I) by A67, FUNCT_4:99;
A70: CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),m))) = (P +* I) . (IC (Comput ((P +* I),(Initialize s),m))) by PBOOLE:143
.= I . (IC (Comput ((P +* I),(Initialize s),m))) by A35, A68, GRFUNC_1:2 ;
A71: Directed I c= I ";" (Stop SCM+FSA) by SCMFSA6A:16;
then A72: dom (Directed I) c= dom (I ";" (Stop SCM+FSA)) by RELAT_1:11;
A73: (Directed I) . (IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),m))) = (I ";" (Stop SCM+FSA)) . (IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),m))) by A69, A71, GRFUNC_1:2
.= (P +* (I ";" (Stop SCM+FSA))) . (IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),m))) by A5, A72, A69, GRFUNC_1:2
.= CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),m))) by PBOOLE:143 ;
A74: DataPart (Comput ((P +* I),(Initialize s),m)) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),m)) by A59, A66;

per cases ;

suppose A75: CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),m))) = halt SCM+FSA ; :: thesis:

then CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),m))) = goto (card I) by A68, A67, A70, A73, SCMFSA8A:16;
then InsCode (CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),m)))) = 6 by SCMFSA_2:23;
then A76: InsCode (CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),m)))) in {0,6,7,8} by ENUMSET1:def 2;
thus DataPart (Comput ((P +* I),(Initialize s),n)) = DataPart (Comput ((P +* I),(Initialize s),m)) by A65, A75, EXTPRO_1:def 3
.= DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),m)) by A59, A66
.= DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) by A64, A76, Th12 ; :: thesis:

end;

suppose CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),m))) <> halt SCM+FSA ; :: thesis:

then CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),m))) = CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),m))) by A68, A67, A70, A73, SCMFSA8A:16;
hence DataPart (Comput ((P +* I),(Initialize s),n)) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) by A65, A64, A74, SCMFSA6C:4; :: thesis:

end;

end;

end;

end;

end;

end;