let k be Element of NAT ; :: thesis: for R being non trivial Ring
for s1, s2 being State of (SCM R)
for q being NAT -defined the InstructionsF of (SCM b1) -valued finite non halt-free Function
for p being non empty b4 -autonomic FinPartState of (SCM R) st p c= s1 & IncIC (p,k) c= s2 holds
for P1, P2 being Instruction-Sequence of (SCM R) st q c= P1 & Reloc (q,k) c= P2 holds
for i being Element of 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))) & (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) )
let R be non trivial Ring; :: thesis: for s1, s2 being State of (SCM R)
for q being NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function
for p being non empty b3 -autonomic FinPartState of (SCM R) st p c= s1 & IncIC (p,k) c= s2 holds
for P1, P2 being Instruction-Sequence of (SCM R) st q c= P1 & Reloc (q,k) c= P2 holds
for i being Element of 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))) & (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) )
let s1, s2 be State of (SCM R); :: thesis: for q being NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of (SCM R) st p c= s1 & IncIC (p,k) c= s2 holds
for P1, P2 being Instruction-Sequence of (SCM R) st q c= P1 & Reloc (q,k) c= P2 holds
for i being Element of 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))) & (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) )
let q be NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function; :: thesis: for p being non empty q -autonomic FinPartState of (SCM R) st p c= s1 & IncIC (p,k) c= s2 holds
for P1, P2 being Instruction-Sequence of (SCM R) st q c= P1 & Reloc (q,k) c= P2 holds
for i being Element of 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))) & (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) )
let p be non empty q -autonomic FinPartState of (SCM R); :: thesis: ( p c= s1 & IncIC (p,k) c= s2 implies for P1, P2 being Instruction-Sequence of (SCM R) st q c= P1 & Reloc (q,k) c= P2 holds
for i being Element of 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))) & (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) ) )
assume that
A2: p c= s1 and
A3: IncIC (p,k) c= s2 ; :: thesis: for P1, P2 being Instruction-Sequence of (SCM R) st q c= P1 & Reloc (q,k) c= P2 holds
for i being Element of 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))) & (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) )
A1: IC in dom p by AMISTD_5:6;
let P1, P2 be Instruction-Sequence of (SCM R); :: thesis: ( q c= P1 & Reloc (q,k) c= P2 implies for i being Element of 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))) & (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) ) )
assume A5: ( q c= P1 & Reloc (q,k) c= P2 ) ; :: thesis: for i being Element of 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))) & (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) )
set s = s1 +* (DataPart s2);
defpred S1[ Element of 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))) & (Comput (P1,s1,$1)) | (dom (DataPart p)) = (Comput (P2,s2,$1)) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),$1)) = DataPart (Comput (P2,s2,$1)) );
A7: IC p = IC s1 by A2, A1, GRFUNC_1:2;
then IC p = IC (Comput (P1,s1,0)) ;
then A8: IC p in dom q by A2, A5, AMISTD_5:def 4;
A9: p c= s1 +* (DataPart s2) by A2, A3, MEMSTR_0:61;
A10: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
set DPp = DataPart p;
let i be Element of NAT ; :: thesis: ( S1[i] implies S1[i + 1] )
assume that
A11: (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) and
A12: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) and
A13: (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) and
A14: DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (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);
A15: 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))) ;
A16: now :: thesis: for s being State of (SCM R)
for d being Data-Location of R holds d in dom (DataPart s)
let s be State of (SCM R); :: thesis: for d being Data-Location of R holds d in dom (DataPart s)
let d be Data-Location of R; :: thesis: d in dom (DataPart s)
d in Data-Locations by SCMRING2:23;
hence d in dom (DataPart s) by MEMSTR_0:9; :: thesis: verum
end;
A17: now :: thesis: for d being Data-Location of R holds (Comput (P1,(s1 +* (DataPart s2)),i)) . d = (Comput (P2,s2,i)) . d
let d be Data-Location of R; :: thesis: (Comput (P1,(s1 +* (DataPart s2)),i)) . d = (Comput (P2,s2,i)) . d
A18: d in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),i))) by A16;
hence (Comput (P1,(s1 +* (DataPart s2)),i)) . d = (DataPart (Comput (P1,(s1 +* (DataPart s2)),i))) . d by FUNCT_1:47
.= (Comput (P2,s2,i)) . d by A14, A18, FUNCT_1:47 ;
:: thesis: verum
end;
set Cs1i1 = Comput (P1,s1,(i + 1));
set Cs1i = Comput (P1,s1,i);
dom (Comput (P1,s1,(i + 1))) = the carrier of (SCM R) by PARTFUN1:def 2;
then A19: dom (Comput (P1,s1,(i + 1))) = {(IC )} \/ (Data-Locations ) by XBOOLE_1:45;
A20: succ ((IC (Comput (P1,s1,i))) + k) = (succ (IC (Comput (P1,s1,i)))) + k ;
A21: 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 Element of NAT ;
assume A22: (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))))
A23: loc in dom q by A2, A5, AMISTD_5:def 4;
loc + k in dom (Reloc (q,k)) by A23, COMPOS_1:46;
then A24: (Reloc (q,k)) . (loc + k) = P2 . (loc + k) by A5, GRFUNC_1:2;
A25: P2 /. (IC (Comput (P2,s2,(i + 1)))) = P2 . (IC (Comput (P2,s2,(i + 1)))) by PBOOLE:143;
CurInstr (P1,(Comput (P1,s1,(i + 1)))) = P1 . loc by PBOOLE:143
.= q . loc by A23, A5, GRFUNC_1:2 ;
hence IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A22, A23, A24, A25, COMPOS_1:35; :: thesis: verum
end;
dom (Comput (P2,s2,i)) = the carrier of (SCM R) by PARTFUN1:def 2;
then A26: dom (Comput (P2,s2,i)) = {(IC )} \/ (Data-Locations ) by XBOOLE_1:45;
dom (DataPart p) = (dom p) /\ (Data-Locations ) by RELAT_1:61;
then A27: dom (DataPart p) c= {(IC )} \/ (Data-Locations ) by XBOOLE_1:10, XBOOLE_1:17;
set Cs3i1 = Comput (P1,(s1 +* (DataPart s2)),(i + 1));
A28: dom (DataPart (Comput (P2,s2,i))) = Data-Locations by MEMSTR_0:9;
A29: dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) = Data-Locations by MEMSTR_0:9;
then A30: dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) c= dom (DataPart (Comput (P2,s2,(i + 1)))) by MEMSTR_0:9;
A31: dom (DataPart (Comput (P2,s2,(i + 1)))) = Data-Locations by MEMSTR_0:9;
A32: now :: thesis: for x being set st x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P2,s2,(i + 1))) . x holds
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
let x be set ; :: thesis: ( x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P2,s2,(i + 1))) . x implies (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x )
assume that
A33: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) and
A34: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P2,s2,(i + 1))) . x ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
thus (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (Comput (P2,s2,(i + 1))) . x by A33, A34, FUNCT_1:47
.= (DataPart (Comput (P2,s2,(i + 1)))) . x by A29, A31, A33, FUNCT_1:47 ; :: thesis: verum
end;
A35: dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),i))) = Data-Locations by MEMSTR_0:9;
A36: now :: thesis: for x being set st x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P1,(s1 +* (DataPart s2)),i)) . x & (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x holds
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
let x be set ; :: thesis: ( x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P1,(s1 +* (DataPart s2)),i)) . x & (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x implies (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x )
assume that
A37: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) and
A38: ( (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P1,(s1 +* (DataPart s2)),i)) . x & (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x ) ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
(DataPart (Comput (P1,(s1 +* (DataPart s2)),i))) . x = (Comput (P1,(s1 +* (DataPart s2)),i)) . x by A35, A29, A37, FUNCT_1:47;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A14, A28, A29, A32, A37, A38, FUNCT_1:47; :: thesis: verum
end;
dom (Comput (P1,s1,i)) = the carrier of (SCM R) by PARTFUN1:def 2;
then A39: dom (Comput (P1,s1,i)) = {(IC )} \/ (Data-Locations ) by XBOOLE_1:45;
dom (Comput (P2,s2,(i + 1))) = the carrier of (SCM R) by PARTFUN1:def 2;
then A40: dom (Comput (P2,s2,(i + 1))) = {(IC )} \/ (Data-Locations ) by XBOOLE_1:45;
set I = CurInstr (P1,(Comput (P1,s1,i)));
A41: 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))) ;
A42: dom ((Comput (P1,s1,i)) | (dom (DataPart p))) = (dom (Comput (P1,s1,i))) /\ (dom (DataPart p)) by RELAT_1:61
.= dom (DataPart p) by A39, A27, XBOOLE_1:28 ;
A43: dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) = (dom (Comput (P1,s1,(i + 1)))) /\ (dom (DataPart p)) by RELAT_1:61
.= dom (DataPart p) by A19, A27, XBOOLE_1:28 ;
A44: dom ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) = (dom (Comput (P2,s2,(i + 1)))) /\ (dom (DataPart p)) by RELAT_1:61
.= dom (DataPart p) by A40, A27, XBOOLE_1:28 ;
then A45: dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) c= dom ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) by A43;
A46: dom ((Comput (P2,s2,i)) | (dom (DataPart p))) = (dom (Comput (P2,s2,i))) /\ (dom (DataPart p)) by RELAT_1:61
.= dom (DataPart p) by A26, A27, XBOOLE_1:28 ;
A47: now :: thesis: for x being set
for d being Data-Location of R st d = x & d in dom (DataPart p) & (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d holds
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
let x be set ; :: thesis: for d being Data-Location of R st d = x & d in dom (DataPart p) & (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d holds
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
let d be Data-Location of R; :: thesis: ( d = x & d in dom (DataPart p) & (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d implies ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x )
assume that
A48: d = x and
A49: d in dom (DataPart p) and
A50: ( (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
A51: ( ((Comput (P1,s1,i)) | (dom (DataPart p))) . d = (Comput (P1,s1,i)) . d & ((Comput (P2,s2,i)) | (dom (DataPart p))) . d = (Comput (P2,s2,i)) . d ) by A42, A46, A49, FUNCT_1:47;
thus ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = (Comput (P1,s1,(i + 1))) . d by A43, A48, A49, FUNCT_1:47
.= ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A13, A44, A48, A49, A50, A51, FUNCT_1:47 ; :: thesis: verum
end;
A52: now :: thesis: for x being set
for d being Data-Location of R st d = x & d in dom (DataPart p) & (Comput (P1,s1,(i + 1))) . d = (Comput (P2,s2,(i + 1))) . d holds
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
let x be set ; :: thesis: for d being Data-Location of R st d = x & d in dom (DataPart p) & (Comput (P1,s1,(i + 1))) . d = (Comput (P2,s2,(i + 1))) . d holds
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
let d be Data-Location of R; :: thesis: ( d = x & d in dom (DataPart p) & (Comput (P1,s1,(i + 1))) . d = (Comput (P2,s2,(i + 1))) . d implies ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x )
assume that
A53: ( d = x & d in dom (DataPart p) ) and
A54: (Comput (P1,s1,(i + 1))) . d = (Comput (P2,s2,(i + 1))) . d ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
thus ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = (Comput (P2,s2,(i + 1))) . d by A43, A53, A54, FUNCT_1:47
.= ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A44, A53, FUNCT_1:47 ; :: thesis: verum
end;
A55: Comput (P1,(s1 +* (DataPart s2)),(i + 1)) = Following (P1,(Comput (P1,(s1 +* (DataPart s2)),i))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,(s1 +* (DataPart s2)),i))) by A2, A9, A5, AMISTD_5:7 ;
per cases ( InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 0 or InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 1 or InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 2 or InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 3 or InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 4 or InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 5 or InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 6 or InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 7 ) by NAT_1:31, SCMRING3:39;
suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 0 ; :: thesis: S1[i + 1]
then A56: CurInstr (P1,(Comput (P1,s1,i))) = halt (SCM R) by SCMRING3:12;
hence (IC (Comput (P1,s1,(i + 1)))) + k = (IC (Comput (P1,s1,i))) + k by A41, EXTPRO_1:def 3
.= IC (Comput (P2,s2,(i + 1))) by A11, A12, A15, A56, EXTPRO_1:def 3 ;
:: thesis: ( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
hence IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A21; :: thesis: ( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
A57: Comput (P2,s2,(i + 1)) = Comput (P2,s2,i) by A12, A15, A56, EXTPRO_1:def 3;
hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A13, A41, A56, EXTPRO_1:def 3; :: thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
thus DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A14, A55, A56, A57, EXTPRO_1:def 3; :: thesis: verum
end;
suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 1 ; :: thesis: S1[i + 1]
then consider da, db being Data-Location of R such that
A58: CurInstr (P1,(Comput (P1,s1,i))) = da := db by SCMRING3:13;
A59: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = da := db by A58, COMPOS_0:4;
A60: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A58, SCMRING2:11;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A11, A12, A41, A15, A20, A59, SCMRING2:11; :: thesis: ( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A11, A12, A21, A41, A15, A20, A59, A60, SCMRING2:11; :: thesis: ( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
A61: (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db by A17;
now :: thesis: for x being set st x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) holds
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
DataPart p c= p by RELAT_1:59;
then A62: dom (DataPart p) c= dom p by GRFUNC_1:2;
let x be set ; :: thesis: ( x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) implies ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 )
assume A63: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
dom (DataPart p) c= Data-Locations by RELAT_1:58;
then reconsider d = x as Data-Location of R by A43, A63, SCMRING2:23;
per cases ( da = d or da <> d ) ;
suppose A64: da = d ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
then ( (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . db & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . db ) by A12, A41, A15, A58, A59, SCMRING2:11;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A2, A9, A43, A52, A58, A61, A63, A62, A64, Th7, A5; :: thesis: verum
end;
suppose da <> d ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
then ( (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A12, A41, A15, A58, A59, SCMRING2:11;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A43, A47, A63; :: thesis: verum
end;
end;
end;
then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A45, GRFUNC_1:2;
hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A43, A44, GRFUNC_1:3; :: thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
now :: thesis: for x being set st x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) holds
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
let x be set ; :: thesis: ( x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) implies (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 )
assume A65: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1
then reconsider d = x as Data-Location of R by A29, SCMRING2:23;
per cases ( da = d or da <> d ) ;
suppose da = d ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1
then ( (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . db & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . db ) by A12, A15, A55, A58, A59, SCMRING2:11;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A17, A32, A65; :: thesis: verum
end;
suppose da <> d ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1
then ( (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A12, A15, A55, A58, A59, SCMRING2:11;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A36, A65; :: thesis: verum
end;
end;
end;
then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A30, GRFUNC_1:2;
hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A29, A31, GRFUNC_1:3; :: thesis: verum
end;
suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 2 ; :: thesis: S1[i + 1]
then consider da, db being Data-Location of R such that
A66: CurInstr (P1,(Comput (P1,s1,i))) = AddTo (da,db) by SCMRING3:14;
A67: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = AddTo (da,db) by A66, COMPOS_0:4;
A68: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A66, SCMRING2:12;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A11, A12, A41, A15, A20, A67, SCMRING2:12; :: thesis: ( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A11, A12, A21, A41, A15, A20, A67, A68, SCMRING2:12; :: thesis: ( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
A69: ( (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da & (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db ) by A17;
now :: thesis: for x being set st x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) holds
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
DataPart p c= p by RELAT_1:59;
then A70: dom (DataPart p) c= dom p by GRFUNC_1:2;
let x be set ; :: thesis: ( x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) implies ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 )
assume A71: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
dom (DataPart p) c= Data-Locations by RELAT_1:58;
then reconsider d = x as Data-Location of R by A43, A71, SCMRING2:23;
per cases ( da = d or da <> d ) ;
suppose A72: da = d ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
then ( (Comput (P1,s1,(i + 1))) . d = ((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . db) & (Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db) ) by A12, A41, A15, A66, A67, SCMRING2:12;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A2, A9, A43, A52, A66, A69, A71, A70, A72, Th8, A5; :: thesis: verum
end;
suppose da <> d ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
then ( (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A12, A41, A15, A66, A67, SCMRING2:12;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A43, A47, A71; :: thesis: verum
end;
end;
end;
then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A45, GRFUNC_1:2;
hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A43, A44, GRFUNC_1:3; :: thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
now :: thesis: for x being set st x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) holds
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
let x be set ; :: thesis: ( x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) implies (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 )
assume A73: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1
then reconsider d = x as Data-Location of R by A29, SCMRING2:23;
per cases ( da = d or da <> d ) ;
suppose da = d ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1
then ( (Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db) & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) + ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) ) by A12, A15, A55, A66, A67, SCMRING2:12;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A32, A69, A73; :: thesis: verum
end;
suppose da <> d ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1
then ( (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A12, A15, A55, A66, A67, SCMRING2:12;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A36, A73; :: thesis: verum
end;
end;
end;
then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A30, GRFUNC_1:2;
hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A29, A31, GRFUNC_1:3; :: thesis: verum
end;
suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 3 ; :: thesis: S1[i + 1]
then consider da, db being Data-Location of R such that
A74: CurInstr (P1,(Comput (P1,s1,i))) = SubFrom (da,db) by SCMRING3:15;
A75: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = SubFrom (da,db) by A74, COMPOS_0:4;
A76: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A74, SCMRING2:13;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A11, A12, A41, A15, A20, A75, SCMRING2:13; :: thesis: ( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A11, A12, A21, A41, A15, A20, A75, A76, SCMRING2:13; :: thesis: ( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
A77: ( (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da & (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db ) by A17;
now :: thesis: for x being set st x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) holds
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
DataPart p c= p by RELAT_1:59;
then A78: dom (DataPart p) c= dom p by GRFUNC_1:2;
let x be set ; :: thesis: ( x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) implies ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 )
assume A79: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
dom (DataPart p) c= Data-Locations by RELAT_1:58;
then reconsider d = x as Data-Location of R by A43, A79, SCMRING2:23;
per cases ( da = d or da <> d ) ;
suppose A80: da = d ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
then ( (Comput (P1,s1,(i + 1))) . d = ((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) & (Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db) ) by A12, A41, A15, A74, A75, SCMRING2:13;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A2, A9, A43, A52, A74, A77, A79, A78, A80, Th9, A5; :: thesis: verum
end;
suppose da <> d ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
then ( (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A12, A41, A15, A74, A75, SCMRING2:13;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A43, A47, A79; :: thesis: verum
end;
end;
end;
then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A45, GRFUNC_1:2;
hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A43, A44, GRFUNC_1:3; :: thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
now :: thesis: for x being set st x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) holds
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
let x be set ; :: thesis: ( x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) implies (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 )
assume A81: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1
then reconsider d = x as Data-Location of R by A29, SCMRING2:23;
per cases ( da = d or da <> d ) ;
suppose da = d ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1
then ( (Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db) & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) - ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) ) by A12, A15, A55, A74, A75, SCMRING2:13;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A32, A77, A81; :: thesis: verum
end;
suppose da <> d ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1
then ( (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A12, A15, A55, A74, A75, SCMRING2:13;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A36, A81; :: thesis: verum
end;
end;
end;
then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A30, GRFUNC_1:2;
hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A29, A31, GRFUNC_1:3; :: thesis: verum
end;
suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 4 ; :: thesis: S1[i + 1]
then consider da, db being Data-Location of R such that
A82: CurInstr (P1,(Comput (P1,s1,i))) = MultBy (da,db) by SCMRING3:16;
A83: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = MultBy (da,db) by A82, COMPOS_0:4;
A84: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A82, SCMRING2:14;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A11, A12, A41, A15, A20, A83, SCMRING2:14; :: thesis: ( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A11, A12, A21, A41, A15, A20, A83, A84, SCMRING2:14; :: thesis: ( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
A85: ( (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da & (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db ) by A17;
now :: thesis: for x being set st x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) holds
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
DataPart p c= p by RELAT_1:59;
then A86: dom (DataPart p) c= dom p by GRFUNC_1:2;
let x be set ; :: thesis: ( x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) implies ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 )
assume A87: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
dom (DataPart p) c= Data-Locations by RELAT_1:58;
then reconsider d = x as Data-Location of R by A43, A87, SCMRING2:23;
per cases ( da = d or da <> d ) ;
suppose A88: da = d ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
then ( (Comput (P1,s1,(i + 1))) . d = ((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . db) & (Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db) ) by A12, A41, A15, A82, A83, SCMRING2:14;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A2, A9, A43, A52, A82, A85, A87, A86, A88, Th10, A5; :: thesis: verum
end;
suppose da <> d ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
then ( (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A12, A41, A15, A82, A83, SCMRING2:14;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A43, A47, A87; :: thesis: verum
end;
end;
end;
then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A45, GRFUNC_1:2;
hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A43, A44, GRFUNC_1:3; :: thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
now :: thesis: for x being set st x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) holds
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
let x be set ; :: thesis: ( x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) implies (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 )
assume A89: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1
then reconsider d = x as Data-Location of R by A29, SCMRING2:23;
per cases ( da = d or da <> d ) ;
suppose da = d ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1
then ( (Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db) & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) * ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) ) by A12, A15, A55, A82, A83, SCMRING2:14;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A32, A85, A89; :: thesis: verum
end;
suppose da <> d ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1
then ( (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A12, A15, A55, A82, A83, SCMRING2:14;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A36, A89; :: thesis: verum
end;
end;
end;
then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A30, GRFUNC_1:2;
hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A29, A31, GRFUNC_1:3; :: thesis: verum
end;
suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 5 ; :: thesis: S1[i + 1]
then consider da being Data-Location of R, r being Element of R such that
A90: CurInstr (P1,(Comput (P1,s1,i))) = da := r by SCMRING3:17;
A91: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = da := r by A90, COMPOS_0:4;
A92: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A90, SCMRING2:17;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A11, A12, A41, A15, A20, A91, SCMRING2:17; :: thesis: ( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A11, A12, A21, A41, A15, A20, A91, A92, SCMRING2:17; :: thesis: ( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
now :: thesis: for x being set st x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) holds
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
let x be set ; :: thesis: ( x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) implies ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 )
assume A93: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
dom (DataPart p) c= Data-Locations by RELAT_1:58;
then reconsider d = x as Data-Location of R by A43, A93, SCMRING2:23;
per cases ( da = d or da <> d ) ;
suppose A94: da = d ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
thus ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = (Comput (P1,s1,(i + 1))) . d by A43, A93, FUNCT_1:49
.= r by A41, A90, A94, SCMRING2:17
.= (Comput (P2,s2,(i + 1))) . d by A12, A15, A91, A94, SCMRING2:17
.= ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A43, A93, FUNCT_1:49 ; :: thesis: verum
end;
suppose da <> d ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
then ( (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A12, A41, A15, A90, A91, SCMRING2:17;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A43, A47, A93; :: thesis: verum
end;
end;
end;
then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A45, GRFUNC_1:2;
hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A43, A44, GRFUNC_1:3; :: thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
now :: thesis: for x being set st x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) holds
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
let x be set ; :: thesis: ( x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) implies (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 )
assume A95: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1
then reconsider d = x as Data-Location of R by A29, SCMRING2:23;
per cases ( da = d or da <> d ) ;
suppose da = d ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1
then ( (Comput (P2,s2,(i + 1))) . d = r & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = r ) by A12, A15, A55, A90, A91, SCMRING2:17;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A32, A95; :: thesis: verum
end;
suppose da <> d ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1
then ( (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A12, A15, A55, A90, A91, SCMRING2:17;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A36, A95; :: thesis: verum
end;
end;
end;
then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A30, GRFUNC_1:2;
hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A29, A31, GRFUNC_1:3; :: thesis: verum
end;
suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 6 ; :: thesis: S1[i + 1]
then consider loc being Element of NAT such that
A96: CurInstr (P1,(Comput (P1,s1,i))) = goto (loc,R) by SCMRING3:18;
A97: CurInstr (P2,(Comput (P2,s2,i))) = goto ((loc + k),R) by A12, A96, SCMRING3:37;
thus (IC (Comput (P1,s1,(i + 1)))) + k = loc + k by A41, A96, SCMRING2:15
.= IC (Comput (P2,s2,(i + 1))) by A15, A97, SCMRING2:15 ; :: thesis: ( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
hence IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A21; :: thesis: ( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
now :: thesis: for x being set st x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) holds
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
let x be set ; :: thesis: ( x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) implies ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x )
assume A98: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
dom (DataPart p) c= Data-Locations by RELAT_1:58;
then reconsider d = x as Data-Location of R by A43, A98, SCMRING2:23;
( (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A41, A15, A96, A97, SCMRING2:15;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A43, A47, A98; :: thesis: verum
end;
then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A45, GRFUNC_1:2;
hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A43, A44, GRFUNC_1:3; :: thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
now :: thesis: for x being set st x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) holds
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
let x be set ; :: thesis: ( x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) implies (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x )
assume A99: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
then reconsider d = x as Data-Location of R by A29, SCMRING2:23;
( (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A15, A55, A96, A97, SCMRING2:15;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A36, A99; :: thesis: verum
end;
then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A30, GRFUNC_1:2;
hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A29, A31, GRFUNC_1:3; :: thesis: verum
end;
suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 7 ; :: thesis: S1[i + 1]
then consider da being Data-Location of R, loc being Element of NAT such that
A100: CurInstr (P1,(Comput (P1,s1,i))) = da =0_goto loc by SCMRING3:19;
A101: now :: thesis: ( ( (Comput (P1,s1,i)) . da = 0. R & (IC (Comput (P1,s1,(i + 1)))) + k = loc + k ) or ( (Comput (P1,s1,i)) . da <> 0. R & (IC (Comput (P1,s1,(i + 1)))) + k = succ (IC (Comput (P2,s2,i))) ) )
per cases ( (Comput (P1,s1,i)) . da = 0. R or (Comput (P1,s1,i)) . da <> 0. R ) ;
case (Comput (P1,s1,i)) . da = 0. R ; :: thesis: (IC (Comput (P1,s1,(i + 1)))) + k = loc + k
hence (IC (Comput (P1,s1,(i + 1)))) + k = loc + k by A41, A100, SCMRING2:16; :: thesis: verum
end;
case (Comput (P1,s1,i)) . da <> 0. R ; :: thesis: (IC (Comput (P1,s1,(i + 1)))) + k = succ (IC (Comput (P2,s2,i)))
hence (IC (Comput (P1,s1,(i + 1)))) + k = succ (IC (Comput (P2,s2,i))) by A11, A41, A20, A100, SCMRING2:16; :: thesis: verum
end;
end;
end;
A102: CurInstr (P2,(Comput (P2,s2,i))) = da =0_goto (loc + k) by A12, A100, SCMRING3:38;
A103: now :: thesis: ( ( (Comput (P2,s2,i)) . da = 0. R & IC (Comput (P2,s2,(i + 1))) = loc + k ) or ( (Comput (P2,s2,i)) . da <> 0. R & IC (Comput (P2,s2,(i + 1))) = succ (IC (Comput (P2,s2,i))) ) )
per cases ( (Comput (P2,s2,i)) . da = 0. R or (Comput (P2,s2,i)) . da <> 0. R ) ;
case (Comput (P2,s2,i)) . da = 0. R ; :: thesis: IC (Comput (P2,s2,(i + 1))) = loc + k
hence IC (Comput (P2,s2,(i + 1))) = loc + k by A15, A102, SCMRING2:16; :: thesis: verum
end;
case (Comput (P2,s2,i)) . da <> 0. R ; :: thesis: IC (Comput (P2,s2,(i + 1))) = succ (IC (Comput (P2,s2,i)))
hence IC (Comput (P2,s2,(i + 1))) = succ (IC (Comput (P2,s2,i))) by A15, A102, SCMRING2:16; :: thesis: verum
end;
end;
end;
A104: (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da by A17;
now :: thesis: (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1)))
per cases ( loc <> succ (IC (Comput (P1,s1,i))) or loc = succ (IC (Comput (P1,s1,i))) ) ;
suppose loc <> succ (IC (Comput (P1,s1,i))) ; :: thesis: (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1)))
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A2, A9, A100, A104, A101, A103, Th11, A5; :: thesis: verum
end;
suppose loc = succ (IC (Comput (P1,s1,i))) ; :: thesis: (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1)))
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A11, A101, A103; :: thesis: verum
end;
end;
end;
hence ( (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) & IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) ) by A21; :: thesis: ( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
now :: thesis: for x being set st x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) holds
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
let x be set ; :: thesis: ( x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) implies ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x )
assume A105: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
dom (DataPart p) c= Data-Locations by RELAT_1:58;
then reconsider d = x as Data-Location of R by A43, A105, SCMRING2:23;
( (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A41, A15, A100, A102, SCMRING2:16;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A43, A47, A105; :: thesis: verum
end;
then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A45, GRFUNC_1:2;
hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A43, A44, GRFUNC_1:3; :: thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
now :: thesis: for x being set st x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) holds
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
let x be set ; :: thesis: ( x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) implies (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x )
assume A106: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
then reconsider d = x as Data-Location of R by A29, SCMRING2:23;
( (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A15, A55, A100, A102, SCMRING2:16;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A36, A106; :: thesis: verum
end;
then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A30, GRFUNC_1:2;
hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A29, A31, GRFUNC_1:3; :: thesis: verum
end;
end;
end;
A107: DataPart p c= p by RELAT_1:59;
A108: DataPart (IncIC (p,k)) = DataPart p by MEMSTR_0:51;
A109: DataPart p c= IncIC (p,k) by A108, MEMSTR_0:12;
A110: (Comput (P1,s1,0)) | (dom (DataPart p)) = s1 | (dom (DataPart p))
.= DataPart p by A2, A107, GRFUNC_1:23, XBOOLE_1:1
.= s2 | (dom (DataPart p)) by A109, A3, GRFUNC_1:23, XBOOLE_1:1
.= (Comput (P2,s2,0)) | (dom (DataPart p)) ;
A111: DataPart (Comput (P1,(s1 +* (DataPart s2)),0)) = DataPart (s1 +* (DataPart s2))
.= DataPart s2 by PBOOLE:142
.= DataPart (Comput (P2,s2,0)) ;
A112: IC in dom (IncIC (p,k)) by MEMSTR_0:52;
A113: (IC (Comput (P1,s1,0))) + k = (IC s1) + k
.= (IC p) + k by A2, A1, GRFUNC_1:2
.= (IC p) + k
.= IC (IncIC (p,k)) by MEMSTR_0:53
.= IC s2 by A3, A112, GRFUNC_1:2
.= IC (Comput (P2,s2,0)) ;
A114: IC in dom (IncIC (p,k)) by MEMSTR_0:52;
A115: (IC p) + k in dom (Reloc (q,k)) by A8, COMPOS_1:46;
A116: P2 /. (IC s2) = P2 . (IC s2) by PBOOLE:143;
A117: CurInstr (P2,(Comput (P2,s2,0))) = P2 . (IC s2) by A116
.= P2 . (IC (IncIC (p,k))) by A3, A114, GRFUNC_1:2
.= P2 . ((IC p) + k) by MEMSTR_0:53
.= P2 . ((IC p) + k)
.= (Reloc (q,k)) . ((IC p) + k) by A115, A5, GRFUNC_1:2 ;
A118: q . (IC p) = P1 . (IC s1) by A7, A8, A5, GRFUNC_1:2;
A119: CurInstr (P1,s1) = q . (IC p) by A118, PBOOLE:143;
A120: IncAddr ((CurInstr (P1,(Comput (P1,s1,0)))),k) = IncAddr ((CurInstr (P1,s1)),k)
.= CurInstr (P2,(Comput (P2,s2,0))) by A117, A8, A119, COMPOS_1:35 ;
A121: S1[ 0 ] by A113, A120, A110, A111;
for n being Element of NAT holds S1[n] from NAT_1:sch 1(A121, A10);
 hence for i being Element of 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))) & (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) ) ; :: thesis: verum