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

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