let s1, s2 be State of ; :: thesis: for I being shiftable No-StopCode Program of st Initialized (stop I) c= s1 & I is_closed_on s1 & I is_halting_on s1 holds
for n being Element of NAT st Shift I,n c= s2 & card I > 0 & IC s2 = inspos n & DataPart s1 = DataPart s2 holds
( IC (Computation s2,(LifeSpan s1)) = inspos ((card I) + n) & DataPart (Computation s1,(LifeSpan s1)) = DataPart (Computation s2,(LifeSpan s1)) )
let I be shiftable No-StopCode Program of ; :: thesis: ( Initialized (stop I) c= s1 & I is_closed_on s1 & I is_halting_on s1 implies for n being Element of NAT st Shift I,n c= s2 & card I > 0 & IC s2 = inspos n & DataPart s1 = DataPart s2 holds
( IC (Computation s2,(LifeSpan s1)) = inspos ((card I) + n) & DataPart (Computation s1,(LifeSpan s1)) = DataPart (Computation s2,(LifeSpan s1)) ) )
set II = Initialized (stop I);
assume that
A1: Initialized (stop I) c= s1 and
A2: I is_closed_on s1 and
A3: I is_halting_on s1 ; :: thesis: for n being Element of NAT st Shift I,n c= s2 & card I > 0 & IC s2 = inspos n & DataPart s1 = DataPart s2 holds
( IC (Computation s2,(LifeSpan s1)) = inspos ((card I) + n) & DataPart (Computation s1,(LifeSpan s1)) = DataPart (Computation s2,(LifeSpan s1)) )
let n be Element of NAT ; :: thesis: ( Shift I,n c= s2 & card I > 0 & IC s2 = inspos n & DataPart s1 = DataPart s2 implies ( IC (Computation s2,(LifeSpan s1)) = inspos ((card I) + n) & DataPart (Computation s1,(LifeSpan s1)) = DataPart (Computation s2,(LifeSpan s1)) ) )
assume that
A4: Shift I,n c= s2 and
A5: card I > 0 and
A6: IC s2 = inspos n and
A7: DataPart s1 = DataPart s2 ; :: thesis: ( IC (Computation s2,(LifeSpan s1)) = inspos ((card I) + n) & DataPart (Computation s1,(LifeSpan s1)) = DataPart (Computation s2,(LifeSpan s1)) )
1 + 0 <= LifeSpan s1 by A1, A3, A5, Th35, INT_1:20;
then consider i being Nat such that
A8: 1 + i = LifeSpan s1 by NAT_1:10;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
A9: i < LifeSpan s1 by A8, XREAL_1:31;
then A10: (IC (Computation s1,i)) + n = IC (Computation s2,i) by A1, A2, A3, A4, A5, A6, A7, Th34;
set L1 = IC (Computation s1,i);
A11: IC (Computation s1,i) in dom I by A1, A2, A3, A8, Th33, XREAL_1:31;
set i2 = CurInstr (Computation s2,i);
A12: Computation s1,(i + 1) = Following (Computation s1,i) by AMI_1:14
.= Exec (CurInstr (Computation s2,i)),(Computation s1,i) by A1, A2, A3, A4, A5, A6, A7, A9, Th34 ;
A13: I c= Initialized (stop I) by SCMPDS_6:17;
then A14: dom I c= dom (Initialized (stop I)) by GRFUNC_1:8;
A15: Computation s2,(i + 1) = Following (Computation s2,i) by AMI_1:14
.= Exec (CurInstr (Computation s2,i)),(Computation s2,i) ;
reconsider m = IC (Computation s1,i) as Element of NAT by ORDINAL1:def 13;
A16: IC (Computation s1,i) = inspos m ;
CurInstr (Computation s2,i) = CurInstr (Computation s1,i) by A1, A2, A3, A4, A5, A6, A7, A9, Th34;
then A17: CurInstr (Computation s2,i) = s1 . (IC (Computation s1,i)) by AMI_1:54
.= (Initialized (stop I)) . (IC (Computation s1,i)) by A1, A11, A14, GRFUNC_1:8
.= I . (IC (Computation s1,i)) by A11, A13, GRFUNC_1:8 ;
then A18: InsCode (CurInstr (Computation s2,i)) <> 1 by A11, A16, SCMPDS_4:def 12;
A19: DataPart (Computation s1,i) = DataPart (Computation s2,i) by A1, A2, A3, A4, A5, A6, A7, A9, Th34;
A20: CurInstr (Computation s2,i) valid_at m by A11, A17, A16, SCMPDS_4:def 12;
A21: InsCode (CurInstr (Computation s2,i)) <> 3 by A11, A17, A16, SCMPDS_4:def 12;
s1 = s1 +* (Initialized (stop I)) by A1, FUNCT_4:79;
then IC (Computation s1,(i + 1)) = inspos (card I) by A2, A3, A8, SCMPDS_6:43;
hence IC (Computation s2,(LifeSpan s1)) = (inspos (card I)) + n by A8, A10, A16, A18, A21, A20, A12, A19, A15, SCMPDS_4:83
.= inspos ((card I) + n) ;
:: thesis: DataPart (Computation s1,(LifeSpan s1)) = DataPart (Computation s2,(LifeSpan s1))
thus DataPart (Computation s1,(LifeSpan s1)) = DataPart (Computation s2,(LifeSpan s1)) by A8, A10, A16, A18, A21, A20, A12, A19, A15, SCMPDS_4:83; :: thesis: verum