let s1, s2 be State of SCMPDS; for I being halt-free shiftable Program of SCMPDS st Initialize (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 ((ProgramPart s1),s1)))) = (card I) + n & DataPart (Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1)))) = DataPart (Comput ((ProgramPart s2),s2,(LifeSpan ((ProgramPart s1),s1)))) )
let I be halt-free shiftable Program of SCMPDS; ( Initialize (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 ((ProgramPart s1),s1)))) = (card I) + n & DataPart (Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1)))) = DataPart (Comput ((ProgramPart s2),s2,(LifeSpan ((ProgramPart s1),s1)))) ) )
assume that
A1:
Initialize (stop I) c= s1
and
A2:
I is_closed_on s1
and
A3:
I is_halting_on s1
; 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 ((ProgramPart s1),s1)))) = (card I) + n & DataPart (Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1)))) = DataPart (Comput ((ProgramPart s2),s2,(LifeSpan ((ProgramPart s1),s1)))) )
let n be Element of NAT ; ( Shift (I,n) c= s2 & card I > 0 & IC s2 = n & DataPart s1 = DataPart s2 implies ( IC (Comput ((ProgramPart s2),s2,(LifeSpan ((ProgramPart s1),s1)))) = (card I) + n & DataPart (Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1)))) = DataPart (Comput ((ProgramPart s2),s2,(LifeSpan ((ProgramPart s1),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
; ( IC (Comput ((ProgramPart s2),s2,(LifeSpan ((ProgramPart s1),s1)))) = (card I) + n & DataPart (Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1)))) = DataPart (Comput ((ProgramPart s2),s2,(LifeSpan ((ProgramPart s1),s1)))) )
1 + 0 <= LifeSpan ((ProgramPart s1),s1)
by A1, A3, A5, Th35, INT_1:20;
then consider i being Nat such that
A8:
1 + i = LifeSpan ((ProgramPart s1),s1)
by NAT_1:10;
I1:
(Initialize s1) +* (stop I) = s1 +* (Initialize (stop I))
by COMPOS_1:125;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
A9:
i < LifeSpan ((ProgramPart s1),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:123;
A12: Comput ((ProgramPart s1),s1,(i + 1)) =
Following ((ProgramPart s1),(Comput ((ProgramPart s1),s1,i)))
by EXTPRO_1:4
.=
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= Initialize (stop I)
by SCMPDS_6:17;
then A14:
dom I c= dom (Initialize (stop I))
by GRFUNC_1:8;
T:
ProgramPart s2 = ProgramPart (Comput ((ProgramPart s2),s2,i))
by AMI_1:123;
A15: Comput ((ProgramPart s2),s2,(i + 1)) =
Following ((ProgramPart s2),(Comput ((ProgramPart s2),s2,i)))
by EXTPRO_1:4
.=
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 COMPOS_1:38;
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 Y, AMI_1:54
.=
(Initialize (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 = (Initialize s1) +* (stop I)
by A1, I1, FUNCT_4:79;
then
IC (Comput ((ProgramPart s1),s1,(i + 1))) = card I
by A2, A3, A8, I1, SCMPDS_6:43;
hence IC (Comput ((ProgramPart s2),s2,(LifeSpan ((ProgramPart s1),s1)))) =
(card I) + n
by A8, A10, A18, A21, A20, A12, A19, A15, SCMPDS_4:83
.=
(card I) + n
;
DataPart (Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1)))) = DataPart (Comput ((ProgramPart s2),s2,(LifeSpan ((ProgramPart s1),s1))))
thus
DataPart (Comput ((ProgramPart s1),s1,(LifeSpan ((ProgramPart s1),s1)))) = DataPart (Comput ((ProgramPart s2),s2,(LifeSpan ((ProgramPart s1),s1))))
by A8, A10, A18, A21, A20, A12, A19, A15, SCMPDS_4:83; verum