let s1, s2 be State of SCMPDS ; :: thesis: for I being shiftable No-StopCode Program of SCMPDS 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 = n & DataPart s1 = DataPart s2 holds
( IC (Comput (ProgramPart s2),s2,(LifeSpan s1)) = (card I) + n & DataPart (Comput (ProgramPart s1),s1,(LifeSpan s1)) = DataPart (Comput (ProgramPart s2),s2,(LifeSpan s1)) )
let I be shiftable No-StopCode Program of SCMPDS ; :: 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 = n & DataPart s1 = DataPart s2 holds
( IC (Comput (ProgramPart s2),s2,(LifeSpan s1)) = (card I) + n & DataPart (Comput (ProgramPart s1),s1,(LifeSpan s1)) = DataPart (Comput (ProgramPart s2),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 = n & DataPart s1 = DataPart s2 holds
( IC (Comput (ProgramPart s2),s2,(LifeSpan s1)) = (card I) + n & DataPart (Comput (ProgramPart s1),s1,(LifeSpan s1)) = DataPart (Comput (ProgramPart s2),s2,(LifeSpan s1)) )
let n be Element of NAT ; :: thesis: ( Shift I,n c= s2 & card I > 0 & IC s2 = n & DataPart s1 = DataPart s2 implies ( IC (Comput (ProgramPart s2),s2,(LifeSpan s1)) = (card I) + n & DataPart (Comput (ProgramPart s1),s1,(LifeSpan s1)) = DataPart (Comput (ProgramPart s2),s2,(LifeSpan s1)) ) )
assume that
A4: Shift I,n c= s2 and
A5: card I > 0 and
A6: IC s2 = n and
A7: DataPart s1 = DataPart s2 ; :: thesis: ( IC (Comput (ProgramPart s2),s2,(LifeSpan s1)) = (card I) + n & DataPart (Comput (ProgramPart s1),s1,(LifeSpan s1)) = DataPart (Comput (ProgramPart s2),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 (Comput (ProgramPart s1),s1,i)) + n = IC (Comput (ProgramPart s2),s2,i) by A1, A2, A3, A4, A5, A6, A7, Th34;
set L1 = IC (Comput (ProgramPart s1),s1,i);
A11: IC (Comput (ProgramPart s1),s1,i) in dom I by A1, A2, A3, A8, Th33, XREAL_1:31;
set i2 = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),(Comput (ProgramPart s2),s2,i);
T: ProgramPart s1 = ProgramPart (Comput (ProgramPart s1),s1,i) by AMI_1:144;
A12: Comput (ProgramPart s1),s1,(i + 1) = Following (ProgramPart s1),(Comput (ProgramPart s1),s1,i) by AMI_1:14
.= Exec (CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),(Comput (ProgramPart s2),s2,i)),(Comput (ProgramPart s1),s1,i) by A1, A2, A3, A4, A5, A6, A7, A9, Th34, T ;
A13: I c= Initialized (stop I) by SCMPDS_6:17;
then A14: dom I c= dom (Initialized (stop I)) by GRFUNC_1:8;
T: ProgramPart s2 = ProgramPart (Comput (ProgramPart s2),s2,i) by AMI_1:144;
A15: Comput (ProgramPart s2),s2,(i + 1) = Following (ProgramPart s2),(Comput (ProgramPart s2),s2,i) by AMI_1:14
.= Exec (CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),(Comput (ProgramPart s2),s2,i)),(Comput (ProgramPart s2),s2,i) by T ;
reconsider m = IC (Comput (ProgramPart s1),s1,i) as Element of NAT ;
Y: (ProgramPart (Comput (ProgramPart s1),s1,i)) /. (IC (Comput (ProgramPart s1),s1,i)) = (Comput (ProgramPart s1),s1,i) . (IC (Comput (ProgramPart s1),s1,i)) by AMI_1:150;
CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),(Comput (ProgramPart s2),s2,i) = CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i) by A1, A2, A3, A4, A5, A6, A7, A9, Th34;
then A17: CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),(Comput (ProgramPart s2),s2,i) = s1 . (IC (Comput (ProgramPart s1),s1,i)) by AMI_1:54, Y
.= (Initialized (stop I)) . (IC (Comput (ProgramPart s1),s1,i)) by A1, A11, A14, GRFUNC_1:8
.= I . (IC (Comput (ProgramPart s1),s1,i)) by A11, A13, GRFUNC_1:8 ;
then A18: InsCode (CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),(Comput (ProgramPart s2),s2,i)) <> 1 by A11, SCMPDS_4:def 12;
A19: DataPart (Comput (ProgramPart s1),s1,i) = DataPart (Comput (ProgramPart s2),s2,i) by A1, A2, A3, A4, A5, A6, A7, A9, Th34;
A20: CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),(Comput (ProgramPart s2),s2,i) valid_at m by A11, A17, SCMPDS_4:def 12;
A21: InsCode (CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),(Comput (ProgramPart s2),s2,i)) <> 3 by A11, A17, SCMPDS_4:def 12;
s1 = s1 +* (Initialized (stop I)) by A1, FUNCT_4:79;
then IC (Comput (ProgramPart s1),s1,(i + 1)) = card I by A2, A3, A8, SCMPDS_6:43;
hence IC (Comput (ProgramPart s2),s2,(LifeSpan s1)) = (card I) + n by A8, A10, A18, A21, A20, A12, A19, A15, SCMPDS_4:83
.= (card I) + n ;
:: thesis: DataPart (Comput (ProgramPart s1),s1,(LifeSpan s1)) = DataPart (Comput (ProgramPart s2),s2,(LifeSpan s1))
thus DataPart (Comput (ProgramPart s1),s1,(LifeSpan s1)) = DataPart (Comput (ProgramPart s2),s2,(LifeSpan s1)) by A8, A10, A18, A21, A20, A12, A19, A15, SCMPDS_4:83; :: thesis: verum