:: Composition of Machines, Instructions and Programs
:: by Andrzej Trybulec
::
:: Received May 20, 2010
:: Copyright (c) 2010-2012 Association of Mizar Users


begin

definition
attrc1 is strict ;
struct COM-Struct  -> ;
aggrCOM-Struct(# InstructionsF #) ->  COM-Struct ;
sel InstructionsF c1 ->  Instructions;
end;

definition
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
func Trivial-COM  ->  strict COM-Struct  means :Def8: :: COMPOS_1:def 8
 the InstructionsF of it = {[0,{},{}]};
existence
 ex b1 being strict COM-Struct st the InstructionsF of b1 = {[0,{},{}]}
proofend;
uniqueness
 for b1, b2 being strict COM-Struct st the InstructionsF of b1 = {[0,{},{}]} & the InstructionsF of b2 = {[0,{},{}]} holds
b1 = b2 ;
end;

:: deftheorem  COMPOS_1:def_1_:_
canceled;

:: deftheorem  COMPOS_1:def_2_:_
canceled;

:: deftheorem  COMPOS_1:def_3_:_
canceled;

:: deftheorem  COMPOS_1:def_4_:_
canceled;

:: deftheorem  COMPOS_1:def_5_:_
canceled;

:: deftheorem  COMPOS_1:def_6_:_
canceled;

:: deftheorem  COMPOS_1:def_7_:_
canceled;

:: deftheorem Def8 defines Trivial-COM COMPOS_1:def_8_:_
 for b1 being strict COM-Struct holds
( b1 = Trivial-COM iff the InstructionsF of b1 = {[0,{},{}]} );

definition
let S be COM-Struct ;
mode Instruction of S is Element of the InstructionsF of S;
end;

definition
canceled;
let S be COM-Struct ;
func halt S ->  Instruction of S equals :: COMPOS_1:def 10
 halt the InstructionsF of S;
coherence
 halt the InstructionsF of S is Instruction of S ;
end;

:: deftheorem  COMPOS_1:def_9_:_
canceled;

:: deftheorem  defines halt COMPOS_1:def_10_:_
 for S being COM-Struct holds halt S = halt the InstructionsF of S;

:: Definicje musi zachowac, zeby nie musiec pisac
:: halt SCM-Instr, zamiast halt SCM, zreszta wyrzucenie jej
:: spowodowaloby problemy z typowaniem.
definition
let S be COM-Struct ;
let I be the InstructionsF of S -valued Function;
attrI is halt-free  means :Def11: :: COMPOS_1:def 11
 not halt S in rng I;
end;

:: deftheorem Def11 defines halt-free COMPOS_1:def_11_:_
 for S being COM-Struct
for I being the InstructionsF of b1 -valued Function holds
( I is halt-free iff not halt S in rng I );

begin

definition
let S be COM-Struct ;
mode Instruction-Sequence of S is the InstructionsF of S -valued ManySortedSet of NAT ;
end;

definition
let S be COM-Struct ;
let P be Instruction-Sequence of S;
let k be Nat;
:: original:.
redefine funcP . k ->  Instruction of S;
coherence
 P . k is Instruction of S
proofend;
end;

begin

definition
let S be COM-Struct ;
let p be NAT -defined the InstructionsF of S -valued Function;
let l be set ;
predp halts_at l means :Def12: :: COMPOS_1:def 12
( l in dom p & p . l = halt S );
end;

:: deftheorem Def12 defines halts_at COMPOS_1:def_12_:_
 for S being COM-Struct
for p being NAT -defined the InstructionsF of b1 -valued Function
for l being set holds
( p halts_at l iff ( l in dom p & p . l = halt S ) );

definition
let S be COM-Struct ;
let s be Instruction-Sequence of S;
let l be Nat;
redefine pred s halts_at l means :: COMPOS_1:def 13
s . l = halt S;
compatibility
 ( s halts_at l iff s . l = halt S )
proofend;
end;

:: deftheorem  defines halts_at COMPOS_1:def_13_:_
 for S being COM-Struct
for s being Instruction-Sequence of S
for l being Nat holds
( s halts_at l iff s . l = halt S );

begin

notation
let S be COM-Struct ;
let i be Instruction of S;
synonym  Load i for <%S%>;
end;

registration
let S be COM-Struct ;
cluster Relation-like NAT -defined the InstructionsF of S -valued Function-like 1 -element initial for set ;
existence
 ex b1 being Function st
( b1 is initial &amp; b1 is 1 -element &amp; b1 is NAT -defined &amp; b1 is the InstructionsF of S -valued )
proofend;
end;

definition
let S be COM-Struct ;
mode preProgram of S is NAT -defined the InstructionsF of S -valued finite Function;
end;

definition
let S be COM-Struct ;
let F be non empty preProgram of S;
attrF is halt-ending  means :Def14: :: COMPOS_1:def 14
F . (LastLoc F) = halt S;
attrF is unique-halt  means :Def15: :: COMPOS_1:def 15
 for f being Nat st F . f = halt S &amp; f in dom F holds
f = LastLoc F;
end;

:: deftheorem Def14 defines halt-ending COMPOS_1:def_14_:_
 for S being COM-Struct
for F being non empty preProgram of S holds
( F is halt-ending iff F . (LastLoc F) = halt S );

:: deftheorem Def15 defines unique-halt COMPOS_1:def_15_:_
 for S being COM-Struct
for F being non empty preProgram of S holds
( F is unique-halt iff for f being Nat st F . f = halt S &amp; f in dom F holds
f = LastLoc F );

registration
let S be COM-Struct ;
cluster non empty trivial Relation-like NAT -defined the InstructionsF of S -valued Function-like finite countable V93() initial for set ;
existence
 ex b1 being preProgram of S st
( b1 is trivial &amp; b1 is initial &amp; not b1 is empty )
proofend;
end;

definition
let S be COM-Struct ;
mode Program of S is non empty initial preProgram of S;
end;

theorem :: COMPOS_1:1
canceled;

theorem :: COMPOS_1:2
for ins being Element of the InstructionsF of Trivial-COM holds InsCode ins = 0
proofend;

begin

definition
let S be COM-Struct ;
func Stop S ->  preProgram of S equals :: COMPOS_1:def 16
 Load ;
coherence
 Load is preProgram of S ;
end;

:: deftheorem  defines Stop COMPOS_1:def_16_:_
 for S being COM-Struct holds Stop S = Load ;

registration
let S be COM-Struct ;
cluster Stop S ->  non empty initial ;
coherence
 ( Stop S is initial &amp; not Stop S is empty ) ;
end;

registration
let S be COM-Struct ;
cluster Stop S ->  non empty trivial initial ;
coherence
 ( Stop S is initial &amp; not Stop S is empty &amp; Stop S is NAT -defined &amp; Stop S is the InstructionsF of S -valued &amp; Stop S is trivial ) ;
end;

Lm1: now__::_thesis:_for_S_being_COM-Struct_holds_
(_dom_(Stop_S)_=_{0}_&amp;_0_in_dom_(Stop_S)_)
let S be COM-Struct ; ::_thesis: ( dom (Stop S) = {0} &amp; 0 in dom (Stop S) )
thus  dom (Stop S) = {0} by FUNCOP_1:13; ::_thesis: 0 in dom (Stop S)
hence  0 in dom (Stop S) by TARSKI:def_1; ::_thesis: verum
end;

Lm2:  for S being COM-Struct holds (card (Stop S)) -' 1 = 0
proofend;

Lm3:  for S being COM-Struct holds LastLoc (Stop S) = 0
proofend;

registration
let S be COM-Struct ;
cluster Stop S ->  halt-ending unique-halt ;
coherence
 ( Stop S is halt-ending &amp; Stop S is unique-halt )
proofend;
end;

registration
let S be COM-Struct ;
cluster non empty trivial Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite countable V93() initial halt-ending unique-halt for set ;
existence
 ex b1 being non empty initial preProgram of S st
( b1 is halt-ending &amp; b1 is unique-halt &amp; b1 is trivial )
proofend;
end;

definition
let S be COM-Struct ;
mode MacroInstruction of S is halt-ending unique-halt Program of S;
end;

registration
let S be COM-Struct ;
cluster non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like finite countable V93() initial for set ;
existence
 ex b1 being preProgram of S st
( b1 is initial &amp; not b1 is empty )
proofend;
end;

theorem Th3: :: COMPOS_1:3
for S being COM-Struct holds 0 in dom (Stop S)
proofend;

theorem :: COMPOS_1:4
for S being COM-Struct holds card (Stop S) = 1 by AFINSQ_1:33;

Lm4:  for k being Nat holds - 1 < k
;

Lm5:  for k being Nat
for a, b, c being Element of NAT st 1 <= a &amp; 2 <= b &amp; not k < a - 1 &amp; not ( a <= k &amp; k <= (a + b) - 3 ) &amp; not k = (a + b) - 2 &amp; not (a + b) - 2 < k holds
k = a - 1
proofend;

begin

theorem Th5: :: COMPOS_1:5
for I being Instruction of Trivial-COM holds JumpPart I = 0
proofend;

theorem :: COMPOS_1:6
for T being InsType of the InstructionsF of Trivial-COM holds JumpParts T = {0}
proofend;

registration
let S be COM-Struct ;
cluster non empty trivial Relation-like NAT -defined the InstructionsF of S -valued Function-like finite  ->  non empty unique-halt for set ;
coherence
 for b1 being non empty preProgram of S st b1 is trivial holds
b1 is unique-halt
proofend;
end;

theorem :: COMPOS_1:7
canceled;

theorem Th8: :: COMPOS_1:8
for S being COM-Struct
for F being MacroInstruction of S st card F = 1 holds
F = Stop S
proofend;

theorem :: COMPOS_1:9
for S being COM-Struct holds LastLoc (Stop S) = 0 by Lm3;

begin

definition
canceled;
canceled;
canceled;
canceled;
let S be COM-Struct ;
let p be NAT -defined the InstructionsF of S -valued finite Function;
let k be Nat;
A1: dom p c= NAT by RELAT_1:def_18;
func IncAddr (p,k) ->  NAT -defined the InstructionsF of S -valued finite Function means :Def21: :: COMPOS_1:def 21
( dom it = dom p &amp; ( for m being Nat st m in dom p holds
it . m = IncAddr ((p /. m),k) ) );
existence
 ex b1 being NAT -defined the InstructionsF of S -valued finite Function st
( dom b1 = dom p &amp; ( for m being Nat st m in dom p holds
b1 . m = IncAddr ((p /. m),k) ) )
proofend;
uniqueness
 for b1, b2 being NAT -defined the InstructionsF of S -valued finite Function st dom b1 = dom p &amp; ( for m being Nat st m in dom p holds
b1 . m = IncAddr ((p /. m),k) ) &amp; dom b2 = dom p &amp; ( for m being Nat st m in dom p holds
b2 . m = IncAddr ((p /. m),k) ) holds
b1 = b2
proofend;
end;

:: deftheorem  COMPOS_1:def_17_:_
canceled;

:: deftheorem  COMPOS_1:def_18_:_
canceled;

:: deftheorem  COMPOS_1:def_19_:_
canceled;

:: deftheorem  COMPOS_1:def_20_:_
canceled;

:: deftheorem Def21 defines IncAddr COMPOS_1:def_21_:_
 for S being COM-Struct
for p being NAT -defined the InstructionsF of b1 -valued finite Function
for k being Nat
for b4 being NAT -defined the InstructionsF of b1 -valued finite Function holds
( b4 = IncAddr (p,k) iff ( dom b4 = dom p &amp; ( for m being Nat st m in dom p holds
b4 . m = IncAddr ((p /. m),k) ) ) );

registration
let S be COM-Struct ;
let F be NAT -defined the InstructionsF of S -valued finite Function;
let k be Nat;
cluster IncAddr (F,k) ->  NAT -defined the InstructionsF of S -valued finite ;
coherence
 ( IncAddr (F,k) is NAT -defined &amp; IncAddr (F,k) is the InstructionsF of S -valued ) ;
end;

registration
let S be COM-Struct ;
let F be empty NAT -defined the InstructionsF of S -valued finite Function;
let k be Nat;
cluster IncAddr (F,k) ->  empty NAT -defined the InstructionsF of S -valued finite ;
coherence
 IncAddr (F,k) is empty
proofend;
end;

registration
let S be COM-Struct ;
let F be non empty NAT -defined the InstructionsF of S -valued finite Function;
let k be Nat;
cluster IncAddr (F,k) ->  non empty NAT -defined the InstructionsF of S -valued finite ;
coherence
 not IncAddr (F,k) is empty
proofend;
end;

registration
let S be COM-Struct ;
let F be NAT -defined the InstructionsF of S -valued finite initial Function;
let k be Nat;
cluster IncAddr (F,k) ->  NAT -defined the InstructionsF of S -valued finite initial ;
coherence
 IncAddr (F,k) is initial
proofend;
end;

theorem :: COMPOS_1:10
canceled;

theorem :: COMPOS_1:11
canceled;

theorem :: COMPOS_1:12
canceled;

theorem :: COMPOS_1:13
canceled;

theorem :: COMPOS_1:14
canceled;

theorem :: COMPOS_1:15
canceled;

registration
let S be COM-Struct ;
let F be NAT -defined the InstructionsF of S -valued finite Function;
reduce IncAddr (F,0) to F;
reducibility
 IncAddr (F,0) = F
proofend;
end;

theorem :: COMPOS_1:16
for S being COM-Struct
for F being NAT -defined the InstructionsF of b1 -valued finite Function holds IncAddr (F,0) = F ;

theorem Th17: :: COMPOS_1:17
for k, m being Nat
for S being COM-Struct
for F being NAT -defined the InstructionsF of b3 -valued finite Function holds IncAddr ((IncAddr (F,k)),m) = IncAddr (F,(k + m))
proofend;

definition
let S be COM-Struct ;
let p be NAT -defined the InstructionsF of S -valued finite Function;
let k be Nat;
func Reloc (p,k) ->  NAT -defined the InstructionsF of S -valued finite Function equals :: COMPOS_1:def 22
 Shift ((IncAddr (p,k)),k);
coherence
 Shift ((IncAddr (p,k)),k) is NAT -defined the InstructionsF of S -valued finite Function ;
end;

:: deftheorem  defines Reloc COMPOS_1:def_22_:_
 for S being COM-Struct
for p being NAT -defined the InstructionsF of b1 -valued finite Function
for k being Nat holds Reloc (p,k) = Shift ((IncAddr (p,k)),k);

theorem Th18: :: COMPOS_1:18
for S being COM-Struct
for F being non empty initial preProgram of S
for G being non empty NAT -defined the InstructionsF of b1 -valued finite Function holds dom (CutLastLoc F) misses dom (Reloc (G,((card F) -' 1)))
proofend;

theorem Th19: :: COMPOS_1:19
for S being COM-Struct
for F being non empty initial unique-halt preProgram of S
for I being Nat st I in dom (CutLastLoc F) holds
(CutLastLoc F) . I <> halt S
proofend;

definition
let S be COM-Struct ;
let F, G be non empty preProgram of S;
funcF ';' G ->  preProgram of S equals :: COMPOS_1:def 23
(CutLastLoc F) +* (Reloc (G,((card F) -' 1)));
coherence
 (CutLastLoc F) +* (Reloc (G,((card F) -' 1))) is preProgram of S ;
end;

:: deftheorem  defines ';' COMPOS_1:def_23_:_
 for S being COM-Struct
for F, G being non empty preProgram of S holds F ';' G = (CutLastLoc F) +* (Reloc (G,((card F) -' 1)));

registration
let S be COM-Struct ;
let F, G be non empty NAT -defined the InstructionsF of S -valued finite Function;
clusterF ';' G ->  non empty ;
coherence
 ( not F ';' G is empty &amp; F ';' G is the InstructionsF of S -valued &amp; F ';' G is NAT -defined ) ;
end;

theorem Th20: :: COMPOS_1:20
for S being COM-Struct
for F being non empty initial preProgram of S
for G being non empty NAT -defined the InstructionsF of b1 -valued finite Function holds
( card (F ';' G) = ((card F) + (card G)) - 1 &amp; card (F ';' G) = ((card F) + (card G)) -' 1 )
proofend;

registration
let S be COM-Struct ;
let F, G be non empty initial preProgram of S;
clusterF ';' G ->  initial ;
coherence
 F ';' G is initial
proofend;
end;

theorem :: COMPOS_1:21
for S being COM-Struct
for F, G being non empty initial preProgram of S holds dom F c= dom (F ';' G)
proofend;

registration
let S be COM-Struct ;
let F, G be non empty initial preProgram of S;
clusterF ';' G ->  non empty initial ;
coherence
 ( F ';' G is initial &amp; not F ';' G is empty ) ;
end;

theorem Th22: :: COMPOS_1:22
for S being COM-Struct
for F, G being non empty initial preProgram of S holds CutLastLoc F c= CutLastLoc (F ';' G)
proofend;

theorem Th23: :: COMPOS_1:23
for S being COM-Struct
for F, G being non empty initial preProgram of S holds (F ';' G) . (LastLoc F) = (IncAddr (G,((card F) -' 1))) . 0
proofend;

theorem :: COMPOS_1:24
for S being COM-Struct
for F, G being non empty initial preProgram of S
for f being Nat st f < (card F) - 1 holds
(IncAddr (F,((card F) -' 1))) . f = (IncAddr ((F ';' G),((card F) -' 1))) . f
proofend;

registration
let S be COM-Struct ;
let F be non empty NAT -defined the InstructionsF of S -valued finite initial Function;
let G be non empty NAT -defined the InstructionsF of S -valued finite initial halt-ending Function;
clusterF ';' G ->  halt-ending ;
coherence
 F ';' G is halt-ending
proofend;
end;

registration
let S be COM-Struct ;
let F, G be non empty NAT -defined the InstructionsF of S -valued finite initial halt-ending unique-halt Function;
clusterF ';' G ->  unique-halt ;
coherence
 F ';' G is unique-halt
proofend;
end;

definition
let S be COM-Struct ;
let F, G be MacroInstruction of S;
:: original:';'
redefine funcF ';' G ->  MacroInstruction of S;
coherence
 F ';' G is MacroInstruction of S ;
end;

registration
let S be COM-Struct ;
let k be Nat;
reduce IncAddr ((Stop S),k) to  Stop S;
reducibility
 IncAddr ((Stop S),k) = Stop S
proofend;
end;

theorem :: COMPOS_1:25
for k being Nat
for S being COM-Struct holds IncAddr ((Stop S),k) = Stop S ;

theorem Th26: :: COMPOS_1:26
for k being Nat
for S being COM-Struct holds Shift ((Stop S),k) = k .--> (halt S)
proofend;

registration
let S be COM-Struct ;
let F be MacroInstruction of S;
reduceF ';' (Stop S) to F;
reducibility
 F ';' (Stop S) = F
proofend;
end;

theorem :: COMPOS_1:27
for S being COM-Struct
for F being MacroInstruction of S holds F ';' (Stop S) = F ;

registration
let S be COM-Struct ;
let F be MacroInstruction of S;
reduce(Stop S) ';' F to F;
reducibility
 (Stop S) ';' F = F
proofend;
end;

theorem Th28: :: COMPOS_1:28
for S being COM-Struct
for F being MacroInstruction of S holds (Stop S) ';' F = F ;

theorem :: COMPOS_1:29
for S being COM-Struct
for F, G, H being MacroInstruction of S holds (F ';' G) ';' H = F ';' (G ';' H)
proofend;

theorem :: COMPOS_1:30
canceled;

theorem :: COMPOS_1:31
for I being Instruction of Trivial-COM holds JumpPart I = 0 by Th5;

begin

theorem Th32: :: COMPOS_1:32
for S being COM-Struct
for k being Nat
for p being NAT -defined the InstructionsF of b1 -valued finite Function holds dom (Reloc (p,k)) = dom (Shift (p,k))
proofend;

theorem Th33: :: COMPOS_1:33
for S being COM-Struct
for k being Nat
for p being NAT -defined the InstructionsF of b1 -valued finite Function holds dom (Reloc (p,k)) =  {  (j + k) where j is Element of NAT : j in dom p  }
proofend;

theorem Th34: :: COMPOS_1:34
for S being COM-Struct
for i, j being Nat
for p being NAT -defined the InstructionsF of b1 -valued finite Function holds Shift ((IncAddr (p,i)),j) = IncAddr ((Shift (p,j)),i)
proofend;

theorem :: COMPOS_1:35
for il being Nat
for S being COM-Struct
for g being NAT -defined the InstructionsF of b2 -valued finite Function
for k being Nat
for I being Instruction of S st il in dom g &amp; I = g . il holds
IncAddr (I,k) = (Reloc (g,k)) . (il + k)
proofend;

definition
let S be COM-Struct ;
let i be Instruction of S;
:: original:Load
redefine func Load i ->  preProgram of S;
coherence
 Load is preProgram of S ;
end;

definition
let S be COM-Struct ;
let I be initial preProgram of S;
func stop I ->  preProgram of S equals :: COMPOS_1:def 24
I ^ (Stop S);
coherence
 I ^ (Stop S) is preProgram of S ;
end;

:: deftheorem  defines stop COMPOS_1:def_24_:_
 for S being COM-Struct
for I being initial preProgram of S holds stop I = I ^ (Stop S);

registration
let S be COM-Struct ;
let I be initial preProgram of S;
cluster stop I ->  non empty initial ;
correctness
coherence
( stop I is initial &amp; not stop I is empty );
;
end;

theorem :: COMPOS_1:36
for S being COM-Struct
for I being Program of S holds 0 in dom (stop I)
proofend;

begin

definition
let S be COM-Struct ;
let i be Instruction of S;
func Macro i ->  preProgram of S equals :: COMPOS_1:def 25
 stop (Load i);
coherence
 stop (Load i) is preProgram of S ;
end;

:: deftheorem  defines Macro COMPOS_1:def_25_:_
 for S being COM-Struct
for i being Instruction of S holds Macro i = stop (Load i);

registration
let S be COM-Struct ;
let i be Instruction of S;
cluster Macro i ->  non empty initial ;
coherence
 ( Macro i is initial &amp; not Macro i is empty ) ;
end;

begin

registration
let S be COM-Struct ;
cluster Stop S ->  non halt-free ;
coherence
 not Stop S is halt-free
proofend;
end;

registration
let S be COM-Struct ;
cluster non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite countable V93() initial non halt-free for set ;
existence
 ex b1 being Program of S st
( not b1 is halt-free &amp; b1 is finite )
proofend;
end;

registration
let S be COM-Struct ;
let p be NAT -defined the InstructionsF of S -valued Function;
let q be NAT -defined the InstructionsF of S -valued non halt-free Function;
clusterp +* q ->  non halt-free ;
coherence
 not p +* q is halt-free
proofend;
end;

registration
let S be COM-Struct ;
let p be NAT -defined the InstructionsF of S -valued finite non halt-free Function;
let k be Nat;
cluster Reloc (p,k) ->  NAT -defined the InstructionsF of S -valued finite non halt-free ;
coherence
 not Reloc (p,k) is halt-free
proofend;
end;

registration
let S be COM-Struct ;
cluster non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite countable V93() initial non halt-free for set ;
existence
 ex b1 being Program of S st
( not b1 is halt-free &amp; not b1 is empty )
proofend;
end;

theorem :: COMPOS_1:37
canceled;

theorem :: COMPOS_1:38
canceled;

theorem :: COMPOS_1:39
canceled;

theorem :: COMPOS_1:40
canceled;

theorem Th41: :: COMPOS_1:41
for n being Nat
for S being COM-Struct
for p, q being NAT -defined the InstructionsF of b2 -valued finite Function holds IncAddr ((p +* q),n) = (IncAddr (p,n)) +* (IncAddr (q,n))
proofend;

theorem :: COMPOS_1:42
for S being COM-Struct
for p, q being NAT -defined the InstructionsF of b1 -valued finite Function
for k being Nat holds Reloc ((p +* q),k) = (Reloc (p,k)) +* (Reloc (q,k))
proofend;

theorem :: COMPOS_1:43
for S being COM-Struct
for p being NAT -defined the InstructionsF of b1 -valued finite Function
for m, n being Nat holds Reloc ((Reloc (p,m)),n) = Reloc (p,(m + n))
proofend;

theorem :: COMPOS_1:44
for S being COM-Struct
for P, Q being NAT -defined the InstructionsF of b1 -valued finite Function
for k being Nat st P c= Q holds
Reloc (P,k) c= Reloc (Q,k)
proofend;

registration
let S be COM-Struct ;
let P be preProgram of S;
reduce Reloc (P,0) to P;
reducibility
 Reloc (P,0) = P ;
end;

theorem :: COMPOS_1:45
for S being COM-Struct
for P being preProgram of S holds Reloc (P,0) = P ;

theorem :: COMPOS_1:46
for il being Nat
for S being COM-Struct
for k being Nat
for P being preProgram of S holds
( il in dom P iff il + k in dom (Reloc (P,k)) )
proofend;

theorem :: COMPOS_1:47
for n being Nat
for S being COM-Struct
for i being Instruction of S
for f being Function of the InstructionsF of S, the InstructionsF of S st f = (id the InstructionsF of S) +* ((halt S) .--> i) holds
for s being NAT -defined the InstructionsF of b2 -valued finite Function holds IncAddr ((f * s),n) = ((id the InstructionsF of S) +* ((halt S) .--> (IncAddr (i,n)))) * (IncAddr (s,n))
proofend;

theorem :: COMPOS_1:48
for S being COM-Struct
for I, J being Program of S holds dom I misses dom (Reloc (J,(card I)))
proofend;

theorem :: COMPOS_1:49
for m being Nat
for S being COM-Struct
for I being preProgram of S holds card (Reloc (I,m)) = card I
proofend;

theorem :: COMPOS_1:50
for x being set
for S being COM-Struct
for i being Instruction of S holds
( x in dom (Load i) iff x = 0 )
proofend;

theorem :: COMPOS_1:51
for S being COM-Struct
for I being Program of S
for loc being Nat st loc in dom (stop I) &amp; (stop I) . loc <> halt S holds
loc in dom I
proofend;

theorem :: COMPOS_1:52
for S being COM-Struct
for i being Instruction of S holds
( dom (Load i) = {0} &amp; (Load i) . 0 = i ) by FUNCOP_1:13, FUNCOP_1:72;

theorem Th53: :: COMPOS_1:53
for S being COM-Struct
for i being Instruction of S holds 0 in dom (Load i)
proofend;

theorem Th54: :: COMPOS_1:54
for S being COM-Struct
for i being Instruction of S holds card (Load i) = 1
proofend;

theorem Th55: :: COMPOS_1:55
for S being COM-Struct
for I being Program of S holds card (stop I) = (card I) + 1
proofend;

theorem Th56: :: COMPOS_1:56
for S being COM-Struct
for i being Instruction of S holds card (Macro i) = 2
proofend;

theorem :: COMPOS_1:57
for S being COM-Struct
for i being Instruction of S holds
( 0 in dom (Macro i) &amp; 1 in dom (Macro i) )
proofend;

theorem :: COMPOS_1:58
for S being COM-Struct
for i being Instruction of S holds (Macro i) . 0 = i
proofend;

theorem :: COMPOS_1:59
for S being COM-Struct
for i being Instruction of S holds (Macro i) . 1 = halt S
proofend;

theorem Th60: :: COMPOS_1:60
for x being set
for S being COM-Struct
for i being Instruction of S holds
( x in dom (Macro i) iff ( x = 0 or x = 1 ) )
proofend;

theorem :: COMPOS_1:61
for S being COM-Struct
for i being Instruction of S holds dom (Macro i) = {0,1}
proofend;

theorem :: COMPOS_1:62
for S being COM-Struct
for I being Program of S
for loc being Nat st loc in dom I holds
loc in dom (stop I)
proofend;

theorem :: COMPOS_1:63
for S being COM-Struct
for loc being Nat
for I being initial preProgram of S st loc in dom I holds
(stop I) . loc = I . loc by AFINSQ_1:def_3;

theorem :: COMPOS_1:64
for S being COM-Struct
for I being Program of S holds
( card I in dom (stop I) &amp; (stop I) . (card I) = halt S )
proofend;

:: from SCMPDS_7, 2011.05.27, A.T.
theorem Th65: :: COMPOS_1:65
for n being Nat
for S being COM-Struct
for I being Program of S
for loc being Nat st loc in dom I holds
(Shift ((stop I),n)) . (loc + n) = (Shift (I,n)) . (loc + n)
proofend;

theorem :: COMPOS_1:66
for n being Nat
for S being COM-Struct
for I being Program of S holds (Shift ((stop I),n)) . n = (Shift (I,n)) . n
proofend;

:: from SCMPDS_5, 2011.05.27,A.T.
registration
let S be COM-Struct ;
cluster empty Relation-like NAT -defined the InstructionsF of S -valued Function-like finite countable V93() for set ;
existence
 ex b1 being preProgram of S st b1 is empty
proofend;
end;

registration
let S be COM-Struct ;
cluster empty Relation-like NAT -defined the InstructionsF of S -valued Function-like finite  ->  halt-free for set ;
coherence
 for b1 being preProgram of S st b1 is empty holds
b1 is halt-free
proofend;
end;

definition
canceled;
let S be COM-Struct ;
let IT be NAT -defined the InstructionsF of S -valued Function;
redefine attr IT is halt-free  means :Def27: :: COMPOS_1:def 27
 for x being Nat st x in dom IT holds
IT . x <> halt S;
compatibility
 ( IT is halt-free iff for x being Nat st x in dom IT holds
IT . x <> halt S )
proofend;
end;

:: deftheorem  COMPOS_1:def_26_:_
canceled;

:: deftheorem Def27 defines halt-free COMPOS_1:def_27_:_
 for S being COM-Struct
for IT being NAT -defined the InstructionsF of b1 -valued Function holds
( IT is halt-free iff for x being Nat st x in dom IT holds
IT . x <> halt S );

registration
let S be COM-Struct ;
cluster non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like finite halt-free  ->  non empty unique-halt for set ;
coherence
 for b1 being non empty preProgram of S st b1 is halt-free holds
b1 is unique-halt
proofend;
end;

theorem :: COMPOS_1:67
for S being COM-Struct
for i being Instruction of S holds rng (Macro i) = {i,(halt S)}
proofend;

registration
let S be COM-Struct ;
let p be initial preProgram of S;
reduce CutLastLoc (stop p) to p;
reducibility
 CutLastLoc (stop p) = p by AFINSQ_2:83;
end;

theorem :: COMPOS_1:68
for S being COM-Struct
for p being initial preProgram of S holds CutLastLoc (stop p) = p ;

registration
let S be COM-Struct ;
let p be initial halt-free preProgram of S;
cluster stop p ->  unique-halt ;
coherence
 stop p is unique-halt
proofend;
end;

registration
let S be COM-Struct ;
let I be Program of S;
let J be non halt-free Program of S;
clusterI ';' J ->  non halt-free ;
coherence
 not I ';' J is halt-free ;
end;

theorem :: COMPOS_1:69
for S being COM-Struct
for I being Program of S holds CutLastLoc (stop I) = I ;

theorem :: COMPOS_1:70
for S being COM-Struct holds InsCode (halt S) = 0 by RECDEF_2:def_1;