let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: 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))),(s +* (Initialize (I ';' (Stop SCM+FSA))))) = 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),(s +* (Initialize I)),n)) = IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n)) ) & ( for n being Element of NAT st n <= pseudo-LifeSpan (s,P,(Directed I)) holds
DataPart (Comput ((P +* I),(s +* (Initialize I)),n)) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),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))),(s +* (Initialize (I ';' (Stop SCM+FSA))))) = 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),(s +* (Initialize I)),n)) = IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n)) ) & ( for n being Element of NAT st n <= pseudo-LifeSpan (s,P,(Directed I)) holds
DataPart (Comput ((P +* I),(s +* (Initialize I)),n)) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n)) ) )
set D = Data-Locations SCM+FSA;
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))),(s +* (Initialize (I ';' (Stop SCM+FSA))))) = 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),(s +* (Initialize I)),n)) = IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n)) ) & ( for n being Element of NAT st n <= pseudo-LifeSpan (s,P,(Directed I)) holds
DataPart (Comput ((P +* I),(s +* (Initialize I)),n)) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n)) ) ) )
set I0 = Directed I;
A1: Reloc ((Directed I),0) = Directed I by COMPOS_1:157;
A2: ProgramPart (Directed I) = Directed I by RELAT_1:209;
set I1 = I ';' (Stop SCM+FSA);
A3: ProgramPart (I ';' (Stop SCM+FSA)) = I ';' (Stop SCM+FSA) by RELAT_1:209;
A4: ProgramPart (Directed I) = Directed I by RELAT_1:209;
set s00 = s +* (Initialize (Directed I));
set P00 = P +* (Directed I);
set s10 = s +* (Initialize (I ';' (Stop SCM+FSA)));
set P10 = P +* (I ';' (Stop SCM+FSA));
reconsider k = pseudo-LifeSpan ((s +* (Initialize (Directed I))),(P +* (Directed I)),(Directed I)) as Element of NAT ;
(Stop SCM+FSA) . 0 = halt SCM+FSA by AFINSQ_1:38;
then A5: halt SCM+FSA = (Stop SCM+FSA) . ((card I) -' (card I)) by XREAL_1:234;
A6: DataPart (s +* (Initialize (Directed I))) = DataPart s by SCMFSA8A:11
.= DataPart (s +* (Initialize (I ';' (Stop SCM+FSA)))) by SCMFSA8A:11 ;
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))),(s +* (Initialize (I ';' (Stop SCM+FSA))))) = 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),(s +* (Initialize I)),n)) = IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n)) ) & ( for n being Element of NAT st n <= pseudo-LifeSpan (s,P,(Directed I)) holds
DataPart (Comput ((P +* I),(s +* (Initialize I)),n)) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n)) ) )
then A8: Directed I is_pseudo-closed_on s +* (Initialize (Directed I)),P +* (Directed I) by Th50;
defpred S1[ Nat] means ( k <= $1 implies ( IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),$1)) = card I & CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),$1))) = halt SCM+FSA ) );
A9: Initialize (I ';' (Stop SCM+FSA)) c= s +* (Initialize (I ';' (Stop SCM+FSA))) by FUNCT_4:26;
A10: I ';' (Stop SCM+FSA) c= P +* (I ';' (Stop SCM+FSA)) by FUNCT_4:26;
I ';' (Stop SCM+FSA) c= Initialize (I ';' (Stop SCM+FSA)) by SCMFSA8A:9;
then A11: I ';' (Stop SCM+FSA) c= s +* (Initialize (I ';' (Stop SCM+FSA))) by A9, XBOOLE_1:1;
A12: Directed I c= I ';' (Stop SCM+FSA) by SCMFSA6A:55;
then A13: dom (Directed I) c= dom (I ';' (Stop SCM+FSA)) by GRFUNC_1:8;
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:157;
then A15: Reloc ((Directed I),0) c= s +* (Initialize (I ';' (Stop SCM+FSA))) by A11, XBOOLE_1:1;
s +* (Initialize (I ';' (Stop SCM+FSA))) = Initialize (s +* (I ';' (Stop SCM+FSA))) by FUNCT_4:15;
then A16: IC (s +* (Initialize (I ';' (Stop SCM+FSA)))) = 0 by FUNCT_4:121;
A17: Initialize (Directed I) c= s +* (Initialize (Directed I)) by FUNCT_4:26;
A18: Directed I c= P +* (Directed I) by FUNCT_4:26;
A19: now
let n be Element of NAT ; :: thesis: ( n <= pseudo-LifeSpan ((s +* (Initialize (Directed I))),(P +* (Directed I)),(Directed I)) implies ( IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),n)) = IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n)) & DataPart (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),n)) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n)) ) )
assume A20: n <= pseudo-LifeSpan ((s +* (Initialize (Directed I))),(P +* (Directed I)),(Directed I)) ; :: thesis: ( IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),n)) = IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n)) & DataPart (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),n)) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n)) )
then (IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),n))) + 0 = IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n)) by A17, A8, A15, A16, A6, Th51, A1, A18, A14;
hence IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),n)) = IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n)) ; :: thesis: DataPart (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),n)) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n))
thus DataPart (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),n)) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n)) by A17, A8, A15, A16, A6, A20, Th51, A1, A18, A14; :: thesis: verum
end;
A21: k = pseudo-LifeSpan (s,P,(Directed I)) by A7, Th50;
A22: (s +* (Initialize (Directed I))) +* (Initialize (Directed I)) = s +* ((Initialize (Directed I)) +* (Initialize (Directed I))) by FUNCT_4:15
.= s +* (Initialize (Directed I)) ;
A23: (P +* (Directed I)) +* (Directed I) = P +* ((Directed I) +* (Directed I)) by FUNCT_4:15
.= P +* (Directed I) ;
A24: now
let n be Element of NAT ; :: thesis: ( n < pseudo-LifeSpan ((s +* (Initialize (Directed I))),(P +* (Directed I)),(Directed I)) implies ( CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),n))) = CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n))) & IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),n)) in dom (Directed I) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),n))) <> halt SCM+FSA ) )
assume A25: n < pseudo-LifeSpan ((s +* (Initialize (Directed I))),(P +* (Directed I)),(Directed I)) ; :: thesis: ( CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),n))) = CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n))) & IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),n)) in dom (Directed I) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),n))) <> halt SCM+FSA )
then IncAddr ((CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),n)))),0) = CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n))) by A17, A8, A15, A16, A6, Th51, A1, A18, A14;
hence CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),n))) = CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n))) by COMPOS_1:91; :: thesis: ( IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),n)) in dom (Directed I) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),n))) <> halt SCM+FSA )
thus IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),n)) in dom (Directed I) by A22, A8, A25, SCMFSA8A:31, A2, A23; :: thesis: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),n))) <> halt SCM+FSA
thus CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),n))) <> halt SCM+FSA by A22, A8, A25, SCMFSA8A:31, A2, A23; :: thesis: verum
end;
A26: now
let n be Element of NAT ; :: thesis: ( CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n))) = halt SCM+FSA implies not k > n )
assume A27: CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n))) = halt SCM+FSA ; :: thesis: not k > n
reconsider l = IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),n)) as Element of NAT ;
A28: (P +* (Directed I)) /. (IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),n))) = (P +* (Directed I)) . (IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),n))) by PBOOLE:158;
assume A29: k > n ; :: thesis: contradiction
then A30: l in dom (Directed I) by A7, A21, SCMFSA8A:def 5, A4;
CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n))) = CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),n))) by A24, A29
.= (P +* (Directed I)) . l by A28
.= (Directed I) . l by A30, GRFUNC_1:8, A18 ;
then halt SCM+FSA in rng (Directed I) by A27, A30, FUNCT_1:def 5;
hence contradiction by COMPOS_1:def 7; :: thesis: verum
end;
A31: card (Stop SCM+FSA) = 1 by COMPOS_1:46;
then card (I ';' (Stop SCM+FSA)) = (card I) + 1 by SCMFSA6A:61;
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:70;
card I < (card I) + (card (Stop SCM+FSA)) by A31, NAT_1:13;
then (I ';' (Stop SCM+FSA)) . (card I) = IncAddr ((halt SCM+FSA),(card I)) by A5, Th13
.= halt SCM+FSA by COMPOS_1:93 ;
then A33: (P +* (I ';' (Stop SCM+FSA))) . (card I) = halt SCM+FSA by A32, A10, GRFUNC_1:8;
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]
A36: (P +* (I ';' (Stop SCM+FSA))) /. (IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),(n + 1)))) = (P +* (I ';' (Stop SCM+FSA))) . (IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),(n + 1)))) by PBOOLE:158;
assume A37: k <= n + 1 ; :: thesis: ( IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),(n + 1))) = card I & CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),(n + 1)))) = halt SCM+FSA )
hereby :: thesis: CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),(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))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),(n + 1))) = card I
hence IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),(n + 1))) = IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),k)) by A19
.= card (Directed I) by A7, A21, SCMFSA8A:def 5, A2
.= card I by SCMFSA8A:34 ;
:: thesis: verum
end;
suppose A38: k <= n ; :: thesis: IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),(n + 1))) = card I
Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),(n + 1)) = Following ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n))) by EXTPRO_1:4
.= Exec ((CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n)))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n))) ;
hence IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),(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))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),(n + 1)))) = halt SCM+FSA by A33, A36; :: thesis: verum
end;
A39: (P +* (I ';' (Stop SCM+FSA))) /. (IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),0))) = (P +* (I ';' (Stop SCM+FSA))) . (IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),0))) by PBOOLE:158;
A40: S1[ 0 ]
proof
assume k <= 0 ; :: thesis: ( IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),0)) = card I & CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),0))) = halt SCM+FSA )
then k = 0 ;
hence IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),0)) = IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),k)) by A19
.= card (Directed I) by A7, A21, SCMFSA8A:def 5, A2
.= card I by SCMFSA8A:34 ;
:: thesis: CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),0))) = halt SCM+FSA
hence CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),0))) = halt SCM+FSA by A33, A39; :: 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))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),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))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),b1)) in dom (I ';' (Stop SCM+FSA))
then IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),n)) = IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n)) by A19;
then IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n)) in dom (Directed I) by A7, A21, A42, SCMFSA8A:def 5, A4;
hence IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n)) in dom (I ';' (Stop SCM+FSA)) by A13; :: thesis: verum
end;
suppose k <= n ; :: thesis: IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),b1)) in dom (I ';' (Stop SCM+FSA))
hence IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),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 7, A3; :: thesis: ( I ';' (Stop SCM+FSA) is_halting_on s,P & LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA))))) = 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),(s +* (Initialize I)),n)) = IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n)) ) & ( for n being Element of NAT st n <= pseudo-LifeSpan (s,P,(Directed I)) holds
DataPart (Comput ((P +* I),(s +* (Initialize I)),n)) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n)) ) )
set s1 = s +* (Initialize I);
set P1 = P +* I;
A43: I c= P +* I by FUNCT_4:26;
A44: card (Directed I) = card I by SCMFSA8A:34;
S1[k] by A41;
then A45: P +* (I ';' (Stop SCM+FSA)) halts_on s +* (Initialize (I ';' (Stop SCM+FSA))) by EXTPRO_1:30;
hence I ';' (Stop SCM+FSA) is_halting_on s,P by SCMFSA7B:def 8, A3; :: thesis: ( LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA))))) = 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),(s +* (Initialize I)),n)) = IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n)) ) & ( for n being Element of NAT st n <= pseudo-LifeSpan (s,P,(Directed I)) holds
DataPart (Comput ((P +* I),(s +* (Initialize I)),n)) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n)) ) )
CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),k))) = halt SCM+FSA by A41;
then A46: LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA))))) = k by A45, A26, EXTPRO_1:def 14;
defpred S2[ Nat] means ( $1 < pseudo-LifeSpan (s,P,(Directed I)) implies ( IC (Comput ((P +* I),(s +* (Initialize I)),$1)) in dom I & IC (Comput ((P +* I),(s +* (Initialize I)),$1)) = IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),$1)) & DataPart (Comput ((P +* I),(s +* (Initialize I)),$1)) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),$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),(s +* (Initialize I)),n));
set l0 = IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n));
assume A48: S2[n] ; :: thesis: S2[n + 1]
assume A49: n + 1 < pseudo-LifeSpan (s,P,(Directed I)) ; :: thesis: ( IC (Comput ((P +* I),(s +* (Initialize I)),(n + 1))) in dom I & IC (Comput ((P +* I),(s +* (Initialize I)),(n + 1))) = IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),(n + 1))) & DataPart (Comput ((P +* I),(s +* (Initialize I)),(n + 1))) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),(n + 1))) )
then A50: IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n)) in dom (Directed I) by A48, FUNCT_4:105, NAT_1:12;
A51: for f being FinSeq-Location holds (Comput ((P +* I),(s +* (Initialize I)),n)) . f = (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n)) . f by A48, A49, NAT_1:12, SCMFSA6A:38;
for a being Int-Location holds (Comput ((P +* I),(s +* (Initialize I)),n)) . a = (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n)) . a by A48, A49, NAT_1:12, SCMFSA6A:38;
then A52: Comput ((P +* I),(s +* (Initialize I)),n), Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n) equal_outside NAT by A48, A49, A51, NAT_1:12, SCMFSA10:91;
A53: now
assume A54: I . (IC (Comput ((P +* I),(s +* (Initialize I)),n))) = halt SCM+FSA ; :: thesis: contradiction
A55: (P +* (Directed I)) /. (IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),n))) = (P +* (Directed I)) . (IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),n))) by PBOOLE:158;
n < k by A21, A49, NAT_1:12;
then A56: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),n))) = (P +* (Directed I)) . (IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n))) by A19, A55
.= (P +* (Directed I)) . (IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n)))
.= (Directed I) . (IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n))) by A50, A18, GRFUNC_1:8
.= (Directed I) . (IC (Comput ((P +* I),(s +* (Initialize I)),n))) by A48, A49, NAT_1:12
.= goto (card I) by A48, A49, A54, NAT_1:12, SCMFSA8A:30 ;
A57: IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),(n + 1))) = IC (Following ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),n)))) by EXTPRO_1:4
.= card I by A56, SCMFSA_2:95
.= card (Directed I) by SCMFSA8A:34 ;
IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),(n + 1))) in dom (Directed I) by A7, A49, SCMFSA8A:31, A2;
hence contradiction by A57; :: thesis: verum
end;
A58: (P +* I) /. (IC (Comput ((P +* I),(s +* (Initialize I)),n))) = (P +* I) . (IC (Comput ((P +* I),(s +* (Initialize I)),n))) by PBOOLE:158;
A59: (P +* (I ';' (Stop SCM+FSA))) /. (IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n))) = (P +* (I ';' (Stop SCM+FSA))) . (IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n))) by PBOOLE:158;
A60: CurInstr ((P +* I),(Comput ((P +* I),(s +* (Initialize I)),n))) = (P +* I) . (IC (Comput ((P +* I),(s +* (Initialize I)),n))) by A58
.= I . (IC (Comput ((P +* I),(s +* (Initialize I)),n))) by A43, GRFUNC_1:8, A48, A49, NAT_1:12
.= (Directed I) . (IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n))) by A48, A49, A53, NAT_1:12, SCMFSA8A:30
.= (P +* (I ';' (Stop SCM+FSA))) . (IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n))) by A50, A14, GRFUNC_1:8
.= CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n))) by A59 ;
A61: Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),(n + 1)) = Following ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n))) by EXTPRO_1:4
.= Exec ((CurInstr ((P +* I),(Comput ((P +* I),(s +* (Initialize I)),n)))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n))) by A60 ;
pseudo-LifeSpan (s,P,(Directed I)) = k by A7, Th50;
then A62: IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),(n + 1))) = IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),(n + 1))) by A19, A49;
A63: dom (Directed I) = dom I by FUNCT_4:105;
Comput ((P +* I),(s +* (Initialize I)),(n + 1)) = Following ((P +* I),(Comput ((P +* I),(s +* (Initialize I)),n))) by EXTPRO_1:4
.= Exec ((CurInstr ((P +* I),(Comput ((P +* I),(s +* (Initialize I)),n)))),(Comput ((P +* I),(s +* (Initialize I)),n))) ;
then A64: Comput ((P +* I),(s +* (Initialize I)),(n + 1)), Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),(n + 1)) equal_outside NAT by A61, A52, AMISTD_2:def 20;
A65: for f being FinSeq-Location holds (Comput ((P +* I),(s +* (Initialize I)),(n + 1))) . f = (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),(n + 1))) . f by SCMFSA10:93, A64;
IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),(n + 1))) in dom (Directed I) by A7, A49, SCMFSA8A:31, A2;
hence IC (Comput ((P +* I),(s +* (Initialize I)),(n + 1))) in dom I by A62, A63, COMPOS_1:24, A64; :: thesis: ( IC (Comput ((P +* I),(s +* (Initialize I)),(n + 1))) = IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),(n + 1))) & DataPart (Comput ((P +* I),(s +* (Initialize I)),(n + 1))) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),(n + 1))) )
thus IC (Comput ((P +* I),(s +* (Initialize I)),(n + 1))) = IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),(n + 1))) by COMPOS_1:24, A64; :: thesis: DataPart (Comput ((P +* I),(s +* (Initialize I)),(n + 1))) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),(n + 1)))
for a being Int-Location holds (Comput ((P +* I),(s +* (Initialize I)),(n + 1))) . a = (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),(n + 1))) . a by SCMFSA10:92, A64;
hence DataPart (Comput ((P +* I),(s +* (Initialize I)),(n + 1))) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),(n + 1))) by A65, SCMFSA6A:38; :: thesis: verum
end;
IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),k)) = card I by A41;
then A66: IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),(LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))))))) = card I by A19, A46;
for n being Element of NAT st not IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),n)) in dom (Directed I) holds
LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA))))) <= n by A24, A46;
hence LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA))))) = pseudo-LifeSpan (s,P,(Directed I)) by A7, A66, A44, SCMFSA8A:def 5, A2; :: thesis: ( ( for n being Element of NAT st n < pseudo-LifeSpan (s,P,(Directed I)) holds
IC (Comput ((P +* I),(s +* (Initialize I)),n)) = IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n)) ) & ( for n being Element of NAT st n <= pseudo-LifeSpan (s,P,(Directed I)) holds
DataPart (Comput ((P +* I),(s +* (Initialize I)),n)) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n)) ) )
A67: S2[ 0 ]
proof
A68: IC (Comput ((P +* I),(s +* (Initialize I)),0)) = IC (s +* (Initialize I)) by EXTPRO_1:3
.= IC (Initialize (s +* I)) by FUNCT_4:15
.= 0 by FUNCT_4:121 ;
assume 0 < pseudo-LifeSpan (s,P,(Directed I)) ; :: thesis: ( IC (Comput ((P +* I),(s +* (Initialize I)),0)) in dom I & IC (Comput ((P +* I),(s +* (Initialize I)),0)) = IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),0)) & DataPart (Comput ((P +* I),(s +* (Initialize I)),0)) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),0)) )
then IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),0)) in dom (Directed I) by A7, SCMFSA8A:31, A2;
then IC (s +* (Initialize (Directed I))) in dom (Directed I) by EXTPRO_1:3;
then 0 in dom (Directed I) by Th31;
hence IC (Comput ((P +* I),(s +* (Initialize I)),0)) in dom I by A68, FUNCT_4:105; :: thesis: ( IC (Comput ((P +* I),(s +* (Initialize I)),0)) = IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),0)) & DataPart (Comput ((P +* I),(s +* (Initialize I)),0)) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),0)) )
thus IC (Comput ((P +* I),(s +* (Initialize I)),0)) = IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),0)) by A16, A68, EXTPRO_1:3; :: thesis: DataPart (Comput ((P +* I),(s +* (Initialize I)),0)) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),0))
thus DataPart (Comput ((P +* I),(s +* (Initialize I)),0)) = DataPart (s +* (Initialize I)) by EXTPRO_1:3
.= DataPart s by SCMFSA8A:11
.= DataPart (s +* (Initialize (I ';' (Stop SCM+FSA)))) by SCMFSA8A:11
.= DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),0)) by EXTPRO_1:3 ; :: 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),(s +* (Initialize I)),n)) = IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n)) ; :: thesis: for n being Element of NAT st n <= pseudo-LifeSpan (s,P,(Directed I)) holds
DataPart (Comput ((P +* I),(s +* (Initialize I)),n)) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n))
let n be Element of NAT ; :: thesis: ( n <= pseudo-LifeSpan (s,P,(Directed I)) implies DataPart (Comput ((P +* I),(s +* (Initialize I)),n)) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n)) )
assume A70: n <= pseudo-LifeSpan (s,P,(Directed I)) ; :: thesis: DataPart (Comput ((P +* I),(s +* (Initialize I)),n)) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),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),(s +* (Initialize I)),n)) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n))
hence DataPart (Comput ((P +* I),(s +* (Initialize I)),n)) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n)) by A69; :: thesis: verum
end;
suppose A71: n = pseudo-LifeSpan (s,P,(Directed I)) ; :: thesis: DataPart (Comput ((P +* I),(s +* (Initialize I)),n)) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n))
hereby :: thesis: verum
per cases ( n = 0 or ex m being Nat st n = m + 1 ) by NAT_1:6;
suppose A72: n = 0 ; :: thesis: DataPart (Comput ((P +* I),(s +* (Initialize I)),n)) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n))
hence DataPart (Comput ((P +* I),(s +* (Initialize I)),n)) = DataPart (s +* (Initialize I)) by EXTPRO_1:3
.= DataPart s by SCMFSA8A:11
.= DataPart (s +* (Initialize (I ';' (Stop SCM+FSA)))) by SCMFSA8A:11
.= DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n)) by A72, EXTPRO_1:3 ;
:: thesis: verum
end;
suppose ex m being Nat st n = m + 1 ; :: thesis: DataPart (Comput ((P +* I),(s +* (Initialize I)),n)) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n))
then consider m being Nat such that
A73: n = m + 1 ;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
A74: Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n) = Following ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),m))) by A73, EXTPRO_1:4
.= Exec ((CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),m)))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),m))) ;
set i = CurInstr ((P +* I),(Comput ((P +* I),(s +* (Initialize I)),m)));
A75: Comput ((P +* I),(s +* (Initialize I)),n) = Following ((P +* I),(Comput ((P +* I),(s +* (Initialize I)),m))) by A73, EXTPRO_1:4
.= Exec ((CurInstr ((P +* I),(Comput ((P +* I),(s +* (Initialize I)),m)))),(Comput ((P +* I),(s +* (Initialize I)),m))) ;
set l0 = IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),m));
set l = IC (Comput ((P +* I),(s +* (Initialize I)),m));
A76: m + 0 < pseudo-LifeSpan (s,P,(Directed I)) by A71, A73, XREAL_1:8;
then A77: IC (Comput ((P +* I),(s +* (Initialize I)),m)) = IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),m)) by A69;
A78: IC (Comput ((P +* I),(s +* (Initialize I)),m)) in dom I by A69, A76;
then A79: IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),m)) in dom (Directed I) by A77, FUNCT_4:105;
A80: (P +* I) /. (IC (Comput ((P +* I),(s +* (Initialize I)),m))) = (P +* I) . (IC (Comput ((P +* I),(s +* (Initialize I)),m))) by PBOOLE:158;
A81: (P +* (I ';' (Stop SCM+FSA))) /. (IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),m))) = (P +* (I ';' (Stop SCM+FSA))) . (IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),m))) by PBOOLE:158;
A82: CurInstr ((P +* I),(Comput ((P +* I),(s +* (Initialize I)),m))) = (P +* I) . (IC (Comput ((P +* I),(s +* (Initialize I)),m))) by A80
.= I . (IC (Comput ((P +* I),(s +* (Initialize I)),m))) by A43, GRFUNC_1:8, A78 ;
A83: Directed I c= I ';' (Stop SCM+FSA) by SCMFSA6A:55;
then dom (Directed I) c= dom (I ';' (Stop SCM+FSA)) by RELAT_1:25;
then A84: IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),m)) in dom (I ';' (Stop SCM+FSA)) by A79;
A85: (Directed I) . (IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),m))) = (I ';' (Stop SCM+FSA)) . (IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),m))) by A79, GRFUNC_1:8, A83
.= (P +* (I ';' (Stop SCM+FSA))) . (IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),m))) by GRFUNC_1:8, A10, A84
.= CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),m))) by A81 ;
A86: DataPart (Comput ((P +* I),(s +* (Initialize I)),m)) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),m)) by A69, A76;
hereby :: thesis: verum
per cases ( CurInstr ((P +* I),(Comput ((P +* I),(s +* (Initialize I)),m))) = halt SCM+FSA or CurInstr ((P +* I),(Comput ((P +* I),(s +* (Initialize I)),m))) <> halt SCM+FSA ) ;
suppose A87: CurInstr ((P +* I),(Comput ((P +* I),(s +* (Initialize I)),m))) = halt SCM+FSA ; :: thesis: DataPart (Comput ((P +* I),(s +* (Initialize I)),n)) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n))
then CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),m))) = goto (card I) by A78, A77, A82, A85, SCMFSA8A:30;
then InsCode (CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),m)))) = 6 by SCMFSA_2:47;
then A88: InsCode (CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),m)))) in {0,6,7,8} by ENUMSET1:def 2;
thus DataPart (Comput ((P +* I),(s +* (Initialize I)),n)) = DataPart (Comput ((P +* I),(s +* (Initialize I)),m)) by A75, A87, EXTPRO_1:def 3
.= DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),m)) by A69, A76
.= DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n)) by A74, A88, Th32 ; :: thesis: verum
end;
suppose CurInstr ((P +* I),(Comput ((P +* I),(s +* (Initialize I)),m))) <> halt SCM+FSA ; :: thesis: DataPart (Comput ((P +* I),(s +* (Initialize I)),n)) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n))
then CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),m))) = CurInstr ((P +* I),(Comput ((P +* I),(s +* (Initialize I)),m))) by A78, A77, A82, A85, SCMFSA8A:30;
hence DataPart (Comput ((P +* I),(s +* (Initialize I)),n)) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n)) by A75, A74, A86, SCMFSA6C:5; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
end;