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 b2 -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 b1 -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 S1[ 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 S1[i] holds
S1[i + 1]
proof
set DPp = DataPart p;
let i be Nat; :: thesis: ( S1[i] implies S1[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: S1[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);
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)))) )
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;
set I = CurInstr (P1,(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;
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;
suppose CurInstr (P1,(Comput (P1,s1,i))) = [0,0,0] ; :: thesis: S1[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;
suppose CurInstr (P1,(Comput (P1,s1,i))) = [1,0,0] ; :: thesis: S1[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;
end;
end;
A19: IC in dom (IncIC (p,k)) by MEMSTR_0:52;
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))) )
thus (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;
then A27: S1[ 0 ] ;
thus for i being Nat holds S1[i] from NAT_1:sch 2(A27, A5); :: thesis: verum