let P be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for I being Program of SCM+FSA st Directed I is_pseudo-closed_on s,P holds
( I ";" (Stop SCM+FSA) is_halting_on s,P & LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s)) = pseudo-LifeSpan (s,P,(Directed I)) & ( for n being 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)) ) & ( for n being Nat st n <= pseudo-LifeSpan (s,P,(Directed I)) holds
DataPart (Comput ((P +* I),(Initialize s),n)) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) ) )
let s be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA st Directed I is_pseudo-closed_on s,P holds
( I ";" (Stop SCM+FSA) is_halting_on s,P & LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s)) = pseudo-LifeSpan (s,P,(Directed I)) & ( for n being 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)) ) & ( for n being Nat st n <= pseudo-LifeSpan (s,P,(Directed I)) holds
DataPart (Comput ((P +* I),(Initialize s),n)) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) ) )
set D = Data-Locations ;
let I be Program of SCM+FSA; :: thesis: ( Directed I is_pseudo-closed_on s,P implies ( I ";" (Stop SCM+FSA) is_halting_on s,P & LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s)) = pseudo-LifeSpan (s,P,(Directed I)) & ( for n being 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)) ) & ( for n being Nat st n <= pseudo-LifeSpan (s,P,(Directed I)) holds
DataPart (Comput ((P +* I),(Initialize s),n)) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) ) ) )
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 by ORDINAL1:def 12;
(Stop SCM+FSA) . 0 = halt SCM+FSA ;
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: ( I ";" (Stop SCM+FSA) is_halting_on s,P & LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s)) = pseudo-LifeSpan (s,P,(Directed I)) & ( for n being 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)) ) & ( for n being Nat st n <= pseudo-LifeSpan (s,P,(Directed I)) holds
DataPart (Comput ((P +* I),(Initialize s),n)) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) ) )
then A4: Directed I is_pseudo-closed_on Initialize s,P +* (Directed I) ;
defpred S1[ 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;
A8: 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 A9: Reloc ((Directed I),0) c= P +* (I ";" (Stop SCM+FSA)) by A6, XBOOLE_1:1;
A10: IC (Initialize s) = 0 by FUNCT_4:113;
A11: Directed I c= P +* (Directed I) by FUNCT_4:25;
A12: now :: thesis: for n being Nat st n <= pseudo-LifeSpan ((Initialize s),(P +* (Directed I)),(Directed I)) holds
( IC (Comput ((P +* (Directed I)),(Initialize s),n)) = IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) & DataPart (Comput ((P +* (Directed I)),(Initialize s),n)) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) )
let n be Nat; :: thesis: ( n <= pseudo-LifeSpan ((Initialize s),(P +* (Directed I)),(Directed I)) implies ( IC (Comput ((P +* (Directed I)),(Initialize s),n)) = IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) & DataPart (Comput ((P +* (Directed I)),(Initialize s),n)) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) ) )
assume A13: n <= pseudo-LifeSpan ((Initialize s),(P +* (Directed I)),(Directed I)) ; :: thesis: ( IC (Comput ((P +* (Directed I)),(Initialize s),n)) = IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) & DataPart (Comput ((P +* (Directed I)),(Initialize s),n)) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) )
then (IC (Comput ((P +* (Directed I)),(Initialize s),n))) + 0 = IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) by A4, A9, A10, A2, Th14, A11;
hence IC (Comput ((P +* (Directed I)),(Initialize s),n)) = IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) ; :: thesis: DataPart (Comput ((P +* (Directed I)),(Initialize s),n)) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n))
thus DataPart (Comput ((P +* (Directed I)),(Initialize s),n)) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) by A4, A9, A10, A2, A13, Th14, A11; :: thesis: verum
end;
A14: k = pseudo-LifeSpan (s,P,(Directed I)) by A3, Th13;
A15: now :: thesis: for n being Nat st n < pseudo-LifeSpan ((Initialize s),(P +* (Directed I)),(Directed I)) holds
( 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))) & IC (Comput ((P +* (Directed I)),(Initialize s),n)) in dom (Directed I) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),n))) <> halt SCM+FSA )
let n be Nat; :: thesis: ( n < pseudo-LifeSpan ((Initialize s),(P +* (Directed I)),(Directed I)) implies ( 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))) & IC (Comput ((P +* (Directed I)),(Initialize s),n)) in dom (Directed I) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),n))) <> halt SCM+FSA ) )
assume A16: n < pseudo-LifeSpan ((Initialize s),(P +* (Directed I)),(Directed I)) ; :: thesis: ( 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))) & IC (Comput ((P +* (Directed I)),(Initialize s),n)) in dom (Directed I) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),n))) <> halt SCM+FSA )
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, A9, A10, A2, Th14, A11;
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: ( IC (Comput ((P +* (Directed I)),(Initialize s),n)) in dom (Directed I) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),n))) <> halt SCM+FSA )
thus IC (Comput ((P +* (Directed I)),(Initialize s),n)) in dom (Directed I) by A4, A16, SCMFSA8A:17; :: thesis: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),n))) <> halt SCM+FSA
thus CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),n))) <> halt SCM+FSA by A4, A16, SCMFSA8A:17; :: thesis: verum
end;
A17: now :: thesis: for n being Nat st CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n))) = halt SCM+FSA holds
not k > n
let n be Nat; :: thesis: ( CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n))) = halt SCM+FSA implies not k > n )
assume A18: CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n))) = halt SCM+FSA ; :: thesis: not k > n
reconsider l = IC (Comput ((P +* (Directed I)),(Initialize s),n)) as Element of NAT ;
assume A19: k > n ; :: thesis: contradiction
then A20: l in dom (Directed I) by A3, A14, 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 A15, A19
.= (P +* (Directed I)) . l by PBOOLE:143
.= (Directed I) . l by A20, A11, GRFUNC_1:2 ;
then halt SCM+FSA in rng (Directed I) by A18, A20, FUNCT_1:def 3;
hence contradiction by COMPOS_1:def 11; :: thesis: verum
end;
A21: card (Stop SCM+FSA) = 1 by AFINSQ_1:34;
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 A22: card I in dom (I ";" (Stop SCM+FSA)) by AFINSQ_1:66;
card I < (card I) + (card (Stop SCM+FSA)) by A21, NAT_1:13;
then A23: (I ";" (Stop SCM+FSA)) . (card I) = IncAddr ((halt SCM+FSA),(card I)) by A1, Th2
.= halt SCM+FSA by COMPOS_0:4 ;
then A24: (P +* (I ";" (Stop SCM+FSA))) . (card I) = halt SCM+FSA by A22, A5, GRFUNC_1:2;
A25: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A26: S1[n] ; :: thesis: S1[n + 1]
assume A27: k <= n + 1 ; :: thesis: ( IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),(n + 1))) = card I & CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),(n + 1)))) = halt SCM+FSA )
hereby :: thesis: CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),(n + 1)))) = halt SCM+FSA
per cases ( k = n + 1 or k <= n ) by A27, NAT_1:8;
suppose k = n + 1 ; :: thesis: IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),(n + 1))) = card I
hence IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),(n + 1))) = IC (Comput ((P +* (Directed I)),(Initialize s),k)) by A12
.= card (Directed I) by A3, A14, SCMFSA8A:def 4
.= card I by SCMFSA6A:36 ;
:: thesis: verum
end;
suppose A28: k <= n ; :: thesis: IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),(n + 1))) = card I
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 A26, A28, EXTPRO_1:def 3; :: thesis: verum
end;
end;
end;
hence CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),(n + 1)))) = halt SCM+FSA by A24, PBOOLE:143; :: thesis: verum
end;
A29: S1[ 0 ]
proof
assume k <= 0 ; :: thesis: ( IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),0)) = card I & CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),0))) = halt SCM+FSA )
then k = 0 ;
hence IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),0)) = IC (Comput ((P +* (Directed I)),(Initialize s),k))
.= card (Directed I) by A3, A14, SCMFSA8A:def 4
.= card I by SCMFSA6A:36 ;
:: thesis: CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),0))) = halt SCM+FSA
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 A23, A22, A5, GRFUNC_1:2 ;
:: thesis: verum
end;
A30: for n being Nat holds S1[n] from NAT_1:sch 2(A29, A25);
 set s1 = Initialize s;
set P1 = P +* I;
A31: I c= P +* I by FUNCT_4:25;
A32: card (Directed I) = card I by SCMFSA6A:36;
S1[k] by A30;
then A33: P +* (I ";" (Stop SCM+FSA)) halts_on Initialize s by EXTPRO_1:29;
hence I ";" (Stop SCM+FSA) is_halting_on s,P ; :: thesis: ( LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s)) = pseudo-LifeSpan (s,P,(Directed I)) & ( for n being 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)) ) & ( for n being Nat st n <= pseudo-LifeSpan (s,P,(Directed I)) holds
DataPart (Comput ((P +* I),(Initialize s),n)) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) ) )
CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),k))) = halt SCM+FSA by A30;
then A34: LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s)) = k by A33, A17, EXTPRO_1:def 15;
defpred S2[ 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)) ) );
A35: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
set l = IC (Comput ((P +* I),(Initialize s),n));
set l0 = IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n));
assume A36: S2[n] ; :: thesis: S2[n + 1]
assume A37: n + 1 < pseudo-LifeSpan (s,P,(Directed I)) ; :: thesis: ( IC (Comput ((P +* I),(Initialize s),(n + 1))) in dom I & IC (Comput ((P +* I),(Initialize s),(n + 1))) = IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),(n + 1))) & DataPart (Comput ((P +* I),(Initialize s),(n + 1))) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),(n + 1))) )
then A38: IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) in dom (Directed I) by A36, FUNCT_4:99, NAT_1:12;
A39: for f being FinSeq-Location holds (Comput ((P +* I),(Initialize s),n)) . f = (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) . f by A36, A37, 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 A36, A37, NAT_1:12, SCMFSA_M:2;
then A40: Comput ((P +* I),(Initialize s),n) = Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n) by A36, A37, A39, NAT_1:12, SCMFSA_2:61;
A41: now :: thesis: not I . (IC (Comput ((P +* I),(Initialize s),n))) = halt SCM+FSA
assume A42: I . (IC (Comput ((P +* I),(Initialize s),n))) = halt SCM+FSA ; :: thesis: contradiction
A43: (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 A14, A37, NAT_1:12;
then A44: 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 A12, A43
.= (Directed I) . (IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n))) by A38, A11, GRFUNC_1:2
.= goto (card I) by A36, A37, A42, NAT_1:12, SCMFSA8A:16 ;
A45: 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 A44, SCMFSA_2:69
.= card (Directed I) by SCMFSA6A:36 ;
IC (Comput ((P +* (Directed I)),(Initialize s),(n + 1))) in dom (Directed I) by A3, A37, SCMFSA8A:17;
hence contradiction by A45; :: thesis: verum
end;
A46: 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 A31, A36, A37, GRFUNC_1:2, NAT_1:12
.= (Directed I) . (IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n))) by A36, A37, A41, NAT_1:12, SCMFSA8A:16
.= (P +* (I ";" (Stop SCM+FSA))) . (IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n))) by A38, A8, GRFUNC_1:2
.= CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n))) by PBOOLE:143 ;
A47: 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 A46 ;
pseudo-LifeSpan (s,P,(Directed I)) = k by A3, Th13;
then A48: IC (Comput ((P +* (Directed I)),(Initialize s),(n + 1))) = IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),(n + 1))) by A12, A37;
A49: 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 A50: Comput ((P +* I),(Initialize s),(n + 1)) = Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),(n + 1)) by A47, A40;
A51: 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 A50;
IC (Comput ((P +* (Directed I)),(Initialize s),(n + 1))) in dom (Directed I) by A3, A37, SCMFSA8A:17;
hence IC (Comput ((P +* I),(Initialize s),(n + 1))) in dom I by A48, A49, A50; :: thesis: ( IC (Comput ((P +* I),(Initialize s),(n + 1))) = IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),(n + 1))) & DataPart (Comput ((P +* I),(Initialize s),(n + 1))) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),(n + 1))) )
thus IC (Comput ((P +* I),(Initialize s),(n + 1))) = IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),(n + 1))) by A50; :: thesis: DataPart (Comput ((P +* I),(Initialize s),(n + 1))) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),(n + 1)))
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 A50;
hence DataPart (Comput ((P +* I),(Initialize s),(n + 1))) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),(n + 1))) by A51, SCMFSA_M:2; :: thesis: verum
end;
IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),k)) = card I by A30;
then A52: IC (Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s))))) = card I by A12, A34;
for n being 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 A15, A34;
hence LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s)) = pseudo-LifeSpan (s,P,(Directed I)) by A3, A52, A32, SCMFSA8A:def 4; :: thesis: ( ( for n being 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)) ) & ( for n being Nat st n <= pseudo-LifeSpan (s,P,(Directed I)) holds
DataPart (Comput ((P +* I),(Initialize s),n)) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) ) )
A53: S2[ 0 ]
proof
A54: 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: ( IC (Comput ((P +* I),(Initialize s),0)) in dom I & IC (Comput ((P +* I),(Initialize s),0)) = IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),0)) & DataPart (Comput ((P +* I),(Initialize s),0)) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),0)) )
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 A54, FUNCT_4:99; :: thesis: ( IC (Comput ((P +* I),(Initialize s),0)) = IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),0)) & DataPart (Comput ((P +* I),(Initialize s),0)) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),0)) )
thus IC (Comput ((P +* I),(Initialize s),0)) = IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),0)) ; :: thesis: DataPart (Comput ((P +* I),(Initialize s),0)) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),0))
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: verum
end;
A55: for n being Nat holds S2[n] from NAT_1:sch 2(A53, A35);
 hence for n being 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: for n being Nat st n <= pseudo-LifeSpan (s,P,(Directed I)) holds
DataPart (Comput ((P +* I),(Initialize s),n)) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n))
let n be Nat; :: thesis: ( n <= pseudo-LifeSpan (s,P,(Directed I)) implies DataPart (Comput ((P +* I),(Initialize s),n)) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) )
assume A56: n <= pseudo-LifeSpan (s,P,(Directed I)) ; :: thesis: DataPart (Comput ((P +* I),(Initialize s),n)) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n))
per cases ( n < pseudo-LifeSpan (s,P,(Directed I)) or n = pseudo-LifeSpan (s,P,(Directed I)) ) by A56, XXREAL_0:1;
suppose n < pseudo-LifeSpan (s,P,(Directed I)) ; :: thesis: DataPart (Comput ((P +* I),(Initialize s),n)) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n))
hence DataPart (Comput ((P +* I),(Initialize s),n)) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) by A55; :: thesis: verum
end;
suppose A57: n = pseudo-LifeSpan (s,P,(Directed I)) ; :: thesis: DataPart (Comput ((P +* I),(Initialize s),n)) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n))
per cases ( n = 0 or ex m being Nat st n = m + 1 ) by NAT_1:6;
suppose ex m being Nat st n = m + 1 ; :: thesis: DataPart (Comput ((P +* I),(Initialize s),n)) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n))
then consider m being Nat such that
A59: n = m + 1 ;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
A60: 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 A59, EXTPRO_1:3;
set i = CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),m)));
A61: Comput ((P +* I),(Initialize s),n) = Following ((P +* I),(Comput ((P +* I),(Initialize s),m))) by A59, EXTPRO_1:3;
set l0 = IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),m));
set l = IC (Comput ((P +* I),(Initialize s),m));
A62: m + 0 < pseudo-LifeSpan (s,P,(Directed I)) by A57, A59, XREAL_1:6;
then A63: IC (Comput ((P +* I),(Initialize s),m)) = IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),m)) by A55;
A64: IC (Comput ((P +* I),(Initialize s),m)) in dom I by A55, A62;
then A65: IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),m)) in dom (Directed I) by A63, FUNCT_4:99;
A66: 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 A31, A64, GRFUNC_1:2 ;
A67: Directed I c= I ";" (Stop SCM+FSA) by SCMFSA6A:16;
then A68: dom (Directed I) c= dom (I ";" (Stop SCM+FSA)) by RELAT_1:11;
A69: (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 A65, A67, GRFUNC_1:2
.= (P +* (I ";" (Stop SCM+FSA))) . (IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),m))) by A5, A68, A65, GRFUNC_1:2
.= CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),m))) by PBOOLE:143 ;
A70: DataPart (Comput ((P +* I),(Initialize s),m)) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),m)) by A55, A62;
per cases ( CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),m))) = halt SCM+FSA or CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),m))) <> halt SCM+FSA ) ;
suppose A71: CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),m))) = halt SCM+FSA ; :: thesis: DataPart (Comput ((P +* I),(Initialize s),n)) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n))
then CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),m))) = goto (card I) by A64, A63, A66, A69, 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 A72: 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 A61, A71, EXTPRO_1:def 3
.= DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),m)) by A55, A62
.= DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) by A60, A72, Th6 ; :: thesis: verum
end;
suppose CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),m))) <> halt SCM+FSA ; :: thesis: DataPart (Comput ((P +* I),(Initialize s),n)) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n))
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 A64, A63, A66, A69, SCMFSA8A:16;
hence DataPart (Comput ((P +* I),(Initialize s),n)) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) by A61, A60, A70, SCMFSA6C:4; :: thesis: verum
end;
end;
end;
end;
end;
end;