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_closed_on s,P & 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 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)) ) & ( for n being Element of 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_closed_on s,P & 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 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)) ) & ( for n being Element of 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 ;
set A = NAT ;
let I be Program of SCM+FSA; :: thesis: ( Directed I is_pseudo-closed_on s,P implies ( I ';' (Stop SCM+FSA) is_closed_on s,P & 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 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)) ) & ( for n being Element of 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 ;
(Stop SCM+FSA) . 0 = halt SCM+FSA by AFINSQ_1:34;
then A5: halt SCM+FSA = (Stop SCM+FSA) . ((card I) -' (card I)) by XREAL_1:232;
A6: DataPart (Initialize s) = DataPart (Initialize s) ;
assume A7: Directed I is_pseudo-closed_on s,P ; :: thesis: ( I ';' (Stop SCM+FSA) is_closed_on s,P & 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 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)) ) & ( for n being Element of 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 A8: Directed I is_pseudo-closed_on Initialize s,P +* (Directed I) by Th50;
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 ) );
A10: I ';' (Stop SCM+FSA) c= P +* (I ';' (Stop SCM+FSA)) by FUNCT_4:25;
A11: I ';' (Stop SCM+FSA) c= P +* (I ';' (Stop SCM+FSA)) by FUNCT_4:25;
A12: Directed I c= I ';' (Stop SCM+FSA) by SCMFSA6A:16;
then A13: dom (Directed I) c= dom (I ';' (Stop SCM+FSA)) by GRFUNC_1:2;
A14: Directed I c= P +* (I ';' (Stop SCM+FSA)) by A12, A10, XBOOLE_1:1;
Reloc ((Directed I),0) c= I ';' (Stop SCM+FSA) by A12, COMPOS_1:45;
then A15: Reloc ((Directed I),0) c= P +* (I ';' (Stop SCM+FSA)) by A11, XBOOLE_1:1;
A16: IC (Initialize s) = 0 by FUNCT_4:113;
A18: Directed I c= P +* (Directed I) by FUNCT_4:25;
A19: now
let n be Element of 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 A20: 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 A8, A15, A16, A6, Th51, A18;
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 A8, A15, A16, A6, A20, Th51, A18; :: thesis: verum
end;
A21: k = pseudo-LifeSpan (s,P,(Directed I)) by A7, Th50;
A22: Initialize (Initialize s) = Initialize s ;
A23: (P +* (Directed I)) +* (Directed I) = P +* ((Directed I) +* (Directed I)) by FUNCT_4:14
.= P +* (Directed I) ;
A24: now
let n be Element of 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 A25: 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 A8, A15, A16, A6, Th51, A18;
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_1:10; :: 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 A22, A8, A25, A23, 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 A22, A8, A25, A23, SCMFSA8A:17; :: thesis: verum
end;
A26: now
let n be Element of 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 A27: 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 A29: k > n ; :: thesis: contradiction
then A30: l in dom (Directed I) by A7, A21, 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 A24, A29
.= (P +* (Directed I)) . l by PBOOLE:143
.= (Directed I) . l by A30, A18, GRFUNC_1:2 ;
then halt SCM+FSA in rng (Directed I) by A27, A30, FUNCT_1:def 3;
hence contradiction by COMPOS_1:def 3; :: thesis: verum
end;
A31: 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 A32: card I in dom (I ';' (Stop SCM+FSA)) by AFINSQ_1:66;
card I < (card I) + (card (Stop SCM+FSA)) by A31, NAT_1:13;
then B33: (I ';' (Stop SCM+FSA)) . (card I) = IncAddr ((halt SCM+FSA),(card I)) by A5, Th13
.= halt SCM+FSA by COMPOS_1:11 ;
then A33: (P +* (I ';' (Stop SCM+FSA))) . (card I) = halt SCM+FSA by A32, A10, GRFUNC_1:2;
A34: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; :: thesis: ( S1[n] implies S1[n + 1] )
assume A35: S1[n] ; :: thesis: S1[n + 1]
assume A37: 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 A37, 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 A19
.= card (Directed I) by A7, A21, SCMFSA8A:def 4
.= card I by SCMFSA8A:20 ;
:: thesis: verum
end;
suppose A38: 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 A35, A38, 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 A33, PBOOLE:143; :: thesis: verum
end;
A40: 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)) by A19
.= card (Directed I) by A7, A21, SCMFSA8A:def 4
.= card I by SCMFSA8A:20 ;
:: 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 B33, A32, A10, GRFUNC_1:2 ;
:: thesis: verum
end;
A41: for n being Element of NAT holds S1[n] from NAT_1:sch 1(A40, A34);
now
let n be Element of NAT ; :: thesis: IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),b1)) in dom (I ';' (Stop SCM+FSA))
per cases ( n < k or k <= n ) ;
suppose A42: n < k ; :: thesis: IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),b1)) in dom (I ';' (Stop SCM+FSA))
then IC (Comput ((P +* (Directed I)),(Initialize s),n)) = IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),n)) by A19;
then IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),n)) in dom (Directed I) by A7, A21, A42, SCMFSA8A:def 4;
hence IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),n)) in dom (I ';' (Stop SCM+FSA)) by A13; :: thesis: verum
end;
suppose k <= n ; :: thesis: IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),b1)) in dom (I ';' (Stop SCM+FSA))
hence IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),n)) in dom (I ';' (Stop SCM+FSA)) by A32, A41; :: thesis: verum
end;
end;
end;
hence I ';' (Stop SCM+FSA) is_closed_on s,P by SCMFSA7B:def 6; :: 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 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)) ) & ( for n being Element of 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 s1 = Initialize s;
set P1 = P +* I;
A43: I c= P +* I by FUNCT_4:25;
A44: card (Directed I) = card I by SCMFSA8A:20;
S1[k] by A41;
then A45: 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: ( LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(Initialize s)) = pseudo-LifeSpan (s,P,(Directed I)) & ( 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)) ) & ( for n being Element of 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 A41;
then A46: LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(Initialize s)) = k by A45, A26, 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)) ) );
A47: for n being Element of NAT st S2[n] holds
S2[n + 1]
proof
let n be Element of 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 A48: S2[n] ; :: thesis: S2[n + 1]
assume A49: 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 A50: IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),n)) in dom (Directed I) by A48, FUNCT_4:99, NAT_1:12;
A51: for f being FinSeq-Location holds (Comput ((P +* I),(Initialize s),n)) . f = (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),n)) . f by A48, A49, NAT_1:12, SCMFSA6A:7;
for a being Int-Location holds (Comput ((P +* I),(Initialize s),n)) . a = (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),n)) . a by A48, A49, NAT_1:12, SCMFSA6A:7;
then A52: Comput ((P +* I),(Initialize s),n) = Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),n) by A48, A49, A51, NAT_1:12, SCMFSA_2:61;
A53: now
assume A54: I . (IC (Comput ((P +* I),(Initialize s),n))) = halt SCM+FSA ; :: thesis: contradiction
A55: (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 A21, A49, NAT_1:12;
then A56: 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 A19, A55
.= (Directed I) . (IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),n))) by A50, A18, GRFUNC_1:2
.= goto (card I) by A48, A49, A54, NAT_1:12, SCMFSA8A:16 ;
A57: 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 A56, SCMFSA_2:69
.= card (Directed I) by SCMFSA8A:20 ;
IC (Comput ((P +* (Directed I)),(Initialize s),(n + 1))) in dom (Directed I) by A7, A49, SCMFSA8A:17;
hence contradiction by A57; :: thesis: verum
end;
A60: 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 A43, A48, A49, GRFUNC_1:2, NAT_1:12
.= (Directed I) . (IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),n))) by A48, A49, A53, NAT_1:12, SCMFSA8A:16
.= (P +* (I ';' (Stop SCM+FSA))) . (IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),n))) by A50, A14, GRFUNC_1:2
.= CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),n))) by PBOOLE:143 ;
A61: 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 A60 ;
pseudo-LifeSpan (s,P,(Directed I)) = k by A7, Th50;
then A62: IC (Comput ((P +* (Directed I)),(Initialize s),(n + 1))) = IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),(n + 1))) by A19, A49;
A63: 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 A64: Comput ((P +* I),(Initialize s),(n + 1)) = Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),(n + 1)) by A61, A52;
A65: 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 A64;
IC (Comput ((P +* (Directed I)),(Initialize s),(n + 1))) in dom (Directed I) by A7, A49, SCMFSA8A:17;
hence IC (Comput ((P +* I),(Initialize s),(n + 1))) in dom I by A62, A63, A64; :: 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 A64; :: 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 A64;
hence DataPart (Comput ((P +* I),(Initialize s),(n + 1))) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),(n + 1))) by A65, SCMFSA6A:7; :: thesis: verum
end;
IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),k)) = card I by A41;
then A66: IC (Comput ((P +* (Directed I)),(Initialize s),(LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(Initialize s))))) = card I by A19, A46;
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 A24, A46;
hence LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(Initialize s)) = pseudo-LifeSpan (s,P,(Directed I)) by A7, A66, A44, SCMFSA8A:def 4; :: thesis: ( ( 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)) ) & ( for n being Element of 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)) ) )
A67: S2[ 0 ]
proof
A68: IC (Comput ((P +* I),(Initialize s),0)) = IC (Initialize s) by EXTPRO_1:2
.= 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 A7, SCMFSA8A:17;
then IC (Initialize s) in dom (Directed I) by EXTPRO_1:2;
then 0 in dom (Directed I) by MEMSTR_0:16;
hence IC (Comput ((P +* I),(Initialize s),0)) in dom I by A68, 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)) by A16, A68, EXTPRO_1:2; :: 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) by EXTPRO_1:2
.= DataPart (Initialize s)
.= DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),0)) by EXTPRO_1:2 ; :: thesis: verum
end;
A69: for n being Element of NAT holds S2[n] from NAT_1:sch 1(A67, A47);
 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: for n being Element of 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 Element of 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 A70: 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 A70, 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 A69; :: thesis: verum
end;
suppose A71: 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
A73: n = m + 1 ;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
A74: 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 A73, EXTPRO_1:3;
set i = CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),m)));
A75: Comput ((P +* I),(Initialize s),n) = Following ((P +* I),(Comput ((P +* I),(Initialize s),m))) by A73, EXTPRO_1:3;
set l0 = IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),m));
set l = IC (Comput ((P +* I),(Initialize s),m));
A76: m + 0 < pseudo-LifeSpan (s,P,(Directed I)) by A71, A73, XREAL_1:6;
then A77: IC (Comput ((P +* I),(Initialize s),m)) = IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),m)) by A69;
A78: IC (Comput ((P +* I),(Initialize s),m)) in dom I by A69, A76;
then A79: IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),m)) in dom (Directed I) by A77, FUNCT_4:99;
A82: 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 A43, A78, GRFUNC_1:2 ;
A83: Directed I c= I ';' (Stop SCM+FSA) by SCMFSA6A:16;
then B84: dom (Directed I) c= dom (I ';' (Stop SCM+FSA)) by RELAT_1:11;
A85: (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 A79, A83, GRFUNC_1:2
.= (P +* (I ';' (Stop SCM+FSA))) . (IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),m))) by A10, B84, A79, GRFUNC_1:2
.= CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),m))) by PBOOLE:143 ;
A86: DataPart (Comput ((P +* I),(Initialize s),m)) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),m)) by A69, A76;
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 A87: 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 A78, A77, A82, A85, 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 A88: 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 A75, A87, EXTPRO_1:def 3
.= DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),m)) by A69, A76
.= DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),n)) by A74, A88, Th32 ; :: 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 A78, A77, A82, A85, SCMFSA8A:16;
hence DataPart (Comput ((P +* I),(Initialize s),n)) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),n)) by A75, A74, A86, SCMFSA6C:4; :: thesis: verum
end;
end;
end;
end;
end;
end;