let s1, s2 be State of SCMPDS; :: thesis: for I being 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
for i being Element of NAT st i < LifeSpan ((ProgramPart s1),s1) holds
( (IC (Comput ((ProgramPart s1),s1,i))) + n = IC (Comput ((ProgramPart s2),s2,i)) & CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i))) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) )
let I be shiftable Program of SCMPDS; :: thesis: ( 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
for i being Element of NAT st i < LifeSpan ((ProgramPart s1),s1) holds
( (IC (Comput ((ProgramPart s1),s1,i))) + n = IC (Comput ((ProgramPart s2),s2,i)) & CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i))) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) ) )
set SI = stop I;
assume that
A1: Initialize (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
for i being Element of NAT st i < LifeSpan ((ProgramPart s1),s1) holds
( (IC (Comput ((ProgramPart s1),s1,i))) + n = IC (Comput ((ProgramPart s2),s2,i)) & CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i))) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) )
dom (stop I) misses dom (Start-At (0,SCMPDS)) by COMPOS_1:130;
then A4: stop I c= Initialize (stop I) by FUNCT_4:33;
then A5: dom (stop I) c= dom (Initialize (stop I)) by GRFUNC_1:8;
let n be Element of NAT ; :: thesis: ( Shift (I,n) c= s2 & card I > 0 & IC s2 = n & DataPart s1 = DataPart s2 implies for i being Element of NAT st i < LifeSpan ((ProgramPart s1),s1) holds
( (IC (Comput ((ProgramPart s1),s1,i))) + n = IC (Comput ((ProgramPart s2),s2,i)) & CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i))) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) ) )
assume that
A6: Shift (I,n) c= s2 and
A7: card I > 0 and
A8: IC s2 = n and
A9: DataPart s1 = DataPart s2 ; :: thesis: for i being Element of NAT st i < LifeSpan ((ProgramPart s1),s1) holds
( (IC (Comput ((ProgramPart s1),s1,i))) + n = IC (Comput ((ProgramPart s2),s2,i)) & CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i))) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) )
defpred S₁[ Element of NAT ] means ( $1 < LifeSpan ((ProgramPart s1),s1) implies ( (IC (Comput ((ProgramPart s1),s1,$1))) + n = IC (Comput ((ProgramPart s2),s2,$1)) & CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,$1))),(Comput ((ProgramPart s1),s1,$1))) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,$1))),(Comput ((ProgramPart s2),s2,$1))) & DataPart (Comput ((ProgramPart s1),s1,$1)) = DataPart (Comput ((ProgramPart s2),s2,$1)) ) );
A10: (Initialize s1) +* (stop I) = s1 +* (Initialize (stop I)) by COMPOS_1:125;
A11: s1 = (Initialize s1) +* (stop I) by A1, A10, FUNCT_4:79;
A12: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A13: S₁[k] ; :: thesis: S₁[k + 1]

now

reconsider m = IC (Comput ((ProgramPart s1),s1,k)) as Element of NAT ;
set i = CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,k))),(Comput ((ProgramPart s1),s1,k)));
A14: k <= k + 1 by NAT_1:11;
reconsider l = IC (Comput ((ProgramPart s1),s1,(k + 1))) as Element of NAT ;
A15: ProgramPart s1 = ProgramPart (Comput ((ProgramPart s1),s1,k)) by AMI_1:123;
A16: Comput ((ProgramPart s1),s1,(k + 1)) = Following ((ProgramPart s1),(Comput ((ProgramPart s1),s1,k))) by EXTPRO_1:4
.= Exec ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,k))),(Comput ((ProgramPart s1),s1,k)))),(Comput ((ProgramPart s1),s1,k))) by A15 ;
assume A17: k + 1 < LifeSpan ((ProgramPart s1),s1) ; :: thesis: ( (IC (Comput ((ProgramPart s1),s1,(k + 1)))) + n = IC (Comput ((ProgramPart s2),s2,(k + 1))) & CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,(k + 1)))),(Comput ((ProgramPart s1),s1,(k + 1)))) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,(k + 1)))),(Comput ((ProgramPart s2),s2,(k + 1)))) & DataPart (Comput ((ProgramPart s1),s1,(k + 1))) = DataPart (Comput ((ProgramPart s2),s2,(k + 1))) )
then A18: IC (Comput ((ProgramPart s1),s1,(k + 1))) in dom I by A1, A2, A3, Th33;
then A19: l + n in dom (Shift (I,n)) by VALUED_1:25;
A20: ProgramPart s2 = ProgramPart (Comput ((ProgramPart s2),s2,k)) by AMI_1:123;
A21: Comput ((ProgramPart s2),s2,(k + 1)) = Following ((ProgramPart s2),(Comput ((ProgramPart s2),s2,k))) by EXTPRO_1:4
.= Exec ((CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,k))),(Comput ((ProgramPart s2),s2,k)))),(Comput ((ProgramPart s2),s2,k))) by A20 ;
A22: IC (Comput ((ProgramPart s1),s1,k)) in dom (stop I) by A2, A11, SCMPDS_6:def 2;
A23: (ProgramPart (Comput ((ProgramPart s1),s1,k))) /. (IC (Comput ((ProgramPart s1),s1,k))) = (Comput ((ProgramPart s1),s1,k)) . (IC (Comput ((ProgramPart s1),s1,k))) by COMPOS_1:38;
A24: CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,k))),(Comput ((ProgramPart s1),s1,k))) = s1 . (IC (Comput ((ProgramPart s1),s1,k))) by A23, AMI_1:54
.= (Initialize (stop I)) . (IC (Comput ((ProgramPart s1),s1,k))) by A1, A5, A22, GRFUNC_1:8
.= (stop I) . (IC (Comput ((ProgramPart s1),s1,k))) by A4, A22, GRFUNC_1:8 ;
then A25: InsCode (CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,k))),(Comput ((ProgramPart s1),s1,k)))) <> 3 by A22, SCMPDS_4:def 12;
A26: IC (Comput ((ProgramPart s1),s1,(k + 1))) in dom (stop I) by A2, A11, SCMPDS_6:def 2;
A27: CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,k))),(Comput ((ProgramPart s1),s1,k))) valid_at m by A22, A24, SCMPDS_4:def 12;
A28: InsCode (CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,k))),(Comput ((ProgramPart s1),s1,k)))) <> 1 by A22, A24, SCMPDS_4:def 12;
hence A29: (IC (Comput ((ProgramPart s1),s1,(k + 1)))) + n = IC (Comput ((ProgramPart s2),s2,(k + 1))) by A13, A17, A14, A16, A21, A25, A27, SCMPDS_4:83, XXREAL_0:2; :: thesis: ( CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,(k + 1)))),(Comput ((ProgramPart s1),s1,(k + 1)))) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,(k + 1)))),(Comput ((ProgramPart s2),s2,(k + 1)))) & DataPart (Comput ((ProgramPart s1),s1,(k + 1))) = DataPart (Comput ((ProgramPart s2),s2,(k + 1))) )
A30: (ProgramPart (Comput ((ProgramPart s1),s1,(k + 1)))) /. (IC (Comput ((ProgramPart s1),s1,(k + 1)))) = (Comput ((ProgramPart s1),s1,(k + 1))) . (IC (Comput ((ProgramPart s1),s1,(k + 1)))) by COMPOS_1:38;
A31: (ProgramPart (Comput ((ProgramPart s2),s2,(k + 1)))) /. (IC (Comput ((ProgramPart s2),s2,(k + 1)))) = (Comput ((ProgramPart s2),s2,(k + 1))) . (IC (Comput ((ProgramPart s2),s2,(k + 1)))) by COMPOS_1:38;
CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,(k + 1)))),(Comput ((ProgramPart s1),s1,(k + 1)))) = s1 . l by A30, AMI_1:54
.= (Initialize (stop I)) . l by A1, A5, A26, GRFUNC_1:8
.= (stop I) . l by A4, A26, GRFUNC_1:8 ;
hence CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,(k + 1)))),(Comput ((ProgramPart s1),s1,(k + 1)))) = (Shift ((stop I),n)) . (l + n) by A26, VALUED_1:def 12
.= (Shift (I,n)) . (IC (Comput ((ProgramPart s2),s2,(k + 1)))) by A29, A18, Th18
.= s2 . (IC (Comput ((ProgramPart s2),s2,(k + 1)))) by A6, A29, A19, GRFUNC_1:8
.= CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,(k + 1)))),(Comput ((ProgramPart s2),s2,(k + 1)))) by A31, AMI_1:54 ;
:: thesis: DataPart (Comput ((ProgramPart s1),s1,(k + 1))) = DataPart (Comput ((ProgramPart s2),s2,(k + 1)))
thus DataPart (Comput ((ProgramPart s1),s1,(k + 1))) = DataPart (Comput ((ProgramPart s2),s2,(k + 1))) by A13, A17, A14, A16, A21, A28, A25, A27, SCMPDS_4:83, XXREAL_0:2; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

let i be Element of NAT ; :: thesis: ( i < LifeSpan ((ProgramPart s1),s1) implies ( (IC (Comput ((ProgramPart s1),s1,i))) + n = IC (Comput ((ProgramPart s2),s2,i)) & CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i))) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) ) )
A32: 0 in dom (stop I) by COMPOS_1:135;
A33: 0 in dom I by A7, AFINSQ_1:70;
A34: S₁[ 0 ]

proof

assume 0 < LifeSpan ((ProgramPart s1),s1) ; :: thesis: ( (IC (Comput ((ProgramPart s1),s1,0))) + n = IC (Comput ((ProgramPart s2),s2,0)) & CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,0))),(Comput ((ProgramPart s1),s1,0))) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,0))),(Comput ((ProgramPart s2),s2,0))) & DataPart (Comput ((ProgramPart s1),s1,0)) = DataPart (Comput ((ProgramPart s2),s2,0)) )
A35: 0 + n in dom (Shift (I,n)) by A33, VALUED_1:25;
A36: IC in dom (Initialize (stop I)) by COMPOS_1:def 16;
then A37: s1 . (IC s1) = s1 . (IC (Initialize (stop I))) by A1, GRFUNC_1:8
.= s1 . 0 by COMPOS_1:def 16
.= (Initialize (stop I)) . 0 by A1, A5, A32, GRFUNC_1:8
.= (stop I) . 0 by A4, A32, GRFUNC_1:8 ;
IC (Comput ((ProgramPart s1),s1,0)) = s1 . (IC ) by EXTPRO_1:3
.= IC (Initialize (stop I)) by A1, A36, GRFUNC_1:8
.= 0 by COMPOS_1:def 16 ;
hence (IC (Comput ((ProgramPart s1),s1,0))) + n = 0 + n
.= IC (Comput ((ProgramPart s2),s2,0)) by A8, EXTPRO_1:3 ;
:: thesis: ( CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,0))),(Comput ((ProgramPart s1),s1,0))) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,0))),(Comput ((ProgramPart s2),s2,0))) & DataPart (Comput ((ProgramPart s1),s1,0)) = DataPart (Comput ((ProgramPart s2),s2,0)) )
A38: Comput ((ProgramPart s1),s1,0) = s1 by EXTPRO_1:3;
A39: Comput ((ProgramPart s2),s2,0) = s2 by EXTPRO_1:3;
A40: (ProgramPart s1) /. (IC s1) = s1 . (IC s1) by COMPOS_1:38;
A41: (ProgramPart s2) /. (IC s2) = s2 . (IC s2) by COMPOS_1:38;
thus CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,0))),(Comput ((ProgramPart s1),s1,0))) = CurInstr ((ProgramPart s1),s1) by A38
.= (Shift ((stop I),n)) . (0 + n) by A32, A37, A40, VALUED_1:def 12
.= (Shift ((stop I),n)) . (0 + n)
.= (Shift (I,n)) . n by A7, Th19
.= CurInstr ((ProgramPart s2),s2) by A6, A8, A35, A41, GRFUNC_1:8
.= CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,0))),(Comput ((ProgramPart s2),s2,0))) by A39 ; :: thesis: DataPart (Comput ((ProgramPart s1),s1,0)) = DataPart (Comput ((ProgramPart s2),s2,0))
thus DataPart (Comput ((ProgramPart s1),s1,0)) = DataPart s2 by A9, EXTPRO_1:3
.= DataPart (Comput ((ProgramPart s2),s2,0)) by EXTPRO_1:3 ; :: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A34, A12);
hence ( i < LifeSpan ((ProgramPart s1),s1) implies ( (IC (Comput ((ProgramPart s1),s1,i))) + n = IC (Comput ((ProgramPart s2),s2,i)) & CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i))) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) ) ) ; :: thesis: verum