let s1, s2 be State of SCMPDS; :: thesis: for P1, P2 being the Instructions of SCMPDS -valued ManySortedSet of NAT
for I being halt-free shiftable Program of SCMPDS st stop I c= P1 & Start-At (0,SCMPDS) c= s1 & 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 the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: for I being halt-free shiftable Program of SCMPDS st stop I c= P1 & Start-At (0,SCMPDS) c= s1 & 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 & Start-At (0,SCMPDS) c= s1 & 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
B1: Start-At (0,SCMPDS) c= s1 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)))) )
XX: P1 +* (stop I) = P1 by A1, FUNCT_4:104;
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:20, B1;
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:104;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
A10: i < LifeSpan (P1,s1) by A8, XREAL_1:31;
then A11: (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) by A1, A2, A3, A4, A6, A7, Th34, B1;
set L1 = IC (Comput (P1,s1,i));
A12: IC (Comput (P1,s1,i)) in dom I by A1, A2, A3, A8, Th33, XREAL_1:31, B1;
set i2 = CurInstr (P2,(Comput (P2,s2,i)));
A14: Comput (P1,s1,(i + 1)) = Following (P1,(Comput (P1,s1,i))) by EXTPRO_1:4
.= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P1,s1,i))) by A1, A2, A3, A4, A6, A7, A10, Th34, B1 ;
A15: I c= stop I by AFINSQ_1:78;
then A16: dom I c= dom (stop I) by RELAT_1:25;
A18: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:4
.= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) ;
reconsider m = IC (Comput (P1,s1,i)) as Element of NAT ;
A19: P1 /. (IC (Comput (P1,s1,i))) = P1 . (IC (Comput (P1,s1,i))) by PBOOLE:158;
CurInstr (P2,(Comput (P2,s2,i))) = CurInstr (P1,(Comput (P1,s1,i))) by A1, A2, A3, A4, A6, A7, A10, Th34, B1;
then A20: CurInstr (P2,(Comput (P2,s2,i))) = P1 . (IC (Comput (P1,s1,i))) by A19
.= (stop I) . (IC (Comput (P1,s1,i))) by A1, A12, A16, GRFUNC_1:8
.= I . (IC (Comput (P1,s1,i))) by A12, A15, GRFUNC_1:8 ;
then A21: InsCode (CurInstr (P2,(Comput (P2,s2,i)))) <> 1 by A12, SCMPDS_4:def 12;
A22: DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) by A1, A2, A3, A4, A6, A7, A10, Th34, B1;
A23: CurInstr (P2,(Comput (P2,s2,i))) valid_at m by A12, A20, SCMPDS_4:def 12;
A24: InsCode (CurInstr (P2,(Comput (P2,s2,i)))) <> 3 by A12, A20, SCMPDS_4:def 12;
s1 = Initialize s1 by A9;
then IC (Comput (P1,s1,(i + 1))) = card I by A2, A3, A8, SCMPDS_6:43, XX;
hence IC (Comput (P2,s2,(LifeSpan (P1,s1)))) = (card I) + n by A8, A11, A21, A24, A23, A14, A22, A18, SCMPDS_4:83
.= (card I) + n ;
:: 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:83; :: thesis: verum