:: by Yasushi Tanaka

::

:: Received June 16, 1994

:: Copyright (c) 1994-2021 Association of Mizar Users

registration

let a, b be Data-Location;

coherence

a := b is ins-loc-free ;

coherence

AddTo (a,b) is ins-loc-free ;

coherence

SubFrom (a,b) is ins-loc-free ;

coherence

MultBy (a,b) is ins-loc-free ;

coherence

Divide (a,b) is ins-loc-free ;

end;
coherence

a := b is ins-loc-free ;

coherence

AddTo (a,b) is ins-loc-free ;

coherence

SubFrom (a,b) is ins-loc-free ;

coherence

MultBy (a,b) is ins-loc-free ;

coherence

Divide (a,b) is ins-loc-free ;

theorem Th2: :: RELOC:2

for k, loc being Nat

for a being Data-Location holds IncAddr ((a =0_goto loc),k) = a =0_goto (loc + k)

for a being Data-Location holds IncAddr ((a =0_goto loc),k) = a =0_goto (loc + k)

proof end;

theorem Th3: :: RELOC:3

for k, loc being Nat

for a being Data-Location holds IncAddr ((a >0_goto loc),k) = a >0_goto (loc + k)

for a being Data-Location holds IncAddr ((a >0_goto loc),k) = a >0_goto (loc + k)

proof end;

theorem Th4: :: RELOC:4

for I being Instruction of SCM

for k being Element of NAT st not not InsCode I = 0 & ... & not InsCode I = 5 holds

IncAddr (I,k) = I

for k being Element of NAT st not not InsCode I = 0 & ... & not InsCode I = 5 holds

IncAddr (I,k) = I

proof end;

theorem :: RELOC:5

for II, I being Instruction of SCM

for k being Element of NAT st not not InsCode I = 0 & ... & not InsCode I = 5 & IncAddr (II,k) = I holds

II = I

for k being Element of NAT st not not InsCode I = 0 & ... & not InsCode I = 5 & IncAddr (II,k) = I holds

II = I

proof end;

Lm1: for k being Nat

for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function

for p being non empty b

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

for P1, P2 being Instruction-Sequence of SCM 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))) & (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)) )

proof end;

theorem :: RELOC:6

for k being Element of NAT

for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function

for p being non empty b_{2} -autonomic FinPartState of SCM

for s1, s2 being State of SCM st IC in dom p & p c= s1 & IncIC (p,k) c= s2 holds

for P1, P2 being Instruction-Sequence of SCM 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)) by Lm1;

for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function

for p being non empty b

for s1, s2 being State of SCM st IC in dom p & p c= s1 & IncIC (p,k) c= s2 holds

for P1, P2 being Instruction-Sequence of SCM 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)) by Lm1;

registration
end;

theorem :: RELOC:7

for k being Element of NAT

for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function

for p being non empty b_{2} -autonomic FinPartState of SCM

for s1, s2, s3 being State of SCM st IC in dom p & p c= s1 & IncIC (p,k) c= s2 & s3 = s1 +* (DataPart s2) holds

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

for i being Element of NAT holds DataPart (Comput (P1,s3,i)) = DataPart (Comput (P2,s2,i)) by Lm1;

for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function

for p being non empty b

for s1, s2, s3 being State of SCM st IC in dom p & p c= s1 & IncIC (p,k) c= s2 & s3 = s1 +* (DataPart s2) holds

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

for i being Element of NAT holds DataPart (Comput (P1,s3,i)) = DataPart (Comput (P2,s2,i)) by Lm1;