let s2 be State of SCMPDS; :: thesis: for P1, P2 being Instruction-Sequence of SCMPDS

for s1 being 0 -started State of SCMPDS

for J being parahalting shiftable Program of st stop J c= P1 holds

for n being Nat st Shift ((stop J),n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds

for i being Nat holds

( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )

let P1, P2 be Instruction-Sequence of SCMPDS; :: thesis: for s1 being 0 -started State of SCMPDS

for J being parahalting shiftable Program of st stop J c= P1 holds

for n being Nat st Shift ((stop J),n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds

for i being Nat holds

( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )

let s1 be 0 -started State of SCMPDS; :: thesis: for J being parahalting shiftable Program of st stop J c= P1 holds

for n being Nat st Shift ((stop J),n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds

for i being Nat holds

( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )

let I be parahalting shiftable Program of ; :: thesis: ( stop I c= P1 implies for n being Nat st Shift ((stop I),n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds

for i being Nat holds

( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) ) )

set SI = stop I;

assume A1: stop I c= P1 ; :: thesis: for n being Nat st Shift ((stop I),n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds

for i being Nat holds

( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )

let n be Nat; :: thesis: ( Shift ((stop I),n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 implies for i being Nat holds

( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) ) )

assume that

A2: Shift ((stop I),n) c= P2 and

A3: IC s2 = n and

A4: DataPart s1 = DataPart s2 ; :: thesis: for i being Nat holds

( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )

A5: 0 in dom (stop I) by COMPOS_1:36;

then A6: 0 + n in dom (Shift ((stop I),n)) by VALUED_1:24;

defpred S_{1}[ Nat] means ( (IC (Comput (P1,s1,$1))) + n = IC (Comput (P2,s2,$1)) & CurInstr (P1,(Comput (P1,s1,$1))) = CurInstr (P2,(Comput (P2,s2,$1))) & DataPart (Comput (P1,s1,$1)) = DataPart (Comput (P2,s2,$1)) );

A7: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

.= (stop I) . 0 by A1, A5, GRFUNC_1:2 ;

let i be Nat; :: thesis: ( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )

A19: DataPart (Comput (P1,s1,0)) = DataPart s2 by A4

.= DataPart (Comput (P2,s2,0)) ;

A20: IC (Comput (P1,s1,0)) = IC s1

.= 0 by MEMSTR_0:def 11 ;

A21: P2 /. (IC s2) = P2 . (IC s2) by PBOOLE:143;

A22: P1 /. (IC s1) = P1 . (IC s1) by PBOOLE:143;

CurInstr (P1,(Comput (P1,s1,0))) = CurInstr (P1,s1)

.= (Shift ((stop I),n)) . (0 + n) by A5, A18, A22, VALUED_1:def 12

.= CurInstr (P2,(Comput (P2,s2,0))) by A2, A3, A6, A21, GRFUNC_1:2 ;

then A23: S_{1}[ 0 ]
by A3, A20, A19;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A23, A7);

hence ( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) ) ; :: thesis: verum

for s1 being 0 -started State of SCMPDS

for J being parahalting shiftable Program of st stop J c= P1 holds

for n being Nat st Shift ((stop J),n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds

for i being Nat holds

( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )

let P1, P2 be Instruction-Sequence of SCMPDS; :: thesis: for s1 being 0 -started State of SCMPDS

for J being parahalting shiftable Program of st stop J c= P1 holds

for n being Nat st Shift ((stop J),n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds

for i being Nat holds

( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )

let s1 be 0 -started State of SCMPDS; :: thesis: for J being parahalting shiftable Program of st stop J c= P1 holds

for n being Nat st Shift ((stop J),n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds

for i being Nat holds

( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )

let I be parahalting shiftable Program of ; :: thesis: ( stop I c= P1 implies for n being Nat st Shift ((stop I),n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds

for i being Nat holds

( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) ) )

set SI = stop I;

assume A1: stop I c= P1 ; :: thesis: for n being Nat st Shift ((stop I),n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds

for i being Nat holds

( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )

let n be Nat; :: thesis: ( Shift ((stop I),n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 implies for i being Nat holds

( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) ) )

assume that

A2: Shift ((stop I),n) c= P2 and

A3: IC s2 = n and

A4: DataPart s1 = DataPart s2 ; :: thesis: for i being Nat holds

( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )

A5: 0 in dom (stop I) by COMPOS_1:36;

then A6: 0 + n in dom (Shift ((stop I),n)) by VALUED_1:24;

defpred S

A7: for k being Nat st S

S

proof

A18: P1 . (IC s1) =
P1 . 0
by MEMSTR_0:def 11
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A8: S_{1}[k]
; :: thesis: S_{1}[k + 1]

reconsider m = IC (Comput (P1,s1,k)) as Nat ;

set i = CurInstr (P1,(Comput (P1,s1,k)));

A9: Comput (P1,s1,(k + 1)) = Following (P1,(Comput (P1,s1,k))) by EXTPRO_1:3

.= Exec ((CurInstr (P1,(Comput (P1,s1,k)))),(Comput (P1,s1,k))) ;

reconsider l = IC (Comput (P1,s1,(k + 1))) as Nat ;

A10: IC (Comput (P1,s1,(k + 1))) in dom (stop I) by A1, Def6;

then A11: l + n in dom (Shift ((stop I),n)) by VALUED_1:24;

A12: Comput (P2,s2,(k + 1)) = Following (P2,(Comput (P2,s2,k))) by EXTPRO_1:3

.= Exec ((CurInstr (P2,(Comput (P2,s2,k)))),(Comput (P2,s2,k))) ;

A13: IC (Comput (P1,s1,k)) in dom (stop I) by A1, Def6;

A14: CurInstr (P1,(Comput (P1,s1,k))) = P1 . (IC (Comput (P1,s1,k))) by PBOOLE:143

.= (stop I) . (IC (Comput (P1,s1,k))) by A1, A13, GRFUNC_1:2 ;

then A15: ( InsCode (CurInstr (P1,(Comput (P1,s1,k)))) <> 1 & InsCode (CurInstr (P1,(Comput (P1,s1,k)))) <> 3 ) by A13, Def9;

A16: CurInstr (P1,(Comput (P1,s1,k))) valid_at m by A13, A14, Def9;

hence A17: (IC (Comput (P1,s1,(k + 1)))) + n = IC (Comput (P2,s2,(k + 1))) by A8, A9, A12, A15, Th26; :: thesis: ( CurInstr (P1,(Comput (P1,s1,(k + 1)))) = CurInstr (P2,(Comput (P2,s2,(k + 1)))) & DataPart (Comput (P1,s1,(k + 1))) = DataPart (Comput (P2,s2,(k + 1))) )

CurInstr (P1,(Comput (P1,s1,(k + 1)))) = P1 . l by PBOOLE:143

.= (stop I) . l by A1, A10, GRFUNC_1:2 ;

hence CurInstr (P1,(Comput (P1,s1,(k + 1)))) = (Shift ((stop I),n)) . (IC (Comput (P2,s2,(k + 1)))) by A17, A10, VALUED_1:def 12

.= P2 . (IC (Comput (P2,s2,(k + 1)))) by A2, A17, A11, GRFUNC_1:2

.= CurInstr (P2,(Comput (P2,s2,(k + 1)))) by PBOOLE:143 ;

:: thesis: DataPart (Comput (P1,s1,(k + 1))) = DataPart (Comput (P2,s2,(k + 1)))

thus DataPart (Comput (P1,s1,(k + 1))) = DataPart (Comput (P2,s2,(k + 1))) by A8, A9, A12, A15, A16, Th26; :: thesis: verum

end;assume A8: S

reconsider m = IC (Comput (P1,s1,k)) as Nat ;

set i = CurInstr (P1,(Comput (P1,s1,k)));

A9: Comput (P1,s1,(k + 1)) = Following (P1,(Comput (P1,s1,k))) by EXTPRO_1:3

.= Exec ((CurInstr (P1,(Comput (P1,s1,k)))),(Comput (P1,s1,k))) ;

reconsider l = IC (Comput (P1,s1,(k + 1))) as Nat ;

A10: IC (Comput (P1,s1,(k + 1))) in dom (stop I) by A1, Def6;

then A11: l + n in dom (Shift ((stop I),n)) by VALUED_1:24;

A12: Comput (P2,s2,(k + 1)) = Following (P2,(Comput (P2,s2,k))) by EXTPRO_1:3

.= Exec ((CurInstr (P2,(Comput (P2,s2,k)))),(Comput (P2,s2,k))) ;

A13: IC (Comput (P1,s1,k)) in dom (stop I) by A1, Def6;

A14: CurInstr (P1,(Comput (P1,s1,k))) = P1 . (IC (Comput (P1,s1,k))) by PBOOLE:143

.= (stop I) . (IC (Comput (P1,s1,k))) by A1, A13, GRFUNC_1:2 ;

then A15: ( InsCode (CurInstr (P1,(Comput (P1,s1,k)))) <> 1 & InsCode (CurInstr (P1,(Comput (P1,s1,k)))) <> 3 ) by A13, Def9;

A16: CurInstr (P1,(Comput (P1,s1,k))) valid_at m by A13, A14, Def9;

hence A17: (IC (Comput (P1,s1,(k + 1)))) + n = IC (Comput (P2,s2,(k + 1))) by A8, A9, A12, A15, Th26; :: thesis: ( CurInstr (P1,(Comput (P1,s1,(k + 1)))) = CurInstr (P2,(Comput (P2,s2,(k + 1)))) & DataPart (Comput (P1,s1,(k + 1))) = DataPart (Comput (P2,s2,(k + 1))) )

CurInstr (P1,(Comput (P1,s1,(k + 1)))) = P1 . l by PBOOLE:143

.= (stop I) . l by A1, A10, GRFUNC_1:2 ;

hence CurInstr (P1,(Comput (P1,s1,(k + 1)))) = (Shift ((stop I),n)) . (IC (Comput (P2,s2,(k + 1)))) by A17, A10, VALUED_1:def 12

.= P2 . (IC (Comput (P2,s2,(k + 1)))) by A2, A17, A11, GRFUNC_1:2

.= CurInstr (P2,(Comput (P2,s2,(k + 1)))) by PBOOLE:143 ;

:: thesis: DataPart (Comput (P1,s1,(k + 1))) = DataPart (Comput (P2,s2,(k + 1)))

thus DataPart (Comput (P1,s1,(k + 1))) = DataPart (Comput (P2,s2,(k + 1))) by A8, A9, A12, A15, A16, Th26; :: thesis: verum

.= (stop I) . 0 by A1, A5, GRFUNC_1:2 ;

let i be Nat; :: thesis: ( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )

A19: DataPart (Comput (P1,s1,0)) = DataPart s2 by A4

.= DataPart (Comput (P2,s2,0)) ;

A20: IC (Comput (P1,s1,0)) = IC s1

.= 0 by MEMSTR_0:def 11 ;

A21: P2 /. (IC s2) = P2 . (IC s2) by PBOOLE:143;

A22: P1 /. (IC s1) = P1 . (IC s1) by PBOOLE:143;

CurInstr (P1,(Comput (P1,s1,0))) = CurInstr (P1,s1)

.= (Shift ((stop I),n)) . (0 + n) by A5, A18, A22, VALUED_1:def 12

.= CurInstr (P2,(Comput (P2,s2,0))) by A2, A3, A6, A21, GRFUNC_1:2 ;

then A23: S

for k being Nat holds S

hence ( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) ) ; :: thesis: verum