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

for s1 being 0 -started State of SCMPDS

for I being shiftable Program of st stop I c= P1 & I is_closed_on s1,P1 & I is_halting_on s1,P1 holds

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

for i being Nat st i < LifeSpan (P1,s1) 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 I being shiftable Program of st stop I c= P1 & I is_closed_on s1,P1 & I is_halting_on s1,P1 holds

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

for i being Nat st i < LifeSpan (P1,s1) 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 I being shiftable Program of st stop I c= P1 & I is_closed_on s1,P1 & I is_halting_on s1,P1 holds

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

for i being Nat st i < LifeSpan (P1,s1) 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 shiftable Program of ; :: thesis: ( stop I c= P1 & I is_closed_on s1,P1 & I is_halting_on s1,P1 implies for n being Nat st Shift (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds

for i being Nat st i < LifeSpan (P1,s1) 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 that

A1: stop I c= P1 and

A2: I is_closed_on s1,P1 and

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

for i being Nat st i < LifeSpan (P1,s1) 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)) )

A4: Start-At (0,SCMPDS) c= s1 by MEMSTR_0:29;

let n be Nat; :: thesis: ( Shift (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 implies for i being Nat st i < LifeSpan (P1,s1) 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

A6: Shift (I,n) c= P2 and

A7: IC s2 = n and

A8: DataPart s1 = DataPart s2 ; :: thesis: for i being Nat st i < LifeSpan (P1,s1) 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)) )

defpred S_{1}[ Nat] means ( $1 < LifeSpan (P1,s1) implies ( (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)) ) );

A9: s1 = Initialize s1 by A4, FUNCT_4:98;

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

S_{1}[k + 1]

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

A26: 0 in dom I by AFINSQ_1:66;

A27: S_{1}[ 0 ]
_{1}[k]
from NAT_1:sch 2(A27, A10);

hence ( i < LifeSpan (P1,s1) implies ( (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 I being shiftable Program of st stop I c= P1 & I is_closed_on s1,P1 & I is_halting_on s1,P1 holds

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

for i being Nat st i < LifeSpan (P1,s1) 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 I being shiftable Program of st stop I c= P1 & I is_closed_on s1,P1 & I is_halting_on s1,P1 holds

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

for i being Nat st i < LifeSpan (P1,s1) 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 I being shiftable Program of st stop I c= P1 & I is_closed_on s1,P1 & I is_halting_on s1,P1 holds

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

for i being Nat st i < LifeSpan (P1,s1) 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 shiftable Program of ; :: thesis: ( stop I c= P1 & I is_closed_on s1,P1 & I is_halting_on s1,P1 implies for n being Nat st Shift (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds

for i being Nat st i < LifeSpan (P1,s1) 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 that

A1: stop I c= P1 and

A2: I is_closed_on s1,P1 and

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

for i being Nat st i < LifeSpan (P1,s1) 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)) )

A4: Start-At (0,SCMPDS) c= s1 by MEMSTR_0:29;

let n be Nat; :: thesis: ( Shift (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 implies for i being Nat st i < LifeSpan (P1,s1) 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

A6: Shift (I,n) c= P2 and

A7: IC s2 = n and

A8: DataPart s1 = DataPart s2 ; :: thesis: for i being Nat st i < LifeSpan (P1,s1) 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)) )

defpred S

A9: s1 = Initialize s1 by A4, FUNCT_4:98;

A10: for k being Nat st S

S

proof

let i be Nat; :: thesis: ( i < LifeSpan (P1,s1) implies ( (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 k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

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

_{1}[k + 1]
; :: thesis: verum

end;assume A11: S

now :: thesis: ( k + 1 < LifeSpan (P1,s1) implies ( (IC (Comput (P1,s1,(k + 1)))) + n = IC (Comput (P2,s2,(k + 1))) & 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))) ) )

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

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

A12: k <= k + 1 by NAT_1:11;

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

A13: 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))) ;

assume A14: k + 1 < LifeSpan (P1,s1) ; :: thesis: ( (IC (Comput (P1,s1,(k + 1)))) + n = IC (Comput (P2,s2,(k + 1))) & 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))) )

then A15: l + n in dom (Shift (I,n)) by A1, A2, A3, Th13, VALUED_1:24;

A16: 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))) ;

A17: P1 +* (stop I) = P1 by A1, FUNCT_4:98;

then A18: IC (Comput (P1,s1,k)) in dom (stop I) by A2, A9, SCMPDS_6:def 2;

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

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

then A20: InsCode (CurInstr (P1,(Comput (P1,s1,k)))) <> 3 by A18, SCMPDS_4:def 9;

A21: IC (Comput (P1,s1,(k + 1))) in dom (stop I) by A2, A9, A17, SCMPDS_6:def 2;

A22: CurInstr (P1,(Comput (P1,s1,k))) valid_at m by A18, A19, SCMPDS_4:def 9;

A23: InsCode (CurInstr (P1,(Comput (P1,s1,k)))) <> 1 by A18, A19, SCMPDS_4:def 9;

hence A24: (IC (Comput (P1,s1,(k + 1)))) + n = IC (Comput (P2,s2,(k + 1))) by A11, A14, A12, A13, A16, A20, A22, SCMPDS_4:28, XXREAL_0:2; :: 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, A21, GRFUNC_1:2 ;

hence CurInstr (P1,(Comput (P1,s1,(k + 1)))) = (Shift ((stop I),n)) . (l + n) by A21, VALUED_1:def 12

.= (Shift (I,n)) . (IC (Comput (P2,s2,(k + 1)))) by A24, A14, A1, A2, A3, Th13, COMPOS_1:65

.= P2 . (IC (Comput (P2,s2,(k + 1)))) by A6, A24, A15, 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 A11, A14, A12, A13, A16, A23, A20, A22, SCMPDS_4:28, XXREAL_0:2; :: thesis: verum

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

A12: k <= k + 1 by NAT_1:11;

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

A13: 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))) ;

assume A14: k + 1 < LifeSpan (P1,s1) ; :: thesis: ( (IC (Comput (P1,s1,(k + 1)))) + n = IC (Comput (P2,s2,(k + 1))) & 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))) )

then A15: l + n in dom (Shift (I,n)) by A1, A2, A3, Th13, VALUED_1:24;

A16: 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))) ;

A17: P1 +* (stop I) = P1 by A1, FUNCT_4:98;

then A18: IC (Comput (P1,s1,k)) in dom (stop I) by A2, A9, SCMPDS_6:def 2;

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

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

then A20: InsCode (CurInstr (P1,(Comput (P1,s1,k)))) <> 3 by A18, SCMPDS_4:def 9;

A21: IC (Comput (P1,s1,(k + 1))) in dom (stop I) by A2, A9, A17, SCMPDS_6:def 2;

A22: CurInstr (P1,(Comput (P1,s1,k))) valid_at m by A18, A19, SCMPDS_4:def 9;

A23: InsCode (CurInstr (P1,(Comput (P1,s1,k)))) <> 1 by A18, A19, SCMPDS_4:def 9;

hence A24: (IC (Comput (P1,s1,(k + 1)))) + n = IC (Comput (P2,s2,(k + 1))) by A11, A14, A12, A13, A16, A20, A22, SCMPDS_4:28, XXREAL_0:2; :: 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, A21, GRFUNC_1:2 ;

hence CurInstr (P1,(Comput (P1,s1,(k + 1)))) = (Shift ((stop I),n)) . (l + n) by A21, VALUED_1:def 12

.= (Shift (I,n)) . (IC (Comput (P2,s2,(k + 1)))) by A24, A14, A1, A2, A3, Th13, COMPOS_1:65

.= P2 . (IC (Comput (P2,s2,(k + 1)))) by A6, A24, A15, 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 A11, A14, A12, A13, A16, A23, A20, A22, SCMPDS_4:28, XXREAL_0:2; :: thesis: verum

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

A26: 0 in dom I by AFINSQ_1:66;

A27: S

proof

for k being Nat holds S
assume
0 < LifeSpan (P1,s1)
; :: thesis: ( (IC (Comput (P1,s1,0))) + n = IC (Comput (P2,s2,0)) & CurInstr (P1,(Comput (P1,s1,0))) = CurInstr (P2,(Comput (P2,s2,0))) & DataPart (Comput (P1,s1,0)) = DataPart (Comput (P2,s2,0)) )

A28: 0 + n in dom (Shift (I,n)) by A26, VALUED_1:24;

A29: P1 . (IC s1) = P1 . 0 by MEMSTR_0:def 11

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

IC (Comput (P1,s1,0)) = 0 by MEMSTR_0:def 11;

hence (IC (Comput (P1,s1,0))) + n = IC (Comput (P2,s2,0)) by A7; :: thesis: ( CurInstr (P1,(Comput (P1,s1,0))) = CurInstr (P2,(Comput (P2,s2,0))) & DataPart (Comput (P1,s1,0)) = DataPart (Comput (P2,s2,0)) )

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

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

thus CurInstr (P1,(Comput (P1,s1,0))) = (Shift ((stop I),n)) . (0 + n) by A25, A29, A30, VALUED_1:def 12

.= (Shift (I,n)) . n by COMPOS_1:66

.= CurInstr (P2,(Comput (P2,s2,0))) by A6, A7, A28, A31, GRFUNC_1:2 ; :: thesis: DataPart (Comput (P1,s1,0)) = DataPart (Comput (P2,s2,0))

thus DataPart (Comput (P1,s1,0)) = DataPart (Comput (P2,s2,0)) by A8; :: thesis: verum

end;A28: 0 + n in dom (Shift (I,n)) by A26, VALUED_1:24;

A29: P1 . (IC s1) = P1 . 0 by MEMSTR_0:def 11

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

IC (Comput (P1,s1,0)) = 0 by MEMSTR_0:def 11;

hence (IC (Comput (P1,s1,0))) + n = IC (Comput (P2,s2,0)) by A7; :: thesis: ( CurInstr (P1,(Comput (P1,s1,0))) = CurInstr (P2,(Comput (P2,s2,0))) & DataPart (Comput (P1,s1,0)) = DataPart (Comput (P2,s2,0)) )

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

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

thus CurInstr (P1,(Comput (P1,s1,0))) = (Shift ((stop I),n)) . (0 + n) by A25, A29, A30, VALUED_1:def 12

.= (Shift (I,n)) . n by COMPOS_1:66

.= CurInstr (P2,(Comput (P2,s2,0))) by A6, A7, A28, A31, GRFUNC_1:2 ; :: thesis: DataPart (Comput (P1,s1,0)) = DataPart (Comput (P2,s2,0))

thus DataPart (Comput (P1,s1,0)) = DataPart (Comput (P2,s2,0)) by A8; :: thesis: verum

hence ( i < LifeSpan (P1,s1) implies ( (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