let N be with_zero set ; :: thesis: for k being Nat

for q being NAT -defined the InstructionsF of (STC N) -valued finite non halt-free Function

for p being non empty b_{2} -autonomic FinPartState of (STC N)

for s1, s2 being State of (STC N) st p c= s1 & IncIC (p,k) c= s2 holds

for P1, P2 being Instruction-Sequence of (STC N) st q c= P1 & Reloc (q,k) c= P2 holds

for i being Nat holds

( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) )

let k be Nat; :: thesis: for q being NAT -defined the InstructionsF of (STC N) -valued finite non halt-free Function

for p being non empty b_{1} -autonomic FinPartState of (STC N)

for s1, s2 being State of (STC N) st p c= s1 & IncIC (p,k) c= s2 holds

for P1, P2 being Instruction-Sequence of (STC N) st q c= P1 & Reloc (q,k) c= P2 holds

for i being Nat holds

( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) )

let q be NAT -defined the InstructionsF of (STC N) -valued finite non halt-free Function; :: thesis: for p being non empty q -autonomic FinPartState of (STC N)

for s1, s2 being State of (STC N) st p c= s1 & IncIC (p,k) c= s2 holds

for P1, P2 being Instruction-Sequence of (STC N) st q c= P1 & Reloc (q,k) c= P2 holds

for i being Nat holds

( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) )

let p be non empty q -autonomic FinPartState of (STC N); :: thesis: for s1, s2 being State of (STC N) st p c= s1 & IncIC (p,k) c= s2 holds

for P1, P2 being Instruction-Sequence of (STC N) st q c= P1 & Reloc (q,k) c= P2 holds

for i being Nat holds

( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) )

let s1, s2 be State of (STC N); :: thesis: ( p c= s1 & IncIC (p,k) c= s2 implies for P1, P2 being Instruction-Sequence of (STC N) st q c= P1 & Reloc (q,k) c= P2 holds

for i being Nat holds

( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) ) )

assume that

A1: p c= s1 and

A2: IncIC (p,k) c= s2 ; :: thesis: for P1, P2 being Instruction-Sequence of (STC N) st q c= P1 & Reloc (q,k) c= P2 holds

for i being Nat holds

( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) )

A3: IC in dom p by Th6;

let P1, P2 be Instruction-Sequence of (STC N); :: thesis: ( q c= P1 & Reloc (q,k) c= P2 implies for i being Nat holds

( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) ) )

assume A4: ( q c= P1 & Reloc (q,k) c= P2 ) ; :: thesis: for i being Nat holds

( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) )

set s3 = s1 +* (DataPart s2);

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

A5: for i being Nat st S_{1}[i] holds

S_{1}[i + 1]

_{1}[ 0 ]
;

thus for i being Nat holds S_{1}[i]
from NAT_1:sch 2(A27, A5); :: thesis: verum

for q being NAT -defined the InstructionsF of (STC N) -valued finite non halt-free Function

for p being non empty b

for s1, s2 being State of (STC N) st p c= s1 & IncIC (p,k) c= s2 holds

for P1, P2 being Instruction-Sequence of (STC N) st q c= P1 & Reloc (q,k) c= P2 holds

for i being Nat holds

( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) )

let k be Nat; :: thesis: for q being NAT -defined the InstructionsF of (STC N) -valued finite non halt-free Function

for p being non empty b

for s1, s2 being State of (STC N) st p c= s1 & IncIC (p,k) c= s2 holds

for P1, P2 being Instruction-Sequence of (STC N) st q c= P1 & Reloc (q,k) c= P2 holds

for i being Nat holds

( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) )

let q be NAT -defined the InstructionsF of (STC N) -valued finite non halt-free Function; :: thesis: for p being non empty q -autonomic FinPartState of (STC N)

for s1, s2 being State of (STC N) st p c= s1 & IncIC (p,k) c= s2 holds

for P1, P2 being Instruction-Sequence of (STC N) st q c= P1 & Reloc (q,k) c= P2 holds

for i being Nat holds

( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) )

let p be non empty q -autonomic FinPartState of (STC N); :: thesis: for s1, s2 being State of (STC N) st p c= s1 & IncIC (p,k) c= s2 holds

for P1, P2 being Instruction-Sequence of (STC N) st q c= P1 & Reloc (q,k) c= P2 holds

for i being Nat holds

( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) )

let s1, s2 be State of (STC N); :: thesis: ( p c= s1 & IncIC (p,k) c= s2 implies for P1, P2 being Instruction-Sequence of (STC N) st q c= P1 & Reloc (q,k) c= P2 holds

for i being Nat holds

( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) ) )

assume that

A1: p c= s1 and

A2: IncIC (p,k) c= s2 ; :: thesis: for P1, P2 being Instruction-Sequence of (STC N) st q c= P1 & Reloc (q,k) c= P2 holds

for i being Nat holds

( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) )

A3: IC in dom p by Th6;

let P1, P2 be Instruction-Sequence of (STC N); :: thesis: ( q c= P1 & Reloc (q,k) c= P2 implies for i being Nat holds

( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) ) )

assume A4: ( q c= P1 & Reloc (q,k) c= P2 ) ; :: thesis: for i being Nat holds

( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) )

set s3 = s1 +* (DataPart s2);

defpred S

A5: for i being Nat st S

S

proof

A19:
IC in dom (IncIC (p,k))
by MEMSTR_0:52;
set DPp = DataPart p;

let i be Nat; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

assume that

A6: (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) and

A7: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) ; :: thesis: S_{1}[i + 1]

set Cs2i1 = Comput (P2,s2,(i + 1));

set Cs3i = Comput (P1,(s1 +* (DataPart s2)),i);

set Cs2i = Comput (P2,s2,i);

set Cs3i1 = Comput (P1,(s1 +* (DataPart s2)),(i + 1));

set Cs1i1 = Comput (P1,s1,(i + 1));

set Cs1i = Comput (P1,s1,i);

A13: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:3

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

reconsider j = IC (Comput (P1,s1,i)) as Nat ;

A14: Comput (P1,s1,(i + 1)) = Following (P1,(Comput (P1,s1,i))) by EXTPRO_1:3

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

A15: the InstructionsF of (STC N) = {[0,0,0],[1,0,0]} by AMISTD_1:def 7;

end;let i be Nat; :: thesis: ( S

assume that

A6: (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) and

A7: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) ; :: thesis: S

set Cs2i1 = Comput (P2,s2,(i + 1));

set Cs3i = Comput (P1,(s1 +* (DataPart s2)),i);

set Cs2i = Comput (P2,s2,i);

set Cs3i1 = Comput (P1,(s1 +* (DataPart s2)),(i + 1));

set Cs1i1 = Comput (P1,s1,(i + 1));

set Cs1i = Comput (P1,s1,i);

A8: now :: thesis: ( (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) implies IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) )

set I = CurInstr (P1,(Comput (P1,s1,i)));reconsider loc = IC (Comput (P1,s1,(i + 1))) as Nat ;

assume A9: (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) ; :: thesis: IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1))))

reconsider kk = loc as Nat ;

A10: loc in dom q by Def4, A4, A1;

A11: loc + k in dom (Reloc (q,k)) by A10, COMPOS_1:46;

A12: dom P2 = NAT by PARTFUN1:def 2;

dom P1 = NAT by PARTFUN1:def 2;

then CurInstr (P1,(Comput (P1,s1,(i + 1)))) = P1 . loc by PARTFUN1:def 6

.= q . loc by A10, A4, GRFUNC_1:2 ;

hence IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = (Reloc (q,k)) . (loc + k) by A10, COMPOS_1:35

.= P2 . (IC (Comput (P2,s2,(i + 1)))) by A9, A11, A4, GRFUNC_1:2

.= CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A12, PARTFUN1:def 6 ;

:: thesis: verum

end;assume A9: (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) ; :: thesis: IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1))))

reconsider kk = loc as Nat ;

A10: loc in dom q by Def4, A4, A1;

A11: loc + k in dom (Reloc (q,k)) by A10, COMPOS_1:46;

A12: dom P2 = NAT by PARTFUN1:def 2;

dom P1 = NAT by PARTFUN1:def 2;

then CurInstr (P1,(Comput (P1,s1,(i + 1)))) = P1 . loc by PARTFUN1:def 6

.= q . loc by A10, A4, GRFUNC_1:2 ;

hence IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = (Reloc (q,k)) . (loc + k) by A10, COMPOS_1:35

.= P2 . (IC (Comput (P2,s2,(i + 1)))) by A9, A11, A4, GRFUNC_1:2

.= CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A12, PARTFUN1:def 6 ;

:: thesis: verum

A13: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:3

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

reconsider j = IC (Comput (P1,s1,i)) as Nat ;

A14: Comput (P1,s1,(i + 1)) = Following (P1,(Comput (P1,s1,i))) by EXTPRO_1:3

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

A15: the InstructionsF of (STC N) = {[0,0,0],[1,0,0]} by AMISTD_1:def 7;

per cases
( CurInstr (P1,(Comput (P1,s1,i))) = [0,0,0] or CurInstr (P1,(Comput (P1,s1,i))) = [1,0,0] )
by A15, TARSKI:def 2;

end;

suppose
CurInstr (P1,(Comput (P1,s1,i))) = [0,0,0]
; :: thesis: S_{1}[i + 1]

then A16:
CurInstr (P1,(Comput (P1,s1,i))) = halt (STC N)
;

thus (IC (Comput (P1,s1,(i + 1)))) + k = (IC (Comput (P1,s1,i))) + k by A14, A16, EXTPRO_1:def 3

.= IC (Comput (P2,s2,(i + 1))) by A6, A13, A16, A7, EXTPRO_1:def 3 ; :: thesis: IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1))))

hence IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A8; :: thesis: verum

end;thus (IC (Comput (P1,s1,(i + 1)))) + k = (IC (Comput (P1,s1,i))) + k by A14, A16, EXTPRO_1:def 3

.= IC (Comput (P2,s2,(i + 1))) by A6, A13, A16, A7, EXTPRO_1:def 3 ; :: thesis: IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1))))

hence IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A8; :: thesis: verum

suppose
CurInstr (P1,(Comput (P1,s1,i))) = [1,0,0]
; :: thesis: S_{1}[i + 1]

then A17:
InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 1
;

then A18: Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P2,s2,i))) = IncIC ((Comput (P2,s2,i)),1) by AMISTD_1:20;

thus (IC (Comput (P1,s1,(i + 1)))) + k = ((IC (Comput (P1,s1,i))) + 1) + k by A14, A17, AMISTD_1:9

.= IC (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P2,s2,i)))) by A18, A6, MEMSTR_0:53

.= IC (Comput (P2,s2,(i + 1))) by A13, A7, COMPOS_0:4 ; :: thesis: IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1))))

hence IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A8; :: thesis: verum

end;then A18: Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P2,s2,i))) = IncIC ((Comput (P2,s2,i)),1) by AMISTD_1:20;

thus (IC (Comput (P1,s1,(i + 1)))) + k = ((IC (Comput (P1,s1,i))) + 1) + k by A14, A17, AMISTD_1:9

.= IC (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P2,s2,i)))) by A18, A6, MEMSTR_0:53

.= IC (Comput (P2,s2,(i + 1))) by A13, A7, COMPOS_0:4 ; :: thesis: IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1))))

hence IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A8; :: thesis: verum

now :: thesis: ( (IC (Comput (P1,s1,0))) + k = IC (Comput (P2,s2,0)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,0)))),k) = CurInstr (P2,(Comput (P2,s2,0))) )

then A27:
Sthus (IC (Comput (P1,s1,0))) + k =
(IC p) + k
by A1, A3, GRFUNC_1:2

.= IC (IncIC (p,k)) by MEMSTR_0:53

.= IC (Comput (P2,s2,0)) by A2, A19, GRFUNC_1:2 ; :: thesis: IncAddr ((CurInstr (P1,(Comput (P1,s1,0)))),k) = CurInstr (P2,(Comput (P2,s2,0)))

reconsider loc = IC p as Nat ;

A20: IC p = IC s1 by A1, A3, GRFUNC_1:2;

IC p = IC (Comput (P1,s1,0)) by A1, A3, GRFUNC_1:2;

then A21: loc in dom q by Def4, A4, A1;

A22: (IC p) + k in dom (Reloc (q,k)) by A21, COMPOS_1:46;

A23: IC in dom (IncIC (p,k)) by MEMSTR_0:52;

A24: q . (IC p) = P1 . (IC s1) by A20, A21, A4, GRFUNC_1:2;

dom P2 = NAT by PARTFUN1:def 2;

then A25: CurInstr (P2,(Comput (P2,s2,0))) = P2 . (IC (Comput (P2,s2,0))) by PARTFUN1:def 6

.= P2 . (IC (IncIC (p,k))) by A2, A23, GRFUNC_1:2

.= P2 . ((IC p) + k) by MEMSTR_0:53

.= (Reloc (q,k)) . ((IC p) + k) by A22, A4, GRFUNC_1:2 ;

A26: dom P1 = NAT by PARTFUN1:def 2;

CurInstr (P1,(Comput (P1,s1,0))) = P1 . (IC s1) by A26, PARTFUN1:def 6;

hence IncAddr ((CurInstr (P1,(Comput (P1,s1,0)))),k) = CurInstr (P2,(Comput (P2,s2,0))) by A25, A21, A24, COMPOS_1:35; :: thesis: verum

end;.= IC (IncIC (p,k)) by MEMSTR_0:53

.= IC (Comput (P2,s2,0)) by A2, A19, GRFUNC_1:2 ; :: thesis: IncAddr ((CurInstr (P1,(Comput (P1,s1,0)))),k) = CurInstr (P2,(Comput (P2,s2,0)))

reconsider loc = IC p as Nat ;

A20: IC p = IC s1 by A1, A3, GRFUNC_1:2;

IC p = IC (Comput (P1,s1,0)) by A1, A3, GRFUNC_1:2;

then A21: loc in dom q by Def4, A4, A1;

A22: (IC p) + k in dom (Reloc (q,k)) by A21, COMPOS_1:46;

A23: IC in dom (IncIC (p,k)) by MEMSTR_0:52;

A24: q . (IC p) = P1 . (IC s1) by A20, A21, A4, GRFUNC_1:2;

dom P2 = NAT by PARTFUN1:def 2;

then A25: CurInstr (P2,(Comput (P2,s2,0))) = P2 . (IC (Comput (P2,s2,0))) by PARTFUN1:def 6

.= P2 . (IC (IncIC (p,k))) by A2, A23, GRFUNC_1:2

.= P2 . ((IC p) + k) by MEMSTR_0:53

.= (Reloc (q,k)) . ((IC p) + k) by A22, A4, GRFUNC_1:2 ;

A26: dom P1 = NAT by PARTFUN1:def 2;

CurInstr (P1,(Comput (P1,s1,0))) = P1 . (IC s1) by A26, PARTFUN1:def 6;

hence IncAddr ((CurInstr (P1,(Comput (P1,s1,0)))),k) = CurInstr (P2,(Comput (P2,s2,0))) by A25, A21, A24, COMPOS_1:35; :: thesis: verum

thus for i being Nat holds S