let s2 be State of SCMPDS; :: thesis: for s1 being 0 -started State of SCMPDS
for J being parahalting shiftable Program of SCMPDS st stop J c= s1 holds
for n being Element of NAT st Shift ((stop J),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 s1),(Comput ((ProgramPart s1),s1,i))) = CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,i))) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) )
let s1 be 0 -started State of SCMPDS; :: thesis: for J being parahalting shiftable Program of SCMPDS st stop J c= s1 holds
for n being Element of NAT st Shift ((stop J),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 s1),(Comput ((ProgramPart s1),s1,i))) = CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,i))) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) )
let I be parahalting shiftable Program of SCMPDS; :: thesis: ( stop I c= 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 s1),(Comput ((ProgramPart s1),s1,i))) = CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,i))) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) ) )
set SI = stop I;
set II = Initialize (stop I);
assume A1: stop I c= 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 s1),(Comput ((ProgramPart s1),s1,i))) = CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,i))) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) )
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 s1),(Comput ((ProgramPart s1),s1,i))) = CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,i))) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) ) )
assume that
A2: Shift ((stop I),n) c= s2 and
A3: IC s2 = n and
A4: 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 s1),(Comput ((ProgramPart s1),s1,i))) = CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,i))) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) )
A5: 0 in dom (stop I) by COMPOS_1:135;
then A6: 0 + n in dom (Shift ((stop I),n)) by VALUED_1:25;
defpred S₁[ Nat] means ( (IC (Comput ((ProgramPart s1),s1,$1))) + n = IC (Comput ((ProgramPart s2),s2,$1)) & CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,$1))) = CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,$1))) & DataPart (Comput ((ProgramPart s1),s1,$1)) = DataPart (Comput ((ProgramPart s2),s2,$1)) );
A9: 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 A10: S₁[k] ; :: thesis: S₁[k + 1]
reconsider m = IC (Comput ((ProgramPart s1),s1,k)) as Element of NAT ;
set i = CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,k)));
A11: Comput ((ProgramPart s1),s1,(k + 1)) = Following ((ProgramPart s1),(Comput ((ProgramPart s1),s1,k))) by EXTPRO_1:4
.= Exec ((CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,k)))),(Comput ((ProgramPart s1),s1,k))) ;
reconsider l = IC (Comput ((ProgramPart s1),s1,(k + 1))) as Element of NAT ;
A13: IC (Comput ((ProgramPart s1),s1,(k + 1))) in dom (stop I) by A1, Def9;
then A14: l + n in dom (Shift ((stop I),n)) by VALUED_1:25;
A15: Comput ((ProgramPart s2),s2,(k + 1)) = Following ((ProgramPart s2),(Comput ((ProgramPart s2),s2,k))) by EXTPRO_1:4
.= Exec ((CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,k)))),(Comput ((ProgramPart s2),s2,k))) ;
A16: IC (Comput ((ProgramPart s1),s1,k)) in dom (stop I) by A1, Def9;
A17: CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,k))) = s1 . (IC (Comput ((ProgramPart s1),s1,k))) by COMPOS_1:38
.= (stop I) . (IC (Comput ((ProgramPart s1),s1,k))) by A1, A16, GRFUNC_1:8 ;
then A18: ( InsCode (CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,k)))) <> 1 & InsCode (CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,k)))) <> 3 ) by A16, Def12;
A19: CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,k))) valid_at m by A16, A17, Def12;
hence A20: (IC (Comput ((ProgramPart s1),s1,(k + 1)))) + n = IC (Comput ((ProgramPart s2),s2,(k + 1))) by A10, A11, A15, A18, Th83; :: thesis: ( CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,(k + 1)))) = CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,(k + 1)))) & DataPart (Comput ((ProgramPart s1),s1,(k + 1))) = DataPart (Comput ((ProgramPart s2),s2,(k + 1))) )
CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,(k + 1)))) = s1 . l by COMPOS_1:38
.= (stop I) . l by A1, A13, GRFUNC_1:8 ;
hence CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,(k + 1)))) = (Shift ((stop I),n)) . (IC (Comput ((ProgramPart s2),s2,(k + 1)))) by A20, A13, VALUED_1:def 12
.= s2 . (IC (Comput ((ProgramPart s2),s2,(k + 1)))) by A2, A20, A14, GRFUNC_1:8
.= CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,(k + 1)))) by COMPOS_1:38 ;
:: 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 A10, A11, A15, A18, A19, Th83; :: thesis: verum

end;

A22: s1 . (IC s1) = s1 . 0 by COMPOS_1:def 16
.= (stop I) . 0 by A1, A5, GRFUNC_1:8 ;
let i be Element of NAT ; :: thesis: ( (IC (Comput ((ProgramPart s1),s1,i))) + n = IC (Comput ((ProgramPart s2),s2,i)) & CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,i))) = CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,i))) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) )
A23: DataPart (Comput ((ProgramPart s1),s1,0)) = DataPart s2 by A4, EXTPRO_1:3
.= DataPart (Comput ((ProgramPart s2),s2,0)) by EXTPRO_1:3 ;
A24: IC (Comput ((ProgramPart s1),s1,0)) = IC s1 by EXTPRO_1:3
.= 0 by COMPOS_1:def 16 ;
u: Comput ((ProgramPart s1),s1,0) = s1 by EXTPRO_1:3;
v: Comput ((ProgramPart s2),s2,0) = s2 by EXTPRO_1:3;
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 s1),(Comput ((ProgramPart s1),s1,0))) = (Shift ((stop I),n)) . (0 + n) by A5, A22, Z, u, VALUED_1:def 12
.= CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,0))) by v, A2, A3, A6, Y, GRFUNC_1:8 ;
then A25: S₁[ 0 ] by A3, A24, A23, EXTPRO_1:3;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A25, A9);
hence ( (IC (Comput ((ProgramPart s1),s1,i))) + n = IC (Comput ((ProgramPart s2),s2,i)) & CurInstr ((ProgramPart s1),(Comput ((ProgramPart s1),s1,i))) = CurInstr ((ProgramPart s2),(Comput ((ProgramPart s2),s2,i))) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) ) ; :: thesis: verum