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 holds
for n being Element of NAT st Shift (stop I),n c= s2 & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Element of NAT 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 implies for n being Element of NAT st Shift (stop I),n c= s2 & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Element of NAT 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 ; :: thesis: for n being Element of NAT st Shift (stop I),n c= s2 & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Element of NAT 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 S1 = s1;
set S2 = s2;
let n be Element of NAT ; :: thesis: ( Shift (stop I),n c= s2 & IC s2 = n & DataPart s1 = DataPart s2 implies for i being Element of NAT 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) ) )
( Initialize (stop I) = (stop I) +* (Start-At 0 ,SCMPDS ) & dom (stop I) misses dom (Start-At 0 ,SCMPDS ) ) by SCMPDS_4:54;
then A3: stop I c= Initialize (stop I) by FUNCT_4:33;
then A4: dom (stop I) c= dom (Initialize (stop I)) by GRFUNC_1:8;
defpred S₁[ Element of NAT ] means ( (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) );
assume that
A5: Shift (stop I),n c= s2 and
A6: IC s2 = n and
A7: DataPart s1 = DataPart s2 ; :: thesis: for i being Element of NAT 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 Element of NAT ; :: thesis: ( (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) )
A8: DataPart (Comput (ProgramPart s1),s1,0 ) = DataPart s2 by A7, AMI_1:13
.= DataPart (Comput (ProgramPart s2),s2,0 ) by AMI_1:13 ;
A9: 0 in dom (stop I) by SCMPDS_4:75;
then A10: 0 + n in dom (Shift (stop I),n) by VALUED_1:25;
A11: IC SCMPDS in dom (Initialize (stop I)) by COMPOS_1:def 16;
then A12: 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, A4, A9, GRFUNC_1:8
.= (stop I) . 0 by A3, A9, GRFUNC_1:8 ;
I1: s1 +* (Initialize (stop I)) = (Initialize s1) +* (stop I) by SCMPDS_4:5;
A13: s1 = (Initialize s1) +* (stop I) by A1, I1, FUNCT_4:79;
A14: 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 A15: S₁[k] ; :: thesis: S₁[k + 1]
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);
T: 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 AMI_1:14
.= Exec (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,k)),(Comput (ProgramPart s1),s1,k)),(Comput (ProgramPart s1),s1,k) by T ;
reconsider l = IC (Comput (ProgramPart s1),s1,(k + 1)) as Element of NAT ;
A18: IC (Comput (ProgramPart s1),s1,(k + 1)) in dom (stop I) by A2, A13, Def2;
then A19: l + n in dom (Shift (stop I),n) by VALUED_1:25;
T: ProgramPart s2 = ProgramPart (Comput (ProgramPart s2),s2,k) by AMI_1:123;
A20: Comput (ProgramPart s2),s2,(k + 1) = Following (ProgramPart s2),(Comput (ProgramPart s2),s2,k) by AMI_1:14
.= Exec (CurInstr (ProgramPart (Comput (ProgramPart s2),s2,k)),(Comput (ProgramPart s2),s2,k)),(Comput (ProgramPart s2),s2,k) by T ;
A21: IC (Comput (ProgramPart s1),s1,k) in dom (stop I) by A2, A13, Def2;
Y: (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;
A22: CurInstr (ProgramPart (Comput (ProgramPart s1),s1,k)),(Comput (ProgramPart s1),s1,k) = s1 . (IC (Comput (ProgramPart s1),s1,k)) by Y, AMI_1:54
.= (Initialize (stop I)) . (IC (Comput (ProgramPart s1),s1,k)) by A1, A4, A21, GRFUNC_1:8
.= (stop I) . (IC (Comput (ProgramPart s1),s1,k)) by A3, A21, GRFUNC_1:8 ;
then A23: ( InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,k)),(Comput (ProgramPart s1),s1,k)) <> 1 & InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,k)),(Comput (ProgramPart s1),s1,k)) <> 3 ) by A21, SCMPDS_4:def 12;
A24: CurInstr (ProgramPart (Comput (ProgramPart s1),s1,k)),(Comput (ProgramPart s1),s1,k) valid_at m by A21, A22, SCMPDS_4:def 12;
hence A25: (IC (Comput (ProgramPart s1),s1,(k + 1))) + n = IC (Comput (ProgramPart s2),s2,(k + 1)) by A15, A16, A20, A23, SCMPDS_4:83; :: 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)) )
Y: (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;
Z: (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 Y, AMI_1:54
.= (Initialize (stop I)) . l by A1, A4, A18, GRFUNC_1:8
.= (stop I) . l by A3, A18, GRFUNC_1:8 ;
hence CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + 1))),(Comput (ProgramPart s1),s1,(k + 1)) = (Shift (stop I),n) . (IC (Comput (ProgramPart s2),s2,(k + 1))) by A25, A18, VALUED_1:def 12
.= s2 . (IC (Comput (ProgramPart s2),s2,(k + 1))) by A5, A25, A19, GRFUNC_1:8
.= CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(k + 1))),(Comput (ProgramPart s2),s2,(k + 1)) by Z, 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 A15, A16, A20, A23, A24, SCMPDS_4:83; :: thesis: verum

end;

A26: IC (Comput (ProgramPart s1),s1,0 ) = s1 . (IC SCMPDS ) by AMI_1:13
.= IC (Initialize (stop I)) by A1, A11, GRFUNC_1:8
.= 0 by COMPOS_1:def 16 ;
u: Comput (ProgramPart s1),s1,0 = s1 by AMI_1:13;
v: Comput (ProgramPart s2),s2,0 = s2 by AMI_1:13;
Y: (ProgramPart s2) /. (IC s2) = s2 . (IC s2) by COMPOS_1:38;
Z: (ProgramPart s1) /. (IC s1) = s1 . (IC s1) by COMPOS_1:38;
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,0 )),(Comput (ProgramPart s1),s1,0 ) = CurInstr (ProgramPart s1),s1 by u
.= (Shift (stop I),n) . (0 + n) by A9, A12, Z, VALUED_1:def 12
.= CurInstr (ProgramPart s2),s2 by A5, A6, A10, Y, GRFUNC_1:8
.= CurInstr (ProgramPart (Comput (ProgramPart s2),s2,0 )),(Comput (ProgramPart s2),s2,0 ) by v ;
then A27: S₁[ 0 ] by A6, A26, A8, AMI_1:13;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A27, A14);
hence ( (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