let s2 be State of SCMPDS; :: thesis: for P1, P2 being Instruction-Sequence of SCMPDS
for s1 being 0 -started State of SCMPDS
for I being halt-free shiftable Program of st stop I c= P1 & I is_closed_on s1,P1 & I is_halting_on s1,P1 holds
for n being Nat st Shift (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds
( IC (Comput (P2,s2,(LifeSpan (P1,s1)))) = (card I) + n & DataPart (Comput (P1,s1,(LifeSpan (P1,s1)))) = DataPart (Comput (P2,s2,(LifeSpan (P1,s1)))) )
let P1, P2 be Instruction-Sequence of SCMPDS; :: thesis: for s1 being 0 -started State of SCMPDS
for I being halt-free shiftable Program of st stop I c= P1 & I is_closed_on s1,P1 & I is_halting_on s1,P1 holds
for n being Nat st Shift (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds
( IC (Comput (P2,s2,(LifeSpan (P1,s1)))) = (card I) + n & DataPart (Comput (P1,s1,(LifeSpan (P1,s1)))) = DataPart (Comput (P2,s2,(LifeSpan (P1,s1)))) )
let s1 be 0 -started State of SCMPDS; :: thesis: for I being halt-free shiftable Program of st stop I c= P1 & I is_closed_on s1,P1 & I is_halting_on s1,P1 holds
for n being Nat st Shift (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds
( IC (Comput (P2,s2,(LifeSpan (P1,s1)))) = (card I) + n & DataPart (Comput (P1,s1,(LifeSpan (P1,s1)))) = DataPart (Comput (P2,s2,(LifeSpan (P1,s1)))) )
let I be halt-free shiftable Program of ; :: thesis: ( stop I c= P1 & I is_closed_on s1,P1 & I is_halting_on s1,P1 implies for n being Nat st Shift (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds
( IC (Comput (P2,s2,(LifeSpan (P1,s1)))) = (card I) + n & DataPart (Comput (P1,s1,(LifeSpan (P1,s1)))) = DataPart (Comput (P2,s2,(LifeSpan (P1,s1)))) ) )
assume that
A1: stop I c= P1 and
A2: I is_closed_on s1,P1 and
A3: I is_halting_on s1,P1 ; :: thesis: for n being Nat st Shift (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds
( IC (Comput (P2,s2,(LifeSpan (P1,s1)))) = (card I) + n & DataPart (Comput (P1,s1,(LifeSpan (P1,s1)))) = DataPart (Comput (P2,s2,(LifeSpan (P1,s1)))) )
A4: Start-At (0,SCMPDS) c= s1 by MEMSTR_0:29;
A5: P1 +* (stop I) = P1 by A1, FUNCT_4:98;
let n be Nat; :: thesis: ( Shift (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 implies ( IC (Comput (P2,s2,(LifeSpan (P1,s1)))) = (card I) + n & DataPart (Comput (P1,s1,(LifeSpan (P1,s1)))) = DataPart (Comput (P2,s2,(LifeSpan (P1,s1)))) ) )
assume that
A6: Shift (I,n) c= P2 and
A7: IC s2 = n and
A8: DataPart s1 = DataPart s2 ; :: thesis: ( IC (Comput (P2,s2,(LifeSpan (P1,s1)))) = (card I) + n & DataPart (Comput (P1,s1,(LifeSpan (P1,s1)))) = DataPart (Comput (P2,s2,(LifeSpan (P1,s1)))) )
1 + 0 <= LifeSpan (P1,s1) by A1, A3, Th15, INT_1:7;
then consider i being Nat such that
A9: 1 + i = LifeSpan (P1,s1) by NAT_1:10;
A10: Initialize s1 = s1 by A4, FUNCT_4:98;
reconsider i = i as Nat ;
A11: i < LifeSpan (P1,s1) by A9, XREAL_1:29;
then A12: (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) by A1, A2, A3, A6, A7, A8, Th14;
set L1 = IC (Comput (P1,s1,i));
A13: IC (Comput (P1,s1,i)) in dom I by A1, A2, A3, A9, Th13, XREAL_1:29;
set i2 = CurInstr (P2,(Comput (P2,s2,i)));
A14: Comput (P1,s1,(i + 1)) = Following (P1,(Comput (P1,s1,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P1,s1,i))) by A1, A2, A3, A6, A7, A8, A11, Th14 ;
A15: I c= stop I by AFINSQ_1:74;
then A16: dom I c= dom (stop I) by RELAT_1:11;
A17: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) ;
reconsider m = IC (Comput (P1,s1,i)) as Nat ;
CurInstr (P2,(Comput (P2,s2,i))) = CurInstr (P1,(Comput (P1,s1,i))) by A1, A2, A3, A6, A7, A8, A11, Th14;
then A18: CurInstr (P2,(Comput (P2,s2,i))) = P1 . (IC (Comput (P1,s1,i))) by PBOOLE:143
.= (stop I) . (IC (Comput (P1,s1,i))) by A1, A13, A16, GRFUNC_1:2
.= I . (IC (Comput (P1,s1,i))) by A13, A15, GRFUNC_1:2 ;
then A19: InsCode (CurInstr (P2,(Comput (P2,s2,i)))) <> 1 by A13, SCMPDS_4:def 9;
A20: DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) by A1, A2, A3, A6, A7, A8, A11, Th14;
A21: CurInstr (P2,(Comput (P2,s2,i))) valid_at m by A13, A18, SCMPDS_4:def 9;
A22: InsCode (CurInstr (P2,(Comput (P2,s2,i)))) <> 3 by A13, A18, SCMPDS_4:def 9;
IC (Comput (P1,s1,(i + 1))) = card I by A2, A3, A9, A5, A10, SCMPDS_6:29;
hence IC (Comput (P2,s2,(LifeSpan (P1,s1)))) = (card I) + n by A9, A12, A19, A22, A21, A14, A20, A17, SCMPDS_4:28; :: thesis: DataPart (Comput (P1,s1,(LifeSpan (P1,s1)))) = DataPart (Comput (P2,s2,(LifeSpan (P1,s1))))
thus DataPart (Comput (P1,s1,(LifeSpan (P1,s1)))) = DataPart (Comput (P2,s2,(LifeSpan (P1,s1)))) by A9, A12, A19, A22, A21, A14, A20, A17, SCMPDS_4:28; :: thesis: verum