:: Relocatability
:: by Yasushi Tanaka
::
:: Received June 16, 1994
:: Copyright (c) 1994 Association of Mizar Users
:: deftheorem RELOC:def 1 :
canceled;
:: deftheorem RELOC:def 2 :
canceled;
:: deftheorem Def3 defines IncAddr RELOC:def 3 :
theorem :: RELOC:1
canceled;
theorem :: RELOC:2
canceled;
theorem :: RELOC:3
canceled;
theorem :: RELOC:4
theorem Th5: :: RELOC:5
theorem Th6: :: RELOC:6
theorem Th7: :: RELOC:7
theorem Th8: :: RELOC:8
theorem Th9: :: RELOC:9
theorem Th10: :: RELOC:10
theorem Th11: :: RELOC:11
theorem Th12: :: RELOC:12
theorem Th13: :: RELOC:13
theorem Th14: :: RELOC:14
theorem :: RELOC:15
canceled;
theorem :: RELOC:16
canceled;
theorem :: RELOC:17
canceled;
definition
canceled;let p be
finite PartFunc of
NAT ,the
Instructions of
SCM ;
let k be
Element of
NAT ;
func IncAddr p,
k -> finite PartFunc of
NAT ,the
Instructions of
SCM means :
Def5:
:: RELOC:def 5
(
dom it = dom p & ( for
m being
Element of
NAT st
m in dom p holds
it . m = IncAddr (p /. m),
k ) );
existence
ex b1 being finite PartFunc of NAT ,the Instructions of SCM st
( dom b1 = dom p & ( for m being Element of NAT st m in dom p holds
b1 . m = IncAddr (p /. m),k ) )
uniqueness
for b1, b2 being finite PartFunc of NAT ,the Instructions of SCM st dom b1 = dom p & ( for m being Element of NAT st m in dom p holds
b1 . m = IncAddr (p /. m),k ) & dom b2 = dom p & ( for m being Element of NAT st m in dom p holds
b2 . m = IncAddr (p /. m),k ) holds
b1 = b2
end;
:: deftheorem RELOC:def 4 :
canceled;
:: deftheorem Def5 defines IncAddr RELOC:def 5 :
theorem :: RELOC:18
theorem Th19: :: RELOC:19
:: deftheorem defines Relocated RELOC:def 6 :
theorem :: RELOC:20
canceled;
theorem Th21: :: RELOC:21
theorem Th22: :: RELOC:22
theorem Th23: :: RELOC:23
theorem Th24: :: RELOC:24
theorem Th25: :: RELOC:25
theorem Th26: :: RELOC:26
theorem Th27: :: RELOC:27
theorem Th28: :: RELOC:28
theorem Th29: :: RELOC:29
theorem Th30: :: RELOC:30
theorem Th31: :: RELOC:31
theorem Th32: :: RELOC:32
theorem :: RELOC:33
Lm1:
for k being Element of NAT
for p being autonomic FinPartState of SCM
for s1, s2 being State of SCM st IC SCM in dom p & p c= s1 & Relocated p,k c= s2 holds
for i being Element of NAT holds
( (IC (Computation s1,i)) + k = IC (Computation s2,i) & IncAddr (CurInstr (Computation s1,i)),k = CurInstr (Computation s2,i) & (Computation s1,i) | (dom (DataPart p)) = (Computation s2,i) | (dom (DataPart (Relocated p,k))) & DataPart (Computation (s1 +* (DataPart s2)),i) = DataPart (Computation s2,i) )
theorem :: RELOC:34
theorem Th35: :: RELOC:35
theorem :: RELOC:36
theorem :: RELOC:37
theorem Th38: :: RELOC:38
theorem Th39: :: RELOC:39
theorem Th40: :: RELOC:40
theorem Th41: :: RELOC:41
theorem Th42: :: RELOC:42
theorem :: RELOC:43