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 SCMPDS st stop I c= P1 & I is_closed_on s1,P1 & I is_halting_on s1,P1 holds
for n being Element of 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 SCMPDS st stop I c= P1 & I is_closed_on s1,P1 & I is_halting_on s1,P1 holds
for n being Element of 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 SCMPDS st stop I c= P1 & I is_closed_on s1,P1 & I is_halting_on s1,P1 holds
for n being Element of 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 SCMPDS; :: thesis: ( stop I c= P1 & I is_closed_on s1,P1 & I is_halting_on s1,P1 implies for n being Element of 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 Element of 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)))) )
B1: Start-At (0,SCMPDS) c= s1 by MEMSTR_0:29;
XX: P1 +* (stop I) = P1 by A1, FUNCT_4:98;
let n be Element of 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
A4: Shift (I,n) c= P2 and
A6: IC s2 = n and
A7: 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, Th35, INT_1:7;
then consider i being Nat such that
A8: 1 + i = LifeSpan (P1,s1) by NAT_1:10;
A9: Initialize s1 = s1 by B1, FUNCT_4:98;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
A10: i < LifeSpan (P1,s1) by A8, XREAL_1:29;
then A11: (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) by A1, A2, A3, A4, A6, A7, Th34;
set L1 = IC (Comput (P1,s1,i));
A12: IC (Comput (P1,s1,i)) in dom I by A1, A2, A3, A8, Th33, 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, A4, A6, A7, A10, Th34 ;
A15: I c= stop I by AFINSQ_1:74;
then A16: dom I c= dom (stop I) by RELAT_1:11;
A18: 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 Element of NAT ;
CurInstr (P2,(Comput (P2,s2,i))) = CurInstr (P1,(Comput (P1,s1,i))) by A1, A2, A3, A4, A6, A7, A10, Th34;
then A20: CurInstr (P2,(Comput (P2,s2,i))) = P1 . (IC (Comput (P1,s1,i))) by PBOOLE:143
.= (stop I) . (IC (Comput (P1,s1,i))) by A1, A12, A16, GRFUNC_1:2
.= I . (IC (Comput (P1,s1,i))) by A12, A15, GRFUNC_1:2 ;
then A21: InsCode (CurInstr (P2,(Comput (P2,s2,i)))) <> 1 by A12, SCMPDS_4:def 9;
A22: DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) by A1, A2, A3, A4, A6, A7, A10, Th34;
A23: CurInstr (P2,(Comput (P2,s2,i))) valid_at m by A12, A20, SCMPDS_4:def 9;
A24: InsCode (CurInstr (P2,(Comput (P2,s2,i)))) <> 3 by A12, A20, SCMPDS_4:def 9;
IC (Comput (P1,s1,(i + 1))) = card I by A2, A3, A8, XX, SCMPDS_6:29, A9;
hence IC (Comput (P2,s2,(LifeSpan (P1,s1)))) = (card I) + n by A8, A11, A21, A24, A23, A14, A22, A18, 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 A8, A11, A21, A24, A23, A14, A22, A18, SCMPDS_4:28; :: thesis: verum