:: COMPOS_1 semantic presentation

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,{},{}]}
proof
take S = COM-Struct(# {[0,{},{}]} #); ::_thesis: the InstructionsF of S = {[0,{},{}]}
thus  the InstructionsF of S = {[0,{},{}]} ; ::_thesis: verum
end;
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;

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
proof
A1: k in NAT by ORDINAL1:def_12;
 dom P = NAT by PARTFUN1:def_2;
then A2: P . k in rng P by A1, FUNCT_1:3;
 rng P c= the InstructionsF of S by RELAT_1:def_19;
hence  P . k is Instruction of S by A2; ::_thesis: verum
end;
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 )
proof
thus  ( s halts_at l implies s . l = halt S ) by Def12; ::_thesis: ( s . l = halt S implies s halts_at l )
assume A1: s . l = halt S ; ::_thesis: s halts_at l
 l in NAT by ORDINAL1:def_12;
hence  l in dom s by PARTFUN1:def_2; :: according to COMPOS_1:def_12 ::_thesis: s . l = halt S
thus  s . l = halt S by A1; ::_thesis: verum
end;
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 & b1 is 1 -element & b1 is NAT -defined & b1 is the InstructionsF of S -valued )
proof
set p = <% the Instruction of S%>;
take  <% the Instruction of S%> ; ::_thesis: ( <% the Instruction of S%> is initial & <% the Instruction of S%> is 1 -element & <% the Instruction of S%> is NAT -defined & <% the Instruction of S%> is the InstructionsF of S -valued )
thus  ( <% the Instruction of S%> is initial & <% the Instruction of S%> is 1 -element & <% the Instruction of S%> is NAT -defined & <% the Instruction of S%> is the InstructionsF of S -valued ) ; ::_thesis: verum
end;
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 & 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 & 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 & b1 is initial & not b1 is empty )
proof
reconsider F = <%(halt S)%> as non empty initial preProgram of S ;
take  F ; ::_thesis: ( F is trivial & F is initial & not F is empty )
thus  ( F is trivial & F is initial & not F is empty ) ; ::_thesis: verum
end;
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
proof
let ins be Element of the InstructionsF of Trivial-COM; ::_thesis: InsCode ins = 0
 the InstructionsF of Trivial-COM = {[0,{},{}]} by Def8;
then  ins = [0,{},{}] by TARSKI:def_1;
hence  InsCode ins = 0 by RECDEF_2:def_1; ::_thesis: verum
end;

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 & not Stop S is empty ) ;
end;

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

Lm1: now__::_thesis:_for_S_being_COM-Struct_holds_
(_dom_(Stop_S)_=_{0}_&_0_in_dom_(Stop_S)_)
let S be COM-Struct ; ::_thesis: ( dom (Stop S) = {0} & 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
proof
let S be COM-Struct ; ::_thesis: (card (Stop S)) -' 1 = 0
thus (card (Stop S)) -' 1 = (card (Stop S)) - 1 by PRE_CIRC:20
.= 1 - 1 by AFINSQ_1:33
.= 0 ; ::_thesis: verum
end;

Lm3:  for S being COM-Struct holds LastLoc (Stop S) = 0
proof
let S be COM-Struct ; ::_thesis: LastLoc (Stop S) = 0
 (card (Stop S)) -' 1 = 0 by Lm2;
hence  LastLoc (Stop S) = 0 by AFINSQ_1:70; ::_thesis: verum
end;

registration
let S be COM-Struct ;
cluster Stop S ->  halt-ending unique-halt ;
coherence
 ( Stop S is halt-ending & Stop S is unique-halt )
proof
thus (Stop S) . (LastLoc (Stop S)) = (0 .--> (halt S)) . 0 by Lm3
.= halt S by FUNCOP_1:72 ; :: according to COMPOS_1:def_14 ::_thesis: Stop S is unique-halt
let l be Nat; :: according to COMPOS_1:def_15 ::_thesis: ( (Stop S) . l = halt S & l in dom (Stop S) implies l = LastLoc (Stop S) )
assume  (Stop S) . l = halt S ; ::_thesis: ( not l in dom (Stop S) or l = LastLoc (Stop S) )
assume  l in dom (Stop S) ; ::_thesis: l = LastLoc (Stop S)
then  l in {0} by Lm1;
then  l = 0 by TARSKI:def_1;
hence  l = LastLoc (Stop S) by Lm3; ::_thesis: verum
end;
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 & b1 is unique-halt & b1 is trivial )
proof
take F = Stop S; ::_thesis: ( F is halt-ending & F is unique-halt & F is trivial )
thus  ( F is halt-ending & F is unique-halt & F is trivial ) ; ::_thesis: verum
end;
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 & not b1 is empty )
proof
take  Stop S ; ::_thesis: ( Stop S is initial & not Stop S is empty )
thus  ( Stop S is initial & not Stop S is empty ) ; ::_thesis: verum
end;
end;

theorem Th3: :: COMPOS_1:3
for S being COM-Struct holds 0 in dom (Stop S)
proof
let S be COM-Struct ; ::_thesis: 0 in dom (Stop S)
 dom (Stop S) = 1 by AFINSQ_1:33;
hence  0 in dom (Stop S) by CARD_1:49, TARSKI:def_1; ::_thesis: verum
end;

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 & 2 <= b & not k < a - 1 & not ( a <= k & k <= (a + b) - 3 ) & not k = (a + b) - 2 & not (a + b) - 2 < k holds
k = a - 1
proof
let k be Nat; ::_thesis: for a, b, c being Element of NAT st 1 <= a & 2 <= b & not k < a - 1 & not ( a <= k & k <= (a + b) - 3 ) & not k = (a + b) - 2 & not (a + b) - 2 < k holds
k = a - 1
let a, b, c be Element of NAT ; ::_thesis: ( 1 <= a & 2 <= b & not k < a - 1 & not ( a <= k & k <= (a + b) - 3 ) & not k = (a + b) - 2 & not (a + b) - 2 < k implies k = a - 1 )
assume that
A1: 1 <= a and
A2: 2 <= b and
A3: a - 1 <= k and
A4: ( a > k or k > (a + b) - 3 ) and
A5: k <> (a + b) - 2 and
A6: k <= (a + b) - 2 ; ::_thesis: k = a - 1
A7: a - 1 is Element of NAT by A1, INT_1:5;
now__::_thesis:_(_(_k_<_a_&_k_<=_a_-_1_)_or_(_(a_+_b)_-_3_<_k_&_k_<=_a_-_1_)_)
percases ( k < a or (a + b) - 3 < k ) by A4;
case k < a ; ::_thesis: k <= a - 1
then  k < (a - 1) + 1 ;
hence  k <= a - 1 by A7, NAT_1:13; ::_thesis: verum
end;
caseA8: (a + b) - 3 < k ; ::_thesis: k <= a - 1
 1 + 2 <= a + b by A1, A2, XREAL_1:7;
then A9: (a + b) - 3 is Element of NAT by INT_1:5;
 k < ((a + b) - 3) + 1 by A5, A6, XXREAL_0:1;
hence  k <= a - 1 by A8, A9, NAT_1:13; ::_thesis: verum
end;
end;
end;
hence  k = a - 1 by A3, XXREAL_0:1; ::_thesis: verum
end;

begin

theorem Th5: :: COMPOS_1:5
for I being Instruction of Trivial-COM holds JumpPart I = 0
proof
let I be Instruction of Trivial-COM; ::_thesis: JumpPart I = 0
 the InstructionsF of Trivial-COM = {[0,0,0]} by Def8;
then  I = [0,0,0] by TARSKI:def_1;
hence  JumpPart I = 0 by RECDEF_2:def_2; ::_thesis: verum
end;

theorem :: COMPOS_1:6
for T being InsType of the InstructionsF of Trivial-COM holds JumpParts T = {0}
proof
let T be InsType of the InstructionsF of Trivial-COM; ::_thesis: JumpParts T = {0}
set A =  {  (JumpPart I) where I is Instruction of Trivial-COM : InsCode I = T  }  ;
 {0} =  {  (JumpPart I) where I is Instruction of Trivial-COM : InsCode I = T  }
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis:  {  (JumpPart I) where I is Instruction of Trivial-COM : InsCode I = T  }  c= {0}
let a be set ; ::_thesis: ( a in {0} implies a in  {  (JumpPart I) where I is Instruction of Trivial-COM : InsCode I = T  }  )
assume  a in {0} ; ::_thesis: a in  {  (JumpPart I) where I is Instruction of Trivial-COM : InsCode I = T  }
then A1: a = 0 by TARSKI:def_1;
 the InstructionsF of Trivial-COM = {[0,0,0]} by Def8;
then A2: InsCodes the InstructionsF of Trivial-COM = {0} by MCART_1:92;
A3: T = 0 by A2, TARSKI:def_1;
 [0,0,0] = halt Trivial-COM ;
then reconsider I = [0,0,0] as Instruction of Trivial-COM ;
A4: JumpPart I = 0 by Th5;
 InsCode I = 0 by RECDEF_2:def_1;
hence  a in  {  (JumpPart I) where I is Instruction of Trivial-COM : InsCode I = T  }  by A1, A3, A4; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  (JumpPart I) where I is Instruction of Trivial-COM : InsCode I = T  }  or a in {0} )
assume  a in  {  (JumpPart I) where I is Instruction of Trivial-COM : InsCode I = T  }  ; ::_thesis: a in {0}
then  ex I being Instruction of Trivial-COM st
( a = JumpPart I & InsCode I = T ) ;
then  a = 0 by Th5;
hence  a in {0} by TARSKI:def_1; ::_thesis: verum
end;
hence  JumpParts T = {0} ; ::_thesis: verum
end;

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
proof
let F be non empty preProgram of S; ::_thesis: ( F is trivial implies F is unique-halt )
assume A1: F is trivial ; ::_thesis: F is unique-halt
let f be Nat; :: according to COMPOS_1:def_15 ::_thesis: ( F . f = halt S & f in dom F implies f = LastLoc F )
assume that
 F . f = halt S and
A2: f in dom F ; ::_thesis: f = LastLoc F
consider x being set  such that
A3: F = {x} by A1, ZFMISC_1:131;
 x in F by A3, TARSKI:def_1;
then consider a, b being set  such that
A4: [a,b] = x by RELAT_1:def_1;
A5: LastLoc F in dom F by VALUED_1:30;
A6: dom F = {a} by A3, A4, RELAT_1:9;
hence f = a by A2, TARSKI:def_1
.= LastLoc F by A5, A6, TARSKI:def_1 ;
::_thesis: verum
end;
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
proof
let S be COM-Struct ; ::_thesis: for F being MacroInstruction of S st card F = 1 holds
F = Stop S
let F be MacroInstruction of S; ::_thesis: ( card F = 1 implies F = Stop S )
assume A1: card F = 1 ; ::_thesis: F = Stop S
then consider x being set  such that
A2: F = {x} by CARD_2:42;
 x in F by A2, TARSKI:def_1;
then consider a, b being set  such that
A3: [a,b] = x by RELAT_1:def_1;
A4: dom F = {a} by A2, A3, RELAT_1:9;
A5: 0 in dom F by AFINSQ_1:65;
then A6: a = 0 by A4;
(card F) -' 1 = (card F) - 1 by PRE_CIRC:20
.= 0 by A1 ;
then  LastLoc F = 0 by AFINSQ_1:70;
then  F . 0 = halt S by Def14;
then  halt S in rng F by A5, FUNCT_1:def_3;
then  halt S in {b} by A2, A3, RELAT_1:9;
then F = {[0,(halt S)]} by A2, A3, A6, TARSKI:def_1
.= 0 .--> (halt S) by FUNCT_4:82 ;
hence  F = Stop S ; ::_thesis: verum
end;

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 & ( 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 & ( for m being Nat st m in dom p holds
b1 . m = IncAddr ((p /. m),k) ) )
proof
defpred S1[ set , set ] means  ex m being Element of NAT st
( $1 = m & $2 = IncAddr ((p /. m),k) );
A2: for e being set st e in dom p holds
ex u being set st S1[e,u]
proof
let e be set ; ::_thesis: ( e in dom p implies ex u being set st S1[e,u] )
assume  e in dom p ; ::_thesis: ex u being set st S1[e,u]
then reconsider l = e as Element of NAT by A1;
consider m being Nat such that
A3: l = m ;
take  IncAddr ((p /. m),k) ; ::_thesis: S1[e, IncAddr ((p /. m),k)]
thus  S1[e, IncAddr ((p /. m),k)] by A3; ::_thesis: verum
end;
consider f being Function such that
A4: dom f = dom p and
A5: for e being set st e in dom p holds
S1[e,f . e] from CLASSES1:sch_1(A2);
A6: rng f c= the InstructionsF of S
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in rng f or e in the InstructionsF of S )
assume  e in rng f ; ::_thesis: e in the InstructionsF of S
then consider u being set  such that
A7: u in dom f and
A8: e = f . u by FUNCT_1:def_3;
 S1[u,f . u] by A7, A5, A4;
hence  e in the InstructionsF of S by A8; ::_thesis: verum
end;
reconsider f = f as NAT -defined the InstructionsF of S -valued finite Function by A1, A4, A6, FINSET_1:10, RELAT_1:def_18, RELAT_1:def_19;
take  f ; ::_thesis: ( dom f = dom p & ( for m being Nat st m in dom p holds
f . m = IncAddr ((p /. m),k) ) )
thus  dom f = dom p by A4; ::_thesis: for m being Nat st m in dom p holds
f . m = IncAddr ((p /. m),k)
let m be Nat; ::_thesis: ( m in dom p implies f . m = IncAddr ((p /. m),k) )
assume  m in dom p ; ::_thesis: f . m = IncAddr ((p /. m),k)
then  ex j being Element of NAT st
( m = j & f . m = IncAddr ((p /. j),k) ) by A5;
hence  f . m = IncAddr ((p /. m),k) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being NAT -defined the InstructionsF of S -valued finite Function st dom b1 = dom p & ( for m being Nat st m in dom p holds
b1 . m = IncAddr ((p /. m),k) ) & dom b2 = dom p & ( for m being Nat st m in dom p holds
b2 . m = IncAddr ((p /. m),k) ) holds
b1 = b2
proof
let IT1, IT2 be NAT -defined the InstructionsF of S -valued finite Function; ::_thesis: ( dom IT1 = dom p & ( for m being Nat st m in dom p holds
IT1 . m = IncAddr ((p /. m),k) ) & dom IT2 = dom p & ( for m being Nat st m in dom p holds
IT2 . m = IncAddr ((p /. m),k) ) implies IT1 = IT2 )
assume that
A9: dom IT1 = dom p and
A10: for m being Nat st m in dom p holds
IT1 . m = IncAddr ((p /. m),k) and
A11: dom IT2 = dom p and
A12: for m being Nat st m in dom p holds
IT2 . m = IncAddr ((p /. m),k) ; ::_thesis: IT1 = IT2
 for x being set st x in dom p holds
IT1 . x = IT2 . x
proof
let x be set ; ::_thesis: ( x in dom p implies IT1 . x = IT2 . x )
assume A13: x in dom p ; ::_thesis: IT1 . x = IT2 . x
then reconsider l = x as Element of NAT by A1;
consider m being Nat such that
A14: l = m ;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
thus IT1 . x = IncAddr ((p /. m),k) by A10, A13, A14
.= IT2 . x by A12, A13, A14 ; ::_thesis: verum
end;
hence  IT1 = IT2 by A9, A11, FUNCT_1:2; ::_thesis: verum
end;
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 & ( 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 & 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
proof
assume  not IncAddr (F,k) is empty ; ::_thesis: contradiction
then reconsider f = IncAddr (F,k) as non empty Function ;
A1: dom f <> {} ;
 dom (IncAddr (F,k)) = dom F by Def21;
hence  contradiction by A1; ::_thesis: verum
end;
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
proof
 dom (IncAddr (F,k)) = dom F by Def21;
hence  not IncAddr (F,k) is empty ; ::_thesis: verum
end;
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
proof
 dom (IncAddr (F,k)) = dom F by Def21;
hence  IncAddr (F,k) is initial by AFINSQ_1:67; ::_thesis: verum
end;
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
proof
 for m being Nat st m in dom F holds
F . m = IncAddr ((F /. m),0)
proof
let m be Nat; ::_thesis: ( m in dom F implies F . m = IncAddr ((F /. m),0) )
assume  m in dom F ; ::_thesis: F . m = IncAddr ((F /. m),0)
then  F /. m = F . m by PARTFUN1:def_6;
hence  F . m = IncAddr ((F /. m),0) by COMPOS_0:3; ::_thesis: verum
end;
hence  IncAddr (F,0) = F by Def21; ::_thesis: verum
end;
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))
proof
let k, m be Nat; ::_thesis: for S being COM-Struct
for F being NAT -defined the InstructionsF of b1 -valued finite Function holds IncAddr ((IncAddr (F,k)),m) = IncAddr (F,(k + m))
let S be COM-Struct ; ::_thesis: for F being NAT -defined the InstructionsF of S -valued finite Function holds IncAddr ((IncAddr (F,k)),m) = IncAddr (F,(k + m))
let F be NAT -defined the InstructionsF of S -valued finite Function; ::_thesis: IncAddr ((IncAddr (F,k)),m) = IncAddr (F,(k + m))
A1: dom (IncAddr ((IncAddr (F,k)),m)) = dom (IncAddr (F,k)) by Def21
.= dom F by Def21 ;
A2: dom (IncAddr (F,(k + m))) = dom F by Def21;
 for x being set st x in dom F holds
(IncAddr ((IncAddr (F,k)),m)) . x = (IncAddr (F,(k + m))) . x
proof
let x be set ; ::_thesis: ( x in dom F implies (IncAddr ((IncAddr (F,k)),m)) . x = (IncAddr (F,(k + m))) . x )
assume A3: x in dom F ; ::_thesis: (IncAddr ((IncAddr (F,k)),m)) . x = (IncAddr (F,(k + m))) . x
reconsider x = x as Element of NAT by A3, ORDINAL1:def_12;
A4: x in dom (IncAddr (F,k)) by A3, Def21;
A5: IncAddr ((F /. x),k) = (IncAddr (F,k)) . x by A3, Def21
.= (IncAddr (F,k)) /. x by A4, PARTFUN1:def_6 ;
(IncAddr ((IncAddr (F,k)),m)) . x = IncAddr (((IncAddr (F,k)) /. x),m) by A4, Def21
.= IncAddr ((F /. x),(k + m)) by A5, COMPOS_0:7
.= (IncAddr (F,(k + m))) . x by A3, Def21 ;
hence  (IncAddr ((IncAddr (F,k)),m)) . x = (IncAddr (F,(k + m))) . x ; ::_thesis: verum
end;
hence  IncAddr ((IncAddr (F,k)),m) = IncAddr (F,(k + m)) by A1, A2, FUNCT_1:2; ::_thesis: verum
end;

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)))
proof
let S be COM-Struct ; ::_thesis: for F being non empty initial preProgram of S
for G being non empty NAT -defined the InstructionsF of S -valued finite Function holds dom (CutLastLoc F) misses dom (Reloc (G,((card F) -' 1)))
let F be non empty initial preProgram of S; ::_thesis: for G being non empty NAT -defined the InstructionsF of S -valued finite Function holds dom (CutLastLoc F) misses dom (Reloc (G,((card F) -' 1)))
let G be non empty NAT -defined the InstructionsF of S -valued finite Function; ::_thesis: dom (CutLastLoc F) misses dom (Reloc (G,((card F) -' 1)))
set k = (card F) -' 1;
assume  not dom (CutLastLoc F) misses dom (Reloc (G,((card F) -' 1))) ; ::_thesis: contradiction
then consider il being set  such that
A1: il in (dom (CutLastLoc F)) /\ (dom (Reloc (G,((card F) -' 1)))) by XBOOLE_0:4;
A2: il in dom (CutLastLoc F) by A1, XBOOLE_0:def_4;
A3: il in dom (Reloc (G,((card F) -' 1))) by A1, XBOOLE_0:def_4;
 dom (Reloc (G,((card F) -' 1))) =  {  (m + ((card F) -' 1)) where m is Element of NAT : m in dom (IncAddr (G,((card F) -' 1)))  }  by VALUED_1:def_12;
then consider m being Element of NAT  such that
A4: il = m + ((card F) -' 1) and
 m in dom (IncAddr (G,((card F) -' 1))) by A3;
reconsider f = CutLastLoc F as non empty NAT -defined finite Function by A1, RELAT_1:38;
 m + ((card F) -' 1) <= LastLoc f by A2, A4, VALUED_1:32;
then A5: m + ((card F) -' 1) <= (card f) -' 1 by AFINSQ_1:70;
A6: card f = (card F) - 1 by VALUED_1:38
.= (card F) -' 1 by PRE_CIRC:20 ;
percases ( ((card F) -' 1) - 1 >= 0 or ((card F) -' 1) - 1 < 0 ) ;
suppose ((card F) -' 1) - 1 >= 0 ; ::_thesis: contradiction
then  m + ((card F) -' 1) <= ((card F) -' 1) - 1 by A5, A6, XREAL_0:def_2;
then  (m + ((card F) -' 1)) - ((card F) -' 1) <= (((card F) -' 1) - 1) - ((card F) -' 1) by XREAL_1:9;
hence  contradiction by Lm4; ::_thesis: verum
end;
suppose ((card F) -' 1) - 1 < 0 ; ::_thesis: contradiction
then  ( m + ((card F) -' 1) = 0 or m + ((card F) -' 1) < 0 ) by A5, A6, XREAL_0:def_2;
hence  contradiction by A6; ::_thesis: verum
end;
end;
end;

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
proof
let S be COM-Struct ; ::_thesis: 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
let F be non empty initial unique-halt preProgram of S; ::_thesis: for I being Nat st I in dom (CutLastLoc F) holds
(CutLastLoc F) . I <> halt S
let I be Nat; ::_thesis: ( I in dom (CutLastLoc F) implies (CutLastLoc F) . I <> halt S )
assume that
A1: I in dom (CutLastLoc F) and
A2: (CutLastLoc F) . I = halt S ; ::_thesis: contradiction
A3: dom (CutLastLoc F) c= dom F by GRFUNC_1:2;
 F . I = halt S by A1, A2, GRFUNC_1:2;
then A4: I = LastLoc F by A1, A3, Def15;
 dom (CutLastLoc F) = (dom F) \ {(LastLoc F)} by VALUED_1:36;
then  not I in {(LastLoc F)} by A1, XBOOLE_0:def_5;
hence  contradiction by A4, TARSKI:def_1; ::_thesis: verum
end;

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 & F ';' G is the InstructionsF of S -valued & 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 & card (F ';' G) = ((card F) + (card G)) -' 1 )
proof
let S be COM-Struct ; ::_thesis: for F being non empty initial preProgram of S
for G being non empty NAT -defined the InstructionsF of S -valued finite Function holds
( card (F ';' G) = ((card F) + (card G)) - 1 & card (F ';' G) = ((card F) + (card G)) -' 1 )
let F be non empty initial preProgram of S; ::_thesis: for G being non empty NAT -defined the InstructionsF of S -valued finite Function holds
( card (F ';' G) = ((card F) + (card G)) - 1 & card (F ';' G) = ((card F) + (card G)) -' 1 )
let G be non empty NAT -defined the InstructionsF of S -valued finite Function; ::_thesis: ( card (F ';' G) = ((card F) + (card G)) - 1 & card (F ';' G) = ((card F) + (card G)) -' 1 )
set k = (card F) -' 1;
 dom (IncAddr (G,((card F) -' 1))), dom (Reloc (G,((card F) -' 1))) are_equipotent by VALUED_1:27;
then A1: IncAddr (G,((card F) -' 1)), Reloc (G,((card F) -' 1)) are_equipotent by PRE_CIRC:21;
 dom (CutLastLoc F) misses dom (Reloc (G,((card F) -' 1))) by Th18;
hence  card (F ';' G) = (card (CutLastLoc F)) + (card (Reloc (G,((card F) -' 1)))) by PRE_CIRC:22
.= (card (CutLastLoc F)) + (card (IncAddr (G,((card F) -' 1)))) by A1, CARD_1:5
.= (card (CutLastLoc F)) + (card (dom (IncAddr (G,((card F) -' 1))))) by CARD_1:62
.= (card (CutLastLoc F)) + (card (dom G)) by Def21
.= (card (CutLastLoc F)) + (card G) by CARD_1:62
.= ((card F) - 1) + (card G) by VALUED_1:38
.= ((card F) + (card G)) - 1 ;
::_thesis: card (F ';' G) = ((card F) + (card G)) -' 1
hence  card (F ';' G) = ((card F) + (card G)) -' 1 by XREAL_0:def_2; ::_thesis: verum
end;

registration
let S be COM-Struct ;
let F, G be non empty initial preProgram of S;
clusterF ';' G ->  initial ;
coherence
 F ';' G is initial
proof
set P = F ';' G;
let f, n be Nat; :: according to AFINSQ_1:def_12 ::_thesis: ( not n in proj1 (F ';' G) or n <= f or f in proj1 (F ';' G) )
assume that
A1: n in dom (F ';' G) and
A2: f < n ; ::_thesis: f in proj1 (F ';' G)
set k = (card F) -' 1;
A3: dom (F ';' G) = (dom (CutLastLoc F)) \/ (dom (Reloc (G,((card F) -' 1)))) by FUNCT_4:def_1;
percases ( n in dom (CutLastLoc F) or n in dom (Reloc (G,((card F) -' 1))) ) by A1, A3, XBOOLE_0:def_3;
suppose n in dom (CutLastLoc F) ; ::_thesis: f in proj1 (F ';' G)
then  f in dom (CutLastLoc F) by A2, AFINSQ_1:def_12;
hence  f in proj1 (F ';' G) by A3, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose n in dom (Reloc (G,((card F) -' 1))) ; ::_thesis: f in proj1 (F ';' G)
then  n in  {  (w + ((card F) -' 1)) where w is Element of NAT : w in dom (IncAddr (G,((card F) -' 1)))  }  by VALUED_1:def_12;
then consider m being Element of NAT  such that
A4: n = m + ((card F) -' 1) and
A5: m in dom (IncAddr (G,((card F) -' 1))) ;
A6: m in dom G by A5, Def21;
now__::_thesis:_(_(_f_<_(card_F)_-'_1_&_f_in_dom_(CutLastLoc_F)_)_or_(_f_>=_(card_F)_-'_1_&_f_in_dom_(Reloc_(G,((card_F)_-'_1)))_)_)
percases ( f < (card F) -' 1 or f >= (card F) -' 1 ) ;
caseA7: f < (card F) -' 1 ; ::_thesis: f in dom (CutLastLoc F)
then  f < (card F) - 1 by PRE_CIRC:20;
then  1 + f < 1 + ((card F) - 1) by XREAL_1:6;
then A8: 1 + f in dom F by AFINSQ_1:66;
 f < 1 + f by NAT_1:19;
then A9: f in dom F by A8, AFINSQ_1:def_12;
 f <> LastLoc F by A7, AFINSQ_1:70;
then  not f in {(LastLoc F)} by TARSKI:def_1;
then  f in (dom F) \ {(LastLoc F)} by A9, XBOOLE_0:def_5;
hence  f in dom (CutLastLoc F) by VALUED_1:36; ::_thesis: verum
end;
case f >= (card F) -' 1 ; ::_thesis: f in dom (Reloc (G,((card F) -' 1)))
then consider l1 being Nat such that
A10: f = ((card F) -' 1) + l1 by NAT_1:10;
reconsider l1 = l1 as Element of NAT by ORDINAL1:def_12;
A11: dom (Reloc (G,((card F) -' 1))) =  {  (w + ((card F) -' 1)) where w is Element of NAT : w in dom (IncAddr (G,((card F) -' 1)))  }  by VALUED_1:def_12;
 ( l1 < m or l1 = m ) by A10, A4, A2, XREAL_1:6;
then  l1 in dom G by A6, AFINSQ_1:def_12;
then  l1 in dom (IncAddr (G,((card F) -' 1))) by Def21;
hence  f in dom (Reloc (G,((card F) -' 1))) by A11, A10; ::_thesis: verum
end;
end;
end;
hence  f in proj1 (F ';' G) by A3, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
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)
proof
let S be COM-Struct ; ::_thesis: for F, G being non empty initial preProgram of S holds dom F c= dom (F ';' G)
let F, G be non empty initial preProgram of S; ::_thesis: dom F c= dom (F ';' G)
set P = F ';' G;
A1: dom (F ';' G) = (dom (CutLastLoc F)) \/ (dom (Reloc (G,((card F) -' 1)))) by FUNCT_4:def_1;
A2: dom F = (dom (CutLastLoc F)) \/ {(LastLoc F)} by VALUED_1:37;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom F or x in dom (F ';' G) )
assume A3: x in dom F ; ::_thesis: x in dom (F ';' G)
percases ( x in dom (CutLastLoc F) or x in {(LastLoc F)} ) by A2, A3, XBOOLE_0:def_3;
suppose x in dom (CutLastLoc F) ; ::_thesis: x in dom (F ';' G)
hence  x in dom (F ';' G) by A1, XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA4: x in {(LastLoc F)} ; ::_thesis: x in dom (F ';' G)
then A5: x = LastLoc F by TARSKI:def_1;
reconsider f = x as Element of NAT by A4;
A6: f = (card F) -' 1 by A5, AFINSQ_1:70
.= ((card F) - 1) + 0 by PRE_CIRC:20 ;
card (F ';' G) = ((card F) + (card G)) - 1 by Th20
.= ((card F) - 1) + (card G) ;
then  f < card (F ';' G) by A6, XREAL_1:6;
hence  x in dom (F ';' G) by AFINSQ_1:66; ::_thesis: verum
end;
end;
end;

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 & 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)
proof
let S be COM-Struct ; ::_thesis: for F, G being non empty initial preProgram of S holds CutLastLoc F c= CutLastLoc (F ';' G)
let F, G be non empty initial preProgram of S; ::_thesis: CutLastLoc F c= CutLastLoc (F ';' G)
set k = (card F) -' 1;
set P = F ';' G;
A1: dom (F ';' G) = (dom (CutLastLoc F)) \/ (dom (Reloc (G,((card F) -' 1)))) by FUNCT_4:def_1;
A2: dom (CutLastLoc F) =  {  m where m is Element of NAT : m < card (CutLastLoc F)  }  by AFINSQ_1:68;
A3: card (CutLastLoc (F ';' G)) = (card (F ';' G)) - 1 by VALUED_1:38
.= (((card F) + (card G)) - 1) - 1 by Th20
.= ((card F) - 1) + ((card G) - 1) ;
A4: for m being Element of NAT st m < card (CutLastLoc F) holds
m < card (CutLastLoc (F ';' G))
proof
let m be Element of NAT ; ::_thesis: ( m < card (CutLastLoc F) implies m < card (CutLastLoc (F ';' G)) )
assume A5: m < card (CutLastLoc F) ; ::_thesis: m < card (CutLastLoc (F ';' G))
A6: card (CutLastLoc F) = (card F) - 1 by VALUED_1:38;
 1 <= card G by NAT_1:14;
then  1 - 1 <= (card G) - 1 by XREAL_1:9;
then  ((card F) - 1) + 0 <= ((card F) - 1) + ((card G) - 1) by XREAL_1:6;
hence  m < card (CutLastLoc (F ';' G)) by A3, A5, A6, XXREAL_0:2; ::_thesis: verum
end;
A7: dom (CutLastLoc F) c= dom (CutLastLoc (F ';' G))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (CutLastLoc F) or x in dom (CutLastLoc (F ';' G)) )
assume  x in dom (CutLastLoc F) ; ::_thesis: x in dom (CutLastLoc (F ';' G))
then consider m being Element of NAT  such that
A8: x = m and
A9: m < card (CutLastLoc F) by A2;
 m < card (CutLastLoc (F ';' G)) by A4, A9;
hence  x in dom (CutLastLoc (F ';' G)) by A8, AFINSQ_1:66; ::_thesis: verum
end;
 for x being set st x in dom (CutLastLoc F) holds
(CutLastLoc F) . x = (CutLastLoc (F ';' G)) . x
proof
let x be set ; ::_thesis: ( x in dom (CutLastLoc F) implies (CutLastLoc F) . x = (CutLastLoc (F ';' G)) . x )
assume A10: x in dom (CutLastLoc F) ; ::_thesis: (CutLastLoc F) . x = (CutLastLoc (F ';' G)) . x
then consider m being Element of NAT  such that
A11: x = m and
A12: m < card (CutLastLoc F) by A2;
A13: dom (Reloc (G,((card F) -' 1))) =  {  (w + ((card F) -' 1)) where w is Element of NAT : w in dom (IncAddr (G,((card F) -' 1)))  }  by VALUED_1:def_12;
A14: now__::_thesis:_not_x_in_dom_(Reloc_(G,((card_F)_-'_1)))
assume  x in dom (Reloc (G,((card F) -' 1))) ; ::_thesis: contradiction
then consider w being Element of NAT  such that
A15: x = w + ((card F) -' 1) and
 w in dom (IncAddr (G,((card F) -' 1))) by A13;
 m < (card F) - 1 by A12, VALUED_1:38;
then  m < (card F) -' 1 by PRE_CIRC:20;
hence  contradiction by A11, A15, NAT_1:11; ::_thesis: verum
end;
A16: x in dom (F ';' G) by A1, A10, XBOOLE_0:def_3;
now__::_thesis:_not_x_=_LastLoc_(F_';'_G)
assume  x = LastLoc (F ';' G) ; ::_thesis: contradiction
then A17: m = (card (F ';' G)) -' 1 by A11, AFINSQ_1:70
.= (card (F ';' G)) - 1 by PRE_CIRC:20 ;
 card (CutLastLoc (F ';' G)) = (card (F ';' G)) - 1 by VALUED_1:38;
hence  contradiction by A4, A12, A17; ::_thesis: verum
end;
then  not x in {(LastLoc (F ';' G))} by TARSKI:def_1;
then  not x in dom ((LastLoc (F ';' G)) .--> ((F ';' G) . (LastLoc (F ';' G)))) by FUNCOP_1:13;
then  x in (dom (F ';' G)) \ (dom ((LastLoc (F ';' G)) .--> ((F ';' G) . (LastLoc (F ';' G))))) by A16, XBOOLE_0:def_5;
hence (CutLastLoc (F ';' G)) . x = ((CutLastLoc F) +* (Reloc (G,((card F) -' 1)))) . x by GRFUNC_1:32
.= (CutLastLoc F) . x by A14, FUNCT_4:11 ;
::_thesis: verum
end;
hence  CutLastLoc F c= CutLastLoc (F ';' G) by A7, GRFUNC_1:2; ::_thesis: verum
end;

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
proof
let S be COM-Struct ; ::_thesis: for F, G being non empty initial preProgram of S holds (F ';' G) . (LastLoc F) = (IncAddr (G,((card F) -' 1))) . 0
let F, G be non empty initial preProgram of S; ::_thesis: (F ';' G) . (LastLoc F) = (IncAddr (G,((card F) -' 1))) . 0
set k = (card F) -' 1;
A1: LastLoc F = 0 + ((card F) -' 1) by AFINSQ_1:70;
A2: 0 in dom (IncAddr (G,((card F) -' 1))) by AFINSQ_1:65;
 dom (Reloc (G,((card F) -' 1))) =  {  (m + ((card F) -' 1)) where m is Element of NAT : m in dom (IncAddr (G,((card F) -' 1)))  }  by VALUED_1:def_12;
then  LastLoc F in dom (Reloc (G,((card F) -' 1))) by A1, A2;
hence (F ';' G) . (LastLoc F) = (Reloc (G,((card F) -' 1))) . (LastLoc F) by FUNCT_4:13
.= (IncAddr (G,((card F) -' 1))) . 0 by A1, A2, VALUED_1:def_12 ;
::_thesis: verum
end;

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
proof
let S be COM-Struct ; ::_thesis: 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
let F, G be non empty initial preProgram of S; ::_thesis: for f being Nat st f < (card F) - 1 holds
(IncAddr (F,((card F) -' 1))) . f = (IncAddr ((F ';' G),((card F) -' 1))) . f
let f be Nat; ::_thesis: ( f < (card F) - 1 implies (IncAddr (F,((card F) -' 1))) . f = (IncAddr ((F ';' G),((card F) -' 1))) . f )
set k = (card F) -' 1;
set P = F ';' G;
assume  f < (card F) - 1 ; ::_thesis: (IncAddr (F,((card F) -' 1))) . f = (IncAddr ((F ';' G),((card F) -' 1))) . f
then  f < card (CutLastLoc F) by VALUED_1:38;
then A1: f in dom (CutLastLoc F) by AFINSQ_1:66;
A2: dom (CutLastLoc F) c= dom F by GRFUNC_1:2;
 CutLastLoc F c= CutLastLoc (F ';' G) by Th22;
then  CutLastLoc F c= F ';' G by XBOOLE_1:1;
then A3: dom (CutLastLoc F) c= dom (F ';' G) by GRFUNC_1:2;
A4: F . f = F /. f by A1, A2, PARTFUN1:def_6;
 dom (CutLastLoc F) misses dom (Reloc (G,((card F) -' 1))) by Th18;
then  (dom (CutLastLoc F)) /\ (dom (Reloc (G,((card F) -' 1)))) = {} by XBOOLE_0:def_7;
then  not f in dom (Reloc (G,((card F) -' 1))) by A1, XBOOLE_0:def_4;
then A5: (F ';' G) . f = (CutLastLoc F) . f by FUNCT_4:11
.= F . f by A1, GRFUNC_1:2 ;
thus (IncAddr (F,((card F) -' 1))) . f = IncAddr ((F /. f),((card F) -' 1)) by A1, A2, Def21
.= IncAddr (((F ';' G) /. f),((card F) -' 1)) by A1, A3, A4, A5, PARTFUN1:def_6
.= (IncAddr ((F ';' G),((card F) -' 1))) . f by A1, A3, Def21 ; ::_thesis: verum
end;

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
proof
set P = F ';' G;
set k = (card F) -' 1;
A1: dom (Reloc (G,((card F) -' 1))) =  {  (m + ((card F) -' 1)) where m is Element of NAT : m in dom (IncAddr (G,((card F) -' 1)))  }  by VALUED_1:def_12;
A2: (card G) -' 1 = LastLoc G by AFINSQ_1:70;
then A3: (card G) -' 1 in dom G by VALUED_1:30;
then A4: (card G) -' 1 in dom (IncAddr (G,((card F) -' 1))) by Def21;
then A5: ((card F) -' 1) + ((card G) -' 1) in dom (Reloc (G,((card F) -' 1))) by A1;
A6: G /. ((card G) -' 1) = G . ((card G) -' 1) by A2, PARTFUN1:def_6, VALUED_1:30
.= halt S by A2, Def14 ;
A7: (card G) - 1 >= 0 by NAT_1:14, XREAL_1:48;
then  ((card F) -' 1) + ((card G) - 1) >= ((card F) -' 1) + 0 by XREAL_1:6;
then A8: (((card F) -' 1) + (card G)) -' 1 = (((card F) -' 1) + (card G)) - 1 by XREAL_0:def_2
.= ((card F) -' 1) + ((card G) - 1)
.= ((card F) -' 1) + ((card G) -' 1) by A7, XREAL_0:def_2 ;
thus (F ';' G) . (LastLoc (F ';' G)) = (F ';' G) . ((card (F ';' G)) -' 1) by AFINSQ_1:70
.= (F ';' G) . ((((card F) + (card G)) -' 1) -' 1) by Th20
.= (F ';' G) . ((((card F) -' 1) + (card G)) -' 1) by NAT_1:14, NAT_D:38
.= (Reloc (G,((card F) -' 1))) . (((card F) -' 1) + ((card G) -' 1)) by A5, A8, FUNCT_4:13
.= (IncAddr (G,((card F) -' 1))) . ((card G) -' 1) by A4, VALUED_1:def_12
.= IncAddr ((G /. ((card G) -' 1)),((card F) -' 1)) by A3, Def21
.= halt S by A6, COMPOS_0:4 ; :: according to COMPOS_1:def_14 ::_thesis: verum
end;
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
proof
set P = F ';' G;
set k = (card F) -' 1;
A1: dom (F ';' G) = (dom (CutLastLoc F)) \/ (dom (Reloc (G,((card F) -' 1)))) by FUNCT_4:def_1;
A2: dom (Reloc (G,((card F) -' 1))) =  {  (m + ((card F) -' 1)) where m is Element of NAT : m in dom (IncAddr (G,((card F) -' 1)))  }  by VALUED_1:def_12;
A3: (card G) - 1 >= 0 by NAT_1:14, XREAL_1:48;
then  ((card F) -' 1) + ((card G) - 1) >= ((card F) -' 1) + 0 by XREAL_1:6;
then A4: (((card F) -' 1) + (card G)) -' 1 = (((card F) -' 1) + (card G)) - 1 by XREAL_0:def_2
.= ((card F) -' 1) + ((card G) - 1)
.= ((card F) -' 1) + ((card G) -' 1) by A3, XREAL_0:def_2 ;
let f be Nat; :: according to COMPOS_1:def_15 ::_thesis: ( (F ';' G) . f = halt S & f in dom (F ';' G) implies f = LastLoc (F ';' G) )
assume that
A5: (F ';' G) . f = halt S and
A6: f in dom (F ';' G) ; ::_thesis: f = LastLoc (F ';' G)
percases ( f in dom (CutLastLoc F) or f in dom (Reloc (G,((card F) -' 1))) ) by A1, A6, XBOOLE_0:def_3;
supposeA7: f in dom (CutLastLoc F) ; ::_thesis: f = LastLoc (F ';' G)
then A8: (CutLastLoc F) . f <> halt S by Th19;
 dom (CutLastLoc F) misses dom (Reloc (G,((card F) -' 1))) by Th18;
then  CutLastLoc F c= F ';' G by FUNCT_4:32;
hence  f = LastLoc (F ';' G) by A5, A7, A8, GRFUNC_1:2; ::_thesis: verum
end;
supposeA9: f in dom (Reloc (G,((card F) -' 1))) ; ::_thesis: f = LastLoc (F ';' G)
then consider m being Element of NAT  such that
A10: f = m + ((card F) -' 1) and
A11: m in dom (IncAddr (G,((card F) -' 1))) by A2;
A12: m in dom G by A11, Def21;
then A13: G /. m = G . m by PARTFUN1:def_6;
IncAddr ((G /. m),((card F) -' 1)) = (IncAddr (G,((card F) -' 1))) . m by A12, Def21
.= (Reloc (G,((card F) -' 1))) . (m + ((card F) -' 1)) by A11, VALUED_1:def_12
.= halt S by A5, A9, A10, FUNCT_4:13 ;
then  G . m = halt S by A13, COMPOS_0:12;
then m = LastLoc G by A12, Def15
.= (card G) -' 1 by AFINSQ_1:70 ;
then m + ((card F) -' 1) = (((card F) + (card G)) -' 1) -' 1 by A4, NAT_1:14, NAT_D:38
.= (card (F ';' G)) -' 1 by Th20 ;
hence  f = LastLoc (F ';' G) by A10, AFINSQ_1:70; ::_thesis: verum
end;
end;
end;
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
proof
A1: dom (IncAddr ((Stop S),k)) = dom (Stop S) by Def21
.= {0} by Lm1 ;
A2: dom (Stop S) = {0} by Lm1;
 for x being set st x in {0} holds
(IncAddr ((Stop S),k)) . x = (Stop S) . x
proof
let x be set ; ::_thesis: ( x in {0} implies (IncAddr ((Stop S),k)) . x = (Stop S) . x )
assume A3: x in {0} ; ::_thesis: (IncAddr ((Stop S),k)) . x = (Stop S) . x
then A4: x = 0 by TARSKI:def_1;
then A5: (Stop S) /. 0 = (Stop S) . 0 by A2, A3, PARTFUN1:def_6
.= halt S by FUNCOP_1:72 ;
thus (IncAddr ((Stop S),k)) . x = IncAddr (((Stop S) /. 0),k) by A2, A3, A4, Def21
.= halt S by A5, COMPOS_0:4
.= (Stop S) . x by A4, FUNCOP_1:72 ; ::_thesis: verum
end;
hence  IncAddr ((Stop S),k) = Stop S by A1, A2, FUNCT_1:2; ::_thesis: verum
end;
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)
proof
let k be Nat; ::_thesis: for S being COM-Struct holds Shift ((Stop S),k) = k .--> (halt S)
let S be COM-Struct ; ::_thesis: Shift ((Stop S),k) = k .--> (halt S)
A1: dom (Shift ((Stop S),k)) =  {  (m + k) where m is Element of NAT : m in dom (Stop S)  }  by VALUED_1:def_12;
A2: 0 in dom (Stop S) by Lm1;
A3: dom (Shift ((Stop S),k)) = {k}
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {k} c= dom (Shift ((Stop S),k))
let x be set ; ::_thesis: ( x in dom (Shift ((Stop S),k)) implies x in {k} )
assume  x in dom (Shift ((Stop S),k)) ; ::_thesis: x in {k}
then consider m being Element of NAT  such that
A4: x = m + k and
A5: m in dom (Stop S) by A1;
 m in {0} by A5, Lm1;
then  m = 0 by TARSKI:def_1;
hence  x in {k} by A4, TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {k} or x in dom (Shift ((Stop S),k)) )
assume  x in {k} ; ::_thesis: x in dom (Shift ((Stop S),k))
then  x = 0 + k by TARSKI:def_1;
hence  x in dom (Shift ((Stop S),k)) by A1, A2; ::_thesis: verum
end;
A6: dom (k .--> (halt S)) = {k} by FUNCOP_1:13;
 for x being set st x in {k} holds
(Shift ((Stop S),k)) . x = (k .--> (halt S)) . x
proof
let x be set ; ::_thesis: ( x in {k} implies (Shift ((Stop S),k)) . x = (k .--> (halt S)) . x )
assume  x in {k} ; ::_thesis: (Shift ((Stop S),k)) . x = (k .--> (halt S)) . x
then A7: x = 0 + k by TARSKI:def_1;
 0 in dom (Stop S) by Lm1;
hence (Shift ((Stop S),k)) . x = (Stop S) . 0 by A7, VALUED_1:def_12
.= halt S by FUNCOP_1:72
.= (k .--> (halt S)) . x by A7, FUNCOP_1:72 ;
::_thesis: verum
end;
hence  Shift ((Stop S),k) = k .--> (halt S) by A3, A6, FUNCT_1:2; ::_thesis: verum
end;

registration
let S be COM-Struct ;
let F be MacroInstruction of S;
reduceF ';' (Stop S) to F;
reducibility
 F ';' (Stop S) = F
proof
set k = (card F) -' 1;
A1: dom F = (dom (CutLastLoc F)) \/ {(LastLoc F)} by VALUED_1:37;
dom (Shift ((Stop S),((card F) -' 1))) = dom (((card F) -' 1) .--> (halt S)) by Th26
.= {((card F) -' 1)} by FUNCOP_1:13
.= {(LastLoc F)} by AFINSQ_1:70 ;
then A2: dom (F ';' (Stop S)) = dom F by A1, FUNCT_4:def_1;
 for x being set st x in dom F holds
(F ';' (Stop S)) . x = F . x
proof
let x be set ; ::_thesis: ( x in dom F implies (F ';' (Stop S)) . x = F . x )
assume A3: x in dom F ; ::_thesis: (F ';' (Stop S)) . x = F . x
 dom (CutLastLoc F) misses dom (Reloc ((Stop S),((card F) -' 1))) by Th18;
then A4: {} = (dom (CutLastLoc F)) /\ (dom (Reloc ((Stop S),((card F) -' 1)))) by XBOOLE_0:def_7;
percases ( x in dom (CutLastLoc F) or x in {(LastLoc F)} ) by A1, A3, XBOOLE_0:def_3;
supposeA5: x in dom (CutLastLoc F) ; ::_thesis: (F ';' (Stop S)) . x = F . x
then  not x in dom (Reloc ((Stop S),((card F) -' 1))) by A4, XBOOLE_0:def_4;
hence (F ';' (Stop S)) . x = (CutLastLoc F) . x by FUNCT_4:11
.= F . x by A5, GRFUNC_1:2 ;
::_thesis: verum
end;
suppose x in {(LastLoc F)} ; ::_thesis: (F ';' (Stop S)) . x = F . x
then A6: x = LastLoc F by TARSKI:def_1;
then A7: x = (card F) -' 1 by AFINSQ_1:70;
A8: 0 in dom (Stop S) by Lm1;
 dom (Shift ((Stop S),((card F) -' 1))) =  {  (m + ((card F) -' 1)) where m is Element of NAT : m in dom (Stop S)  }  by VALUED_1:def_12;
then  0 + ((card F) -' 1) in dom (Shift ((Stop S),((card F) -' 1))) by A8;
hence (F ';' (Stop S)) . x = (Shift ((Stop S),(0 + ((card F) -' 1)))) . x by A7, FUNCT_4:13
.= (Stop S) . 0 by A7, A8, VALUED_1:def_12
.= halt S by FUNCOP_1:72
.= F . x by A6, Def14 ;
::_thesis: verum
end;
end;
end;
hence  F ';' (Stop S) = F by A2, FUNCT_1:2; ::_thesis: verum
end;
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
proof
 (card (Stop S)) -' 1 = 0 by Lm2;
hence (Stop S) ';' F = {} +* (Reloc (F,0))
.= Reloc (F,0)
.= F ;
::_thesis: verum
end;
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)
proof
let S be COM-Struct ; ::_thesis: for F, G, H being MacroInstruction of S holds (F ';' G) ';' H = F ';' (G ';' H)
let F, G, H be MacroInstruction of S; ::_thesis: (F ';' G) ';' H = F ';' (G ';' H)
percases ( F = Stop S or G = Stop S or ( F <> Stop S & G <> Stop S ) ) ;
supposeA1: F = Stop S ; ::_thesis: (F ';' G) ';' H = F ';' (G ';' H)
hence (F ';' G) ';' H = ((Stop S) ';' G) ';' H
.= F ';' (G ';' H) by A1, Th28 ;
::_thesis: verum
end;
supposeA2: G = Stop S ; ::_thesis: (F ';' G) ';' H = F ';' (G ';' H)
hence (F ';' G) ';' H = (F ';' (Stop S)) ';' H
.= F ';' (G ';' H) by A2, Th28 ;
::_thesis: verum
end;
supposethat A3: F <> Stop S and
A4: G <> Stop S ; ::_thesis: (F ';' G) ';' H = F ';' (G ';' H)
set X =  {  k where k is Element of NAT : k < ((((card F) + (card G)) + (card H)) - 1) - 1  }  ;
A5: card ((F ';' G) ';' H) = ((card (F ';' G)) + (card H)) - 1 by Th20
.= ((((card F) + (card G)) - 1) + (card H)) - 1 by Th20
.= ((((card F) + (card G)) + (card H)) - 1) - 1 ;
A6: card (F ';' (G ';' H)) = ((card F) + (card (G ';' H))) - 1 by Th20
.= ((card F) + (((card G) + (card H)) - 1)) - 1 by Th20
.= ((((card F) + (card G)) + (card H)) - 1) - 1 ;
A7: dom ((F ';' G) ';' H) =  {  k where k is Element of NAT : k < ((((card F) + (card G)) + (card H)) - 1) - 1  }  by A5, AFINSQ_1:68;
A8: dom (F ';' (G ';' H)) =  {  k where k is Element of NAT : k < ((((card F) + (card G)) + (card H)) - 1) - 1  }  by A6, AFINSQ_1:68;
 for x being set st x in  {  k where k is Element of NAT : k < ((((card F) + (card G)) + (card H)) - 1) - 1  }  holds
((F ';' G) ';' H) . x = (F ';' (G ';' H)) . x
proof
let x be set ; ::_thesis: ( x in  {  k where k is Element of NAT : k < ((((card F) + (card G)) + (card H)) - 1) - 1  }  implies ((F ';' G) ';' H) . x = (F ';' (G ';' H)) . x )
assume  x in  {  k where k is Element of NAT : k < ((((card F) + (card G)) + (card H)) - 1) - 1  }  ; ::_thesis: ((F ';' G) ';' H) . x = (F ';' (G ';' H)) . x
then consider k being Element of NAT  such that
A9: x = k and
A10: k < ((((card F) + (card G)) + (card H)) - 1) - 1 ;
A11: dom (Reloc ((G ';' H),((card F) -' 1))) =  {  (m + ((card F) -' 1)) where m is Element of NAT : m in dom (IncAddr ((G ';' H),((card F) -' 1)))  }  by VALUED_1:def_12;
A12: dom (Reloc (H,((card (F ';' G)) -' 1))) =  {  (m + ((card (F ';' G)) -' 1)) where m is Element of NAT : m in dom (IncAddr (H,((card (F ';' G)) -' 1)))  }  by VALUED_1:def_12;
A13: dom (Reloc (H,((card G) -' 1))) =  {  (m + ((card G) -' 1)) where m is Element of NAT : m in dom (IncAddr (H,((card G) -' 1)))  }  by VALUED_1:def_12;
A14: (card (F ';' G)) -' 1 = (card (F ';' G)) - 1 by PRE_CIRC:20
.= (((card F) + (card G)) - 1) - 1 by Th20 ;
then  (card (F ';' G)) -' 1 = ((card F) - 1) + ((card G) - 1) ;
then A15: (card (F ';' G)) -' 1 = ((card G) -' 1) + ((card F) - 1) by PRE_CIRC:20
.= ((card G) -' 1) + ((card F) -' 1) by PRE_CIRC:20 ;
A16: dom (Reloc (G,((card F) -' 1))) =  {  (m + ((card F) -' 1)) where m is Element of NAT : m in dom (IncAddr (G,((card F) -' 1)))  }  by VALUED_1:def_12;
A17: (card F) -' 1 = (card F) - 1 by PRE_CIRC:20;
A18: (card G) -' 1 = (card G) - 1 by PRE_CIRC:20;
A19: for W being MacroInstruction of S st W <> Stop S holds
2 <= card W
proof
let W be MacroInstruction of S; ::_thesis: ( W <> Stop S implies 2 <= card W )
assume A20: W <> Stop S ; ::_thesis: 2 <= card W
assume  2 > card W ; ::_thesis: contradiction
then  1 + 1 > card W ;
then  card W <= 1 by NAT_1:13;
hence  contradiction by A20, Th8, NAT_1:25; ::_thesis: verum
end;
then  2 <= card F by A3;
then A21: 1 <= card F by XXREAL_0:2;
A22: 2 <= card G by A4, A19;
percases ( k < (card F) - 1 or k = (card F) - 1 or ( card F <= k & k <= ((card F) + (card G)) - 3 ) or k = ((card F) + (card G)) - 2 or ((card F) + (card G)) - 2 < k ) by A21, A22, Lm5;
supposeA23: k < (card F) - 1 ; ::_thesis: ((F ';' G) ';' H) . x = (F ';' (G ';' H)) . x
A24: CutLastLoc F c= CutLastLoc (F ';' G) by Th22;
A25: now__::_thesis:_not_x_in_dom_(Reloc_((G_';'_H),((card_F)_-'_1)))
assume  x in dom (Reloc ((G ';' H),((card F) -' 1))) ; ::_thesis: contradiction
then consider m being Element of NAT  such that
A26: x = m + ((card F) -' 1) and
 m in dom (IncAddr ((G ';' H),((card F) -' 1))) by A11;
 k = m + ((card F) - 1) by A9, A26, PRE_CIRC:20;
then  m + ((card F) - 1) < (card F) -' 1 by A23, PRE_CIRC:20;
then  m + ((card F) -' 1) < (card F) -' 1 by PRE_CIRC:20;
hence  contradiction by NAT_1:11; ::_thesis: verum
end;
A27: now__::_thesis:_not_x_in_dom_(Reloc_(H,((card_(F_';'_G))_-'_1)))
assume  x in dom (Reloc (H,((card (F ';' G)) -' 1))) ; ::_thesis: contradiction
then consider m being Element of NAT  such that
A28: x = m + ((card (F ';' G)) -' 1) and
 m in dom (IncAddr (H,((card (F ';' G)) -' 1))) by A12;
 (m + ((card G) -' 1)) + ((card F) -' 1) < (card F) -' 1 by A23, A9, A15, A28, PRE_CIRC:20;
hence  contradiction by NAT_1:11; ::_thesis: verum
end;
 k < card (CutLastLoc F) by A23, VALUED_1:38;
then A29: x in dom (CutLastLoc F) by A9, AFINSQ_1:66;
thus ((F ';' G) ';' H) . x = (CutLastLoc (F ';' G)) . x by A27, FUNCT_4:11
.= (CutLastLoc F) . x by A24, A29, GRFUNC_1:2
.= (F ';' (G ';' H)) . x by A25, FUNCT_4:11 ; ::_thesis: verum
end;
supposeA30: k = (card F) - 1 ; ::_thesis: ((F ';' G) ';' H) . x = (F ';' (G ';' H)) . x
A31: now__::_thesis:_not_x_in_dom_(Reloc_(H,((card_(F_';'_G))_-'_1)))
assume  x in dom (Reloc (H,((card (F ';' G)) -' 1))) ; ::_thesis: contradiction
then consider m being Element of NAT  such that
A32: x = m + ((card (F ';' G)) -' 1) and
 m in dom (IncAddr (H,((card (F ';' G)) -' 1))) by A12;
 (m + ((card G) -' 1)) + ((card F) -' 1) = (card F) -' 1 by A30, A15, A32, A9, PRE_CIRC:20;
then  (card G) -' 1 = 0 ;
then  (card G) - 1 = 0 by PRE_CIRC:20;
hence  contradiction by A4, Th8; ::_thesis: verum
end;
A33: 0 in dom (IncAddr ((G ';' H),((card F) -' 1))) by AFINSQ_1:65;
A34: 0 in dom (IncAddr (G,((card F) -' 1))) by AFINSQ_1:65;
A35: 0 in dom G by AFINSQ_1:65;
A36: 0 in dom (G ';' H) by AFINSQ_1:65;
 k = 0 + ((card F) -' 1) by A30, PRE_CIRC:20;
then A37: x in dom (Reloc ((G ';' H),((card F) -' 1))) by A9, A11, A33;
A38: k = (card F) -' 1 by A30, PRE_CIRC:20;
A39: x = 0 + k by A9;
 0 in dom (IncAddr (G,((card F) -' 1))) by AFINSQ_1:65;
then A40: x in dom (Reloc (G,((card F) -' 1))) by A16, A38, A39;
then  x in (dom (CutLastLoc F)) \/ (dom (Reloc (G,((card F) -' 1)))) by XBOOLE_0:def_3;
then A41: x in dom (F ';' G) by FUNCT_4:def_1;
now__::_thesis:_not_x_in_dom_((LastLoc_(F_';'_G))_.-->_((F_';'_G)_._(LastLoc_(F_';'_G))))
A42: dom ((LastLoc (F ';' G)) .--> ((F ';' G) . (LastLoc (F ';' G)))) = {(LastLoc (F ';' G))} by FUNCOP_1:13
.= {((card (F ';' G)) -' 1)} by AFINSQ_1:70 ;
assume  x in dom ((LastLoc (F ';' G)) .--> ((F ';' G) . (LastLoc (F ';' G)))) ; ::_thesis: contradiction
then  x = (card (F ';' G)) -' 1 by A42, TARSKI:def_1;
then  (card G) - 1 = 0 by A38, A9, A15, PRE_CIRC:20;
hence  contradiction by A4, Th8; ::_thesis: verum
end;
then A43: x in (dom (F ';' G)) \ (dom ((LastLoc (F ';' G)) .--> ((F ';' G) . (LastLoc (F ';' G))))) by A41, XBOOLE_0:def_5;
 1 <= card G by NAT_1:14;
then  card G > 1 by A4, Th8, XXREAL_0:1;
then A44: (card G) - 1 > 1 - 1 by XREAL_1:9;
then  (card G) -' 1 > 1 - 1 by PRE_CIRC:20;
then A45: not 0 in dom (Reloc (H,((card G) -' 1))) by VALUED_1:29;
 card (CutLastLoc G) <> {} by A44, VALUED_1:38;
then A46: 0 in dom (CutLastLoc G) by AFINSQ_1:65, CARD_1:27;
A47: G /. 0 = G . 0 by A35, PARTFUN1:def_6
.= (CutLastLoc G) . 0 by A46, GRFUNC_1:2
.= (G ';' H) . 0 by A45, FUNCT_4:11
.= (G ';' H) /. 0 by A36, PARTFUN1:def_6 ;
thus ((F ';' G) ';' H) . x = ((F ';' G) \ ((LastLoc (F ';' G)) .--> ((F ';' G) . (LastLoc (F ';' G))))) . x by A31, FUNCT_4:11
.= ((CutLastLoc F) +* (Reloc (G,((card F) -' 1)))) . x by A43, GRFUNC_1:32
.= (Reloc (G,((card F) -' 1))) . x by A40, FUNCT_4:13
.= (IncAddr (G,((card F) -' 1))) . 0 by A34, A38, A39, VALUED_1:def_12
.= IncAddr (((G ';' H) /. 0),((card F) -' 1)) by A35, A47, Def21
.= (IncAddr ((G ';' H),((card F) -' 1))) . 0 by A36, Def21
.= (Reloc ((G ';' H),((card F) -' 1))) . x by A33, A38, A39, VALUED_1:def_12
.= (F ';' (G ';' H)) . x by A37, FUNCT_4:13 ; ::_thesis: verum
end;
supposethat A48: card F <= k and
A49: k <= ((card F) + (card G)) - 3 ; ::_thesis: ((F ';' G) ';' H) . x = (F ';' (G ';' H)) . x
A50: now__::_thesis:_not_x_in_dom_(Reloc_(H,((card_(F_';'_G))_-'_1)))
assume  x in dom (Reloc (H,((card (F ';' G)) -' 1))) ; ::_thesis: contradiction
then consider m being Element of NAT  such that
A51: x = m + ((card (F ';' G)) -' 1) and
 m in dom (IncAddr (H,((card (F ';' G)) -' 1))) by A12;
 m + (((card G) -' 1) + ((card F) -' 1)) <= (- 1) + (((card G) -' 1) + ((card F) -' 1)) by A9, A15, A17, A18, A49, A51;
hence  contradiction by XREAL_1:6; ::_thesis: verum
end;
 (card F) -' 1 <= card F by NAT_D:35;
then A52: x = (k -' ((card F) -' 1)) + ((card F) -' 1) by A9, A48, XREAL_1:235, XXREAL_0:2;
A53: (card F) - (card F) <= k - (card F) by A48, XREAL_1:9;
 (card F) - 1 < (card F) - 0 by XREAL_1:15;
then  k - ((card F) - 1) >= 0 by A53, XREAL_1:15;
then A54: k - ((card F) -' 1) >= 0 by PRE_CIRC:20;
A55: ((card F) + (card G)) - 3 < (((card F) + (card G)) - 3) + 1 by XREAL_1:29;
then A56: k < ((card G) - 1) + ((card F) - 1) by A49, XXREAL_0:2;
 (k - ((card F) - 1)) + ((card F) - 1) < ((card G) - 1) + ((card F) - 1) by A49, A55, XXREAL_0:2;
then  k - ((card F) - 1) < (card G) - 1 by XREAL_1:7;
then  k - ((card F) -' 1) < (card G) - 1 by PRE_CIRC:20;
then  k -' ((card F) -' 1) < (card G) - 1 by A54, XREAL_0:def_2;
then  k -' ((card F) -' 1) < card (CutLastLoc G) by VALUED_1:38;
then A57: k -' ((card F) -' 1) in dom (CutLastLoc G) by AFINSQ_1:66;
then  k -' ((card F) -' 1) in (dom (CutLastLoc G)) \/ (dom (Reloc (H,((card G) -' 1)))) by XBOOLE_0:def_3;
then A58: k -' ((card F) -' 1) in dom (G ';' H) by FUNCT_4:def_1;
then A59: k -' ((card F) -' 1) in dom (IncAddr ((G ';' H),((card F) -' 1))) by Def21;
then A60: x in dom (Reloc ((G ';' H),((card F) -' 1))) by A11, A52;
 ((card G) + (card F)) - 2 < ((card F) + (card G)) - 1 by XREAL_1:15;
then  k < ((card F) + (card G)) - 1 by A56, XXREAL_0:2;
then  k < card (F ';' G) by Th20;
then A61: x in dom (F ';' G) by A9, AFINSQ_1:66;
now__::_thesis:_not_x_in_dom_((LastLoc_(F_';'_G))_.-->_((F_';'_G)_._(LastLoc_(F_';'_G))))
assume  x in dom ((LastLoc (F ';' G)) .--> ((F ';' G) . (LastLoc (F ';' G)))) ; ::_thesis: contradiction
then  x in {(LastLoc (F ';' G))} by FUNCOP_1:13;
then x = LastLoc (F ';' G) by TARSKI:def_1
.= (card (F ';' G)) -' 1 by AFINSQ_1:70 ;
then  k = ((card G) - 1) + ((card F) - 1) by A9, A15, A18, PRE_CIRC:20;
hence  contradiction by A49, A55; ::_thesis: verum
end;
then A62: x in (dom (F ';' G)) \ (dom ((LastLoc (F ';' G)) .--> ((F ';' G) . (LastLoc (F ';' G))))) by A61, XBOOLE_0:def_5;
A63: dom (CutLastLoc G) c= dom G by GRFUNC_1:2;
then  k -' ((card F) -' 1) in dom G by A57;
then A64: k -' ((card F) -' 1) in dom (IncAddr (G,((card F) -' 1))) by Def21;
then A65: x in dom (Reloc (G,((card F) -' 1))) by A16, A52;
A66: now__::_thesis:_not_k_-'_((card_F)_-'_1)_in_dom_(Reloc_(H,((card_G)_-'_1)))
assume  k -' ((card F) -' 1) in dom (Reloc (H,((card G) -' 1))) ; ::_thesis: contradiction
then consider m being Element of NAT  such that
A67: k -' ((card F) -' 1) = m + ((card G) -' 1) and
 m in dom (IncAddr (H,((card G) -' 1))) by A13;
A68: m = (k -' ((card F) -' 1)) - ((card G) -' 1) by A67
.= (k - ((card F) -' 1)) - ((card G) -' 1) by A54, XREAL_0:def_2
.= (k - ((card F) - 1)) - ((card G) -' 1) by PRE_CIRC:20
.= (k - ((card F) - 1)) - ((card G) - 1) by PRE_CIRC:20
.= k - (((card F) + (card G)) - 2) ;
 k - (((card F) + (card G)) - 2) <= (((card F) + (card G)) - 3) - (((card F) + (card G)) - 2) by A49, XREAL_1:9;
hence  contradiction by A68, Lm4; ::_thesis: verum
end;
A69: (G ';' H) /. (k -' ((card F) -' 1)) = ((CutLastLoc G) +* (Reloc (H,((card G) -' 1)))) . (k -' ((card F) -' 1)) by A58, PARTFUN1:def_6
.= (CutLastLoc G) . (k -' ((card F) -' 1)) by A66, FUNCT_4:11
.= G . (k -' ((card F) -' 1)) by A57, GRFUNC_1:2 ;
thus ((F ';' G) ';' H) . x = ((F ';' G) \ ((LastLoc (F ';' G)) .--> ((F ';' G) . (LastLoc (F ';' G))))) . x by A50, FUNCT_4:11
.= ((CutLastLoc F) +* (Reloc (G,((card F) -' 1)))) . x by A62, GRFUNC_1:32
.= (Reloc (G,((card F) -' 1))) . x by A65, FUNCT_4:13
.= (IncAddr (G,((card F) -' 1))) . (k -' ((card F) -' 1)) by A52, A64, VALUED_1:def_12
.= IncAddr ((G /. (k -' ((card F) -' 1))),((card F) -' 1)) by A57, A63, Def21
.= IncAddr (((G ';' H) /. (k -' ((card F) -' 1))),((card F) -' 1)) by A57, A63, A69, PARTFUN1:def_6
.= (IncAddr ((G ';' H),((card F) -' 1))) . (k -' ((card F) -' 1)) by A58, Def21
.= (Reloc ((G ';' H),((card F) -' 1))) . x by A52, A59, VALUED_1:def_12
.= (F ';' (G ';' H)) . x by A60, FUNCT_4:13 ; ::_thesis: verum
end;
supposeA70: k = ((card F) + (card G)) - 2 ; ::_thesis: ((F ';' G) ';' H) . x = (F ';' (G ';' H)) . x
then A71: x = (k -' ((card (F ';' G)) -' 1)) + ((card (F ';' G)) -' 1) by A9, A14, XREAL_1:235;
 k - ((card (F ';' G)) -' 1) = 0 by A14, A70;
then A72: k -' ((card (F ';' G)) -' 1) = 0 by XREAL_0:def_2;
then A73: k -' ((card (F ';' G)) -' 1) in dom (IncAddr (H,((card (F ';' G)) -' 1))) by AFINSQ_1:65;
then A74: x in dom (Reloc (H,((card (F ';' G)) -' 1))) by A12, A71;
A75: x = ((card G) -' 1) + ((card F) -' 1) by A9, A17, A18, A70;
 ((card G) - 1) + 0 < ((card G) - 1) + (card H) by XREAL_1:6;
then  (card G) -' 1 < ((card G) + (card H)) - 1 by PRE_CIRC:20;
then  (card G) -' 1 < card (G ';' H) by Th20;
then A76: (card G) -' 1 in dom (G ';' H) by AFINSQ_1:66;
then A77: (card G) -' 1 in dom (IncAddr ((G ';' H),((card F) -' 1))) by Def21;
then A78: x in dom (Reloc ((G ';' H),((card F) -' 1))) by A11, A75;
A79: 0 in dom H by AFINSQ_1:65;
A80: (G ';' H) /. ((card G) -' 1) = (G ';' H) . ((card G) -' 1) by A76, PARTFUN1:def_6;
A81: 0 in dom (IncAddr (H,((card G) -' 1))) by AFINSQ_1:65;
then A82: (IncAddr (H,((card G) -' 1))) /. 0 = (IncAddr (H,((card G) -' 1))) . 0 by PARTFUN1:def_6
.= IncAddr ((H /. 0),((card G) -' 1)) by A79, Def21 ;
(G ';' H) /. ((card G) -' 1) = (G ';' H) . (LastLoc G) by A80, AFINSQ_1:70
.= (IncAddr (H,((card G) -' 1))) . 0 by Th23
.= (IncAddr (H,((card G) -' 1))) /. 0 by A81, PARTFUN1:def_6 ;
then A83: IncAddr (((G ';' H) /. ((card G) -' 1)),((card F) -' 1)) = IncAddr ((H /. 0),((card (F ';' G)) -' 1)) by A15, A82, COMPOS_0:7;
thus ((F ';' G) ';' H) . x = (Reloc (H,((card (F ';' G)) -' 1))) . x by A74, FUNCT_4:13
.= (IncAddr (H,((card (F ';' G)) -' 1))) . (k -' ((card (F ';' G)) -' 1)) by A71, A73, VALUED_1:def_12
.= IncAddr ((H /. 0),((card (F ';' G)) -' 1)) by A72, A79, Def21
.= (IncAddr ((G ';' H),((card F) -' 1))) . ((card G) -' 1) by A76, A83, Def21
.= (Reloc ((G ';' H),((card F) -' 1))) . x by A75, A77, VALUED_1:def_12
.= (F ';' (G ';' H)) . x by A78, FUNCT_4:13 ; ::_thesis: verum
end;
supposeA84: ((card F) + (card G)) - 2 < k ; ::_thesis: ((F ';' G) ';' H) . x = (F ';' (G ';' H)) . x
then A85: x = (k -' ((card (F ';' G)) -' 1)) + ((card (F ';' G)) -' 1) by A9, A14, XREAL_1:235;
 k + 0 < (((card F) + (card G)) - (1 + 1)) + (card H) by A10;
then  k - (((card F) + (card G)) - (1 + 1)) < (card H) - 0 by XREAL_1:21;
then  k -' ((card (F ';' G)) -' 1) < card H by A14, XREAL_0:def_2;
then A86: k -' ((card (F ';' G)) -' 1) in dom H by AFINSQ_1:66;
then A87: k -' ((card (F ';' G)) -' 1) in dom (IncAddr (H,((card (F ';' G)) -' 1))) by Def21;
then A88: x in dom (Reloc (H,((card (F ';' G)) -' 1))) by A12, A85;
A89: (card F) -' 1 <= ((card G) -' 1) + ((card F) -' 1) by NAT_1:11;
then A90: k >= (card F) -' 1 by A14, A15, A84, XXREAL_0:2;
A91: x = (k -' ((card F) -' 1)) + ((card F) -' 1) by A9, A14, A15, A84, A89, XREAL_1:235, XXREAL_0:2;
A92: k - ((card F) -' 1) >= 0 by A90, XREAL_1:48;
A93: k - ((card F) -' 1) < (((((card F) + (card G)) + (card H)) - 1) - 1) - ((card F) -' 1) by A10, XREAL_1:9;
then A94: k -' ((card F) -' 1) < ((((card F) + (card G)) + (card H)) - (card F)) - 1 by A17, A92, XREAL_0:def_2;
 k -' ((card F) -' 1) < ((((card F) - (card F)) + (card G)) + (card H)) - 1 by A17, A92, A93, XREAL_0:def_2;
then  k -' ((card F) -' 1) < card (G ';' H) by Th20;
then A95: k -' ((card F) -' 1) in dom (G ';' H) by AFINSQ_1:66;
then  k -' ((card F) -' 1) in dom (IncAddr ((G ';' H),((card F) -' 1))) by Def21;
then A96: x in dom (Reloc ((G ';' H),((card F) -' 1))) by A11, A91;
A97: k -' ((card F) -' 1) in dom (IncAddr ((G ';' H),((card F) -' 1))) by A95, Def21;
A98: k - ((card F) -' 1) >= ((card (F ';' G)) -' 1) - ((card F) -' 1) by A14, A84, XREAL_1:9;
then A99: k -' ((card F) -' 1) >= (((card F) -' 1) + ((card G) -' 1)) - ((card F) -' 1) by A14, A15, A84, A89, XREAL_1:233, XXREAL_0:2;
A100: k -' ((card F) -' 1) >= (card G) -' 1 by A14, A15, A84, A89, A98, XREAL_1:233, XXREAL_0:2;
A101: k -' ((card F) -' 1) = ((k -' ((card F) -' 1)) -' ((card G) -' 1)) + ((card G) -' 1) by A99, XREAL_1:235;
 (k -' ((card F) -' 1)) - ((card G) -' 1) < (((card G) + (card H)) - 1) - ((card G) - 1) by A18, A94, XREAL_1:9;
then  (k -' ((card F) -' 1)) -' ((card G) -' 1) < ((card H) + ((card G) - 1)) - ((card G) - 1) by A100, XREAL_1:233;
then  (k -' ((card F) -' 1)) -' ((card G) -' 1) in dom H by AFINSQ_1:66;
then A102: (k -' ((card F) -' 1)) -' ((card G) -' 1) in dom (IncAddr (H,((card G) -' 1))) by Def21;
then A103: k -' ((card F) -' 1) in dom (Reloc (H,((card G) -' 1))) by A13, A101;
A104: (k -' ((card F) -' 1)) -' ((card G) -' 1) = (k -' ((card F) -' 1)) - ((card G) -' 1) by A99, XREAL_1:233
.= (k - ((card F) -' 1)) - ((card G) -' 1) by A14, A15, A84, A89, XREAL_1:233, XXREAL_0:2
.= k - (((card F) -' 1) + ((card G) -' 1))
.= k -' ((card (F ';' G)) -' 1) by A14, A15, A84, XREAL_1:233 ;
A105: (G ';' H) /. (k -' ((card F) -' 1)) = ((CutLastLoc G) +* (Reloc (H,((card G) -' 1)))) . (k -' ((card F) -' 1)) by A95, PARTFUN1:def_6
.= (Reloc (H,((card G) -' 1))) . (k -' ((card F) -' 1)) by A103, FUNCT_4:13
.= (IncAddr (H,((card G) -' 1))) . (k -' ((card (F ';' G)) -' 1)) by A101, A102, A104, VALUED_1:def_12
.= IncAddr ((H /. (k -' ((card (F ';' G)) -' 1))),((card G) -' 1)) by A86, Def21 ;
thus ((F ';' G) ';' H) . x = (Reloc (H,((card (F ';' G)) -' 1))) . x by A88, FUNCT_4:13
.= (IncAddr (H,((card (F ';' G)) -' 1))) . (k -' ((card (F ';' G)) -' 1)) by A85, A87, VALUED_1:def_12
.= IncAddr ((H /. (k -' ((card (F ';' G)) -' 1))),((card (F ';' G)) -' 1)) by A86, Def21
.= IncAddr (((G ';' H) /. (k -' ((card F) -' 1))),((card F) -' 1)) by A15, A105, COMPOS_0:7
.= (IncAddr ((G ';' H),((card F) -' 1))) . (k -' ((card F) -' 1)) by A95, Def21
.= (Reloc ((G ';' H),((card F) -' 1))) . x by A91, A97, VALUED_1:def_12
.= (F ';' (G ';' H)) . x by A96, FUNCT_4:13 ; ::_thesis: verum
end;
end;
end;
hence  (F ';' G) ';' H = F ';' (G ';' H) by A7, A8, FUNCT_1:2; ::_thesis: verum
end;
end;
end;

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))
proof
let S be COM-Struct ; ::_thesis: for k being Nat
for p being NAT -defined the InstructionsF of S -valued finite Function holds dom (Reloc (p,k)) = dom (Shift (p,k))
let k be Nat; ::_thesis: for p being NAT -defined the InstructionsF of S -valued finite Function holds dom (Reloc (p,k)) = dom (Shift (p,k))
let p be NAT -defined the InstructionsF of S -valued finite Function; ::_thesis: dom (Reloc (p,k)) = dom (Shift (p,k))
A1: dom (IncAddr (p,k)) = dom p by Def21;
thus  dom (Reloc (p,k)) =  {  (m + k) where m is Element of NAT : m in dom p  }  by A1, VALUED_1:def_12
.= dom (Shift (p,k)) by VALUED_1:def_12 ; ::_thesis: verum
end;

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  }
proof
let S be COM-Struct ; ::_thesis: for k being Nat
for p being NAT -defined the InstructionsF of S -valued finite Function holds dom (Reloc (p,k)) =  {  (j + k) where j is Element of NAT : j in dom p  }
let k be Nat; ::_thesis: for p being NAT -defined the InstructionsF of S -valued finite Function holds dom (Reloc (p,k)) =  {  (j + k) where j is Element of NAT : j in dom p  }
let p be NAT -defined the InstructionsF of S -valued finite Function; ::_thesis: dom (Reloc (p,k)) =  {  (j + k) where j is Element of NAT : j in dom p  }
thus  dom (Reloc (p,k)) = dom (Shift (p,k)) by Th32
.=  {  (j + k) where j is Element of NAT : j in dom p  }  by VALUED_1:def_12 ; ::_thesis: verum
end;

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)
proof
let S be COM-Struct ; ::_thesis: for i, j being Nat
for p being NAT -defined the InstructionsF of S -valued finite Function holds Shift ((IncAddr (p,i)),j) = IncAddr ((Shift (p,j)),i)
let i, j be Nat; ::_thesis: for p being NAT -defined the InstructionsF of S -valued finite Function holds Shift ((IncAddr (p,i)),j) = IncAddr ((Shift (p,j)),i)
let p be NAT -defined the InstructionsF of S -valued finite Function; ::_thesis: Shift ((IncAddr (p,i)),j) = IncAddr ((Shift (p,j)),i)
set f = Shift ((IncAddr (p,i)),j);
set g = IncAddr ((Shift (p,j)),i);
 dom (IncAddr (p,i)) = dom p by Def21;
then  dom (Shift (p,j)) =  {  (m + j) where m is Element of NAT : m in dom (IncAddr (p,i))  }  by VALUED_1:def_12
.= dom (Shift ((IncAddr (p,i)),j)) by VALUED_1:def_12 ;
then A1: dom (Shift ((IncAddr (p,i)),j)) = dom (IncAddr ((Shift (p,j)),i)) by Def21;
now__::_thesis:_for_x_being_set_st_x_in_dom_(Shift_((IncAddr_(p,i)),j))_holds_
(Shift_((IncAddr_(p,i)),j))_._x_=_(IncAddr_((Shift_(p,j)),i))_._x
let x be set ; ::_thesis: ( x in dom (Shift ((IncAddr (p,i)),j)) implies (Shift ((IncAddr (p,i)),j)) . x = (IncAddr ((Shift (p,j)),i)) . x )
A2: dom (Shift ((IncAddr (p,i)),j)) c= NAT by RELAT_1:def_18;
assume A3: x in dom (Shift ((IncAddr (p,i)),j)) ; ::_thesis: (Shift ((IncAddr (p,i)),j)) . x = (IncAddr ((Shift (p,j)),i)) . x
then reconsider x9 = x as Element of NAT by A2;
reconsider xx = x9 as Element of NAT ;
 x in  {  (m + j) where m is Element of NAT : m in dom (IncAddr (p,i))  }  by A3, VALUED_1:def_12;
then consider m being Element of NAT  such that
A4: x = m + j and
A5: m in dom (IncAddr (p,i)) ;
A6: m in dom p by A5, Def21;
 dom (Shift (p,j)) =  {  (mm + j) where mm is Element of NAT : mm in dom p  }  by VALUED_1:def_12;
then A7: x9 in dom (Shift (p,j)) by A4, A6;
reconsider mm = m as Element of NAT ;
A8: p /. mm = p . m by A6, PARTFUN1:def_6
.= (Shift (p,j)) . (m + j) by A6, VALUED_1:def_12
.= (Shift (p,j)) /. xx by A4, A7, PARTFUN1:def_6 ;
thus (Shift ((IncAddr (p,i)),j)) . x = (IncAddr (p,i)) . m by A5, A4, VALUED_1:def_12
.= IncAddr (((Shift (p,j)) /. xx),i) by A6, A8, Def21
.= (IncAddr ((Shift (p,j)),i)) . x by A7, Def21 ; ::_thesis: verum
end;
hence  Shift ((IncAddr (p,i)),j) = IncAddr ((Shift (p,j)),i) by A1, FUNCT_1:2; ::_thesis: verum
end;

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 & I = g . il holds
IncAddr (I,k) = (Reloc (g,k)) . (il + k)
proof
let il be Nat; ::_thesis: for S being COM-Struct
for g being NAT -defined the InstructionsF of b1 -valued finite Function
for k being Nat
for I being Instruction of S st il in dom g & I = g . il holds
IncAddr (I,k) = (Reloc (g,k)) . (il + k)
let S be COM-Struct ; ::_thesis: for g being NAT -defined the InstructionsF of S -valued finite Function
for k being Nat
for I being Instruction of S st il in dom g & I = g . il holds
IncAddr (I,k) = (Reloc (g,k)) . (il + k)
let g be NAT -defined the InstructionsF of S -valued finite Function; ::_thesis: for k being Nat
for I being Instruction of S st il in dom g & I = g . il holds
IncAddr (I,k) = (Reloc (g,k)) . (il + k)
let k be Nat; ::_thesis: for I being Instruction of S st il in dom g & I = g . il holds
IncAddr (I,k) = (Reloc (g,k)) . (il + k)
let I be Instruction of S; ::_thesis: ( il in dom g & I = g . il implies IncAddr (I,k) = (Reloc (g,k)) . (il + k) )
assume that
A1: il in dom g and
A2: I = g . il ; ::_thesis: IncAddr (I,k) = (Reloc (g,k)) . (il + k)
reconsider ii = il as Element of NAT by ORDINAL1:def_12;
A3: il in dom (IncAddr (g,k)) by A1, Def21;
thus (Reloc (g,k)) . (il + k) = (IncAddr (g,k)) . ii by A3, VALUED_1:def_12
.= IncAddr ((g /. ii),k) by A1, Def21
.= IncAddr (I,k) by A1, A2, PARTFUN1:def_6 ; ::_thesis: verum
end;


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 & 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)
proof
let S be COM-Struct ; ::_thesis: for I being Program of S holds 0 in dom (stop I)
let I be Program of S; ::_thesis: 0 in dom (stop I)
card (stop I) = (card I) + (card (Stop S)) by AFINSQ_1:17
.= (card I) + 1 by AFINSQ_1:33 ;
hence  0 in dom (stop I) by AFINSQ_1:66; ::_thesis: verum
end;

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 & 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
proof
 rng (Stop S) = {(halt S)} by AFINSQ_1:33;
hence  halt S in rng (Stop S) by TARSKI:def_1; :: according to COMPOS_1:def_11 ::_thesis: verum
end;
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 & b1 is finite )
proof
take  Stop S ; ::_thesis: ( not Stop S is halt-free & Stop S is finite )
thus  ( not Stop S is halt-free & Stop S is finite ) ; ::_thesis: verum
end;
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
proof
A1: halt S in rng q by Def11;
 rng q c= rng (p +* q) by FUNCT_4:18;
hence  halt S in rng (p +* q) by A1; :: according to COMPOS_1:def_11 ::_thesis: verum
end;
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
proof
A1: dom p c= NAT by RELAT_1:def_18;
 halt S in rng p by Def11;
then consider x being set  such that
A2: x in dom p and
A3: p . x = halt S by FUNCT_1:def_3;
A4: x in dom (IncAddr (p,k)) by A2, Def21;
A5: dom (IncAddr (p,k)) c= NAT by RELAT_1:def_18;
reconsider m = x as Element of NAT by A1, A2;
(IncAddr (p,k)) . m = IncAddr ((p /. m),k) by A2, Def21
.= IncAddr ((halt S),k) by A3, A2, PARTFUN1:def_6
.= halt S by COMPOS_0:4 ;
then  halt S in rng (IncAddr (p,k)) by A4, FUNCT_1:3;
hence  halt S in rng (Reloc (p,k)) by A5, VALUED_1:26; :: according to COMPOS_1:def_11 ::_thesis: verum
end;
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 & not b1 is empty )
proof
take  Stop S ; ::_thesis: ( not Stop S is halt-free & not Stop S is empty )
thus  ( not Stop S is halt-free & not Stop S is empty ) ; ::_thesis: verum
end;
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))
proof
let n be Nat; ::_thesis: for S being COM-Struct
for p, q being NAT -defined the InstructionsF of b1 -valued finite Function holds IncAddr ((p +* q),n) = (IncAddr (p,n)) +* (IncAddr (q,n))
let S be COM-Struct ; ::_thesis: for p, q being NAT -defined the InstructionsF of S -valued finite Function holds IncAddr ((p +* q),n) = (IncAddr (p,n)) +* (IncAddr (q,n))
let p, q be NAT -defined the InstructionsF of S -valued finite Function; ::_thesis: IncAddr ((p +* q),n) = (IncAddr (p,n)) +* (IncAddr (q,n))
A1: dom (IncAddr (q,n)) = dom q by Def21;
A2: now__::_thesis:_for_m_being_Nat_st_m_in_dom_(p_+*_q)_holds_
((IncAddr_(p,n))_+*_(IncAddr_(q,n)))_._m_=_IncAddr_(((p_+*_q)_/._m),n)
let m be Nat; ::_thesis: ( m in dom (p +* q) implies ((IncAddr (p,n)) +* (IncAddr (q,n))) . b1 = IncAddr (((p +* q) /. b1),n) )
assume A3: m in dom (p +* q) ; ::_thesis: ((IncAddr (p,n)) +* (IncAddr (q,n))) . b1 = IncAddr (((p +* q) /. b1),n)
percases ( m in dom q or not m in dom q ) ;
supposeA4: m in dom q ; ::_thesis: ((IncAddr (p,n)) +* (IncAddr (q,n))) . b1 = IncAddr (((p +* q) /. b1),n)
A5: (p +* q) /. m = (p +* q) . m by A3, PARTFUN1:def_6
.= q . m by A4, FUNCT_4:13
.= q /. m by A4, PARTFUN1:def_6 ;
thus ((IncAddr (p,n)) +* (IncAddr (q,n))) . m = (IncAddr (q,n)) . m by A1, A4, FUNCT_4:13
.= IncAddr (((p +* q) /. m),n) by A4, A5, Def21 ; ::_thesis: verum
end;
supposeA6: not m in dom q ; ::_thesis: ((IncAddr (p,n)) +* (IncAddr (q,n))) . b1 = IncAddr (((p +* q) /. b1),n)
 m in (dom p) \/ (dom q) by A3, FUNCT_4:def_1;
then A7: m in dom p by A6, XBOOLE_0:def_3;
A8: (p +* q) /. m = (p +* q) . m by A3, PARTFUN1:def_6
.= p . m by A6, FUNCT_4:11
.= p /. m by A7, PARTFUN1:def_6 ;
thus ((IncAddr (p,n)) +* (IncAddr (q,n))) . m = (IncAddr (p,n)) . m by A1, A6, FUNCT_4:11
.= IncAddr (((p +* q) /. m),n) by A7, A8, Def21 ; ::_thesis: verum
end;
end;
end;
 dom (IncAddr (p,n)) = dom p by Def21;
then  dom ((IncAddr (p,n)) +* (IncAddr (q,n))) = (dom p) \/ (dom q) by A1, FUNCT_4:def_1
.= dom (p +* q) by FUNCT_4:def_1 ;
hence  IncAddr ((p +* q),n) = (IncAddr (p,n)) +* (IncAddr (q,n)) by A2, Def21; ::_thesis: verum
end;

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))
proof
let S be COM-Struct ; ::_thesis: for p, q being NAT -defined the InstructionsF of S -valued finite Function
for k being Nat holds Reloc ((p +* q),k) = (Reloc (p,k)) +* (Reloc (q,k))
let p, q be NAT -defined the InstructionsF of S -valued finite Function; ::_thesis: for k being Nat holds Reloc ((p +* q),k) = (Reloc (p,k)) +* (Reloc (q,k))
let k be Nat; ::_thesis: Reloc ((p +* q),k) = (Reloc (p,k)) +* (Reloc (q,k))
A1: Reloc ((p +* q),k) = IncAddr ((Shift ((p +* q),k)),k) by Th34;
A2: Reloc (p,k) = IncAddr ((Shift (p,k)),k) by Th34;
A3: Reloc (q,k) = IncAddr ((Shift (q,k)),k) by Th34;
thus  Reloc ((p +* q),k) = IncAddr (((Shift (p,k)) +* (Shift (q,k))),k) by A1, VALUED_1:23
.= (Reloc (p,k)) +* (Reloc (q,k)) by A2, A3, Th41 ; ::_thesis: verum
end;

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))
proof
let S be COM-Struct ; ::_thesis: for p being NAT -defined the InstructionsF of S -valued finite Function
for m, n being Nat holds Reloc ((Reloc (p,m)),n) = Reloc (p,(m + n))
let p be NAT -defined the InstructionsF of S -valued finite Function; ::_thesis: for m, n being Nat holds Reloc ((Reloc (p,m)),n) = Reloc (p,(m + n))
let m, n be Nat; ::_thesis: Reloc ((Reloc (p,m)),n) = Reloc (p,(m + n))
thus  Reloc ((Reloc (p,m)),n) = Shift ((Shift ((IncAddr ((IncAddr (p,m)),n)),m)),n) by Th34
.= Shift ((Shift ((IncAddr (p,(m + n))),m)),n) by Th17
.= Reloc (p,(m + n)) by VALUED_1:21 ; ::_thesis: verum
end;

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)
proof
let S be COM-Struct ; ::_thesis: for P, Q being NAT -defined the InstructionsF of S -valued finite Function
for k being Nat st P c= Q holds
Reloc (P,k) c= Reloc (Q,k)
let P, Q be NAT -defined the InstructionsF of S -valued finite Function; ::_thesis: for k being Nat st P c= Q holds
Reloc (P,k) c= Reloc (Q,k)
let k be Nat; ::_thesis: ( P c= Q implies Reloc (P,k) c= Reloc (Q,k) )
set rP = Reloc (P,k);
set rQ = Reloc (Q,k);
A1: dom (Reloc (P,k)) =  {  (m + k) where m is Element of NAT : m in dom P  }  by Th33;
A2: dom (Shift (P,k)) =  {  (m + k) where m is Element of NAT : m in dom P  }  by VALUED_1:def_12;
A3: dom (Shift (Q,k)) =  {  (m + k) where m is Element of NAT : m in dom Q  }  by VALUED_1:def_12;
A4: Reloc (Q,k) = IncAddr ((Shift (Q,k)),k) by Th34;
assume A5: P c= Q ; ::_thesis: Reloc (P,k) c= Reloc (Q,k)
then A6: Shift (P,k) c= Shift (Q,k) by VALUED_1:20;
A7: dom P c= dom Q by A5, GRFUNC_1:2;
A8: now__::_thesis:_for_x_being_set_st_x_in_dom_(Reloc_(P,k))_holds_
(Reloc_(P,k))_._x_=_(Reloc_(Q,k))_._x
let x be set ; ::_thesis: ( x in dom (Reloc (P,k)) implies (Reloc (P,k)) . x = (Reloc (Q,k)) . x )
assume  x in dom (Reloc (P,k)) ; ::_thesis: (Reloc (P,k)) . x = (Reloc (Q,k)) . x
then consider m1 being Element of NAT  such that
A9: x = m1 + k and
A10: m1 in dom P by A1;
A11: m1 + k in dom (Shift (Q,k)) by A7, A3, A10;
A12: m1 + k in dom (Shift (P,k)) by A2, A10;
then A13: (Shift (P,k)) /. (m1 + k) = (Shift (P,k)) . (m1 + k) by PARTFUN1:def_6
.= (Shift (Q,k)) . (m1 + k) by A6, A12, GRFUNC_1:2
.= (Shift (Q,k)) /. (m1 + k) by A11, PARTFUN1:def_6 ;
thus (Reloc (P,k)) . x = (IncAddr ((Shift (P,k)),k)) . x by Th34
.= IncAddr (((Shift (Q,k)) /. (m1 + k)),k) by A12, A13, A9, Def21
.= (Reloc (Q,k)) . x by A9, A11, A4, Def21 ; ::_thesis: verum
end;
A14: dom (Shift (P,k)) c= dom (Shift (Q,k)) by A6, GRFUNC_1:2;
now__::_thesis:_for_x_being_set_st_x_in_dom_(Reloc_(P,k))_holds_
x_in_dom_(Reloc_(Q,k))
let x be set ; ::_thesis: ( x in dom (Reloc (P,k)) implies x in dom (Reloc (Q,k)) )
assume  x in dom (Reloc (P,k)) ; ::_thesis: x in dom (Reloc (Q,k))
then  x in dom (Shift (P,k)) by Th32;
then  x in dom (Shift (Q,k)) by A14;
hence  x in dom (Reloc (Q,k)) by Th32; ::_thesis: verum
end;
then  dom (Reloc (P,k)) c= dom (Reloc (Q,k)) by TARSKI:def_3;
hence  Reloc (P,k) c= Reloc (Q,k) by A8, GRFUNC_1:2; ::_thesis: verum
end;

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)) )
proof
let il be Nat; ::_thesis: 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)) )
let S be COM-Struct ; ::_thesis: for k being Nat
for P being preProgram of S holds
( il in dom P iff il + k in dom (Reloc (P,k)) )
let k be Nat; ::_thesis: for P being preProgram of S holds
( il in dom P iff il + k in dom (Reloc (P,k)) )
let P be preProgram of S; ::_thesis: ( il in dom P iff il + k in dom (Reloc (P,k)) )
A1: dom (Reloc (P,k)) =  {  (j + k) where j is Element of NAT : j in dom P  }  by Th33;
reconsider il1 = il as Element of NAT by ORDINAL1:def_12;
 ( il1 in dom P implies il1 + k in dom (Reloc (P,k)) ) by A1;
hence  ( il in dom P implies il + k in dom (Reloc (P,k)) ) ; ::_thesis: ( il + k in dom (Reloc (P,k)) implies il in dom P )
assume  il + k in dom (Reloc (P,k)) ; ::_thesis: il in dom P
then  ex j being Element of NAT st
( il + k = j + k & j in dom P ) by A1;
hence  il in dom P ; ::_thesis: verum
end;

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))
proof
let n be Nat; ::_thesis: 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 b1 -valued finite Function holds IncAddr ((f * s),n) = ((id the InstructionsF of S) +* ((halt S) .--> (IncAddr (i,n)))) * (IncAddr (s,n))
let S be COM-Struct ; ::_thesis: 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 S -valued finite Function holds IncAddr ((f * s),n) = ((id the InstructionsF of S) +* ((halt S) .--> (IncAddr (i,n)))) * (IncAddr (s,n))
let i be Instruction of S; ::_thesis: 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 S -valued finite Function holds IncAddr ((f * s),n) = ((id the InstructionsF of S) +* ((halt S) .--> (IncAddr (i,n)))) * (IncAddr (s,n))
let f be Function of the InstructionsF of S, the InstructionsF of S; ::_thesis: ( f = (id the InstructionsF of S) +* ((halt S) .--> i) implies for s being NAT -defined the InstructionsF of S -valued finite Function holds IncAddr ((f * s),n) = ((id the InstructionsF of S) +* ((halt S) .--> (IncAddr (i,n)))) * (IncAddr (s,n)) )
assume A1: f = (id the InstructionsF of S) +* ((halt S) .--> i) ; ::_thesis: for s being NAT -defined the InstructionsF of S -valued finite Function holds IncAddr ((f * s),n) = ((id the InstructionsF of S) +* ((halt S) .--> (IncAddr (i,n)))) * (IncAddr (s,n))
let s be NAT -defined the InstructionsF of S -valued finite Function; ::_thesis: IncAddr ((f * s),n) = ((id the InstructionsF of S) +* ((halt S) .--> (IncAddr (i,n)))) * (IncAddr (s,n))
 rng ((halt S) .--> (IncAddr (i,n))) = {(IncAddr (i,n))} by FUNCOP_1:8;
then A2: rng ((id the InstructionsF of S) +* ((halt S) .--> (IncAddr (i,n)))) c= (rng (id the InstructionsF of S)) \/ {(IncAddr (i,n))} by FUNCT_4:17;
A3: (rng (id the InstructionsF of S)) \/ {(IncAddr (i,n))} = the InstructionsF of S by ZFMISC_1:40;
A4: dom ((halt S) .--> (IncAddr (i,n))) = {(halt S)} by FUNCOP_1:13;
then  dom ((id the InstructionsF of S) +* ((halt S) .--> (IncAddr (i,n)))) = (dom (id the InstructionsF of S)) \/ {(halt S)} by FUNCT_4:def_1
.= the InstructionsF of S by ZFMISC_1:40 ;
then reconsider g = (id the InstructionsF of S) +* ((halt S) .--> (IncAddr (i,n))) as Function of the InstructionsF of S, the InstructionsF of S by A2, A3, RELSET_1:4;
A5: dom (IncAddr (s,n)) = dom s by Def21
.= dom (f * s) by FUNCT_2:123 ;
A6: dom ((halt S) .--> i) = {(halt S)} by FUNCOP_1:13;
A7: now__::_thesis:_for_m_being_Nat_st_m_in_dom_(f_*_s)_holds_
(g_*_(IncAddr_(s,n)))_._m_=_IncAddr_(((f_*_s)_/._m),n)
let m be Nat; ::_thesis: ( m in dom (f * s) implies (g * (IncAddr (s,n))) . b1 = IncAddr (((f * s) /. b1),n) )
assume A8: m in dom (f * s) ; ::_thesis: (g * (IncAddr (s,n))) . b1 = IncAddr (((f * s) /. b1),n)
then A9: m in dom s by FUNCT_2:123;
percases ( s . m = halt S or s . m <> halt S ) ;
supposeA10: s . m = halt S ; ::_thesis: (g * (IncAddr (s,n))) . b1 = IncAddr (((f * s) /. b1),n)
reconsider mm = m as Element of NAT by ORDINAL1:def_12;
A11: (IncAddr (s,n)) . m = IncAddr ((s /. mm),n) by A9, Def21
.= IncAddr ((halt S),n) by A9, A10, PARTFUN1:def_6
.= halt S by COMPOS_0:4 ;
A12: halt S in {(halt S)} by TARSKI:def_1;
A13: (f * s) /. m = (f * s) . m by A8, PARTFUN1:def_6
.= f . (halt S) by A9, A10, FUNCT_1:13
.= ((halt S) .--> i) . (halt S) by A1, A6, A12, FUNCT_4:13
.= i by FUNCOP_1:72 ;
thus (g * (IncAddr (s,n))) . m = g . ((IncAddr (s,n)) . m) by A5, A8, FUNCT_1:13
.= ((halt S) .--> (IncAddr (i,n))) . ((IncAddr (s,n)) . m) by A4, A11, A12, FUNCT_4:13
.= IncAddr (((f * s) /. m),n) by A11, A13, FUNCOP_1:72 ; ::_thesis: verum
end;
supposeA14: s . m <> halt S ; ::_thesis: (g * (IncAddr (s,n))) . b1 = IncAddr (((f * s) /. b1),n)
A15: s /. m = s . m by A9, PARTFUN1:def_6;
A16: not IncAddr ((s /. m),n) = halt S by COMPOS_0:12, A14, A15;
A17: not s /. m in {(halt S)} by A14, A15, TARSKI:def_1;
A18: not IncAddr ((s /. m),n) in {(halt S)} by A16, TARSKI:def_1;
A19: (f * s) /. m = (f * s) . m by A8, PARTFUN1:def_6
.= f . (s . m) by A9, FUNCT_1:13
.= (id the InstructionsF of S) . (s /. m) by A1, A6, A15, A17, FUNCT_4:11
.= s /. m by FUNCT_1:18 ;
thus (g * (IncAddr (s,n))) . m = g . ((IncAddr (s,n)) . m) by A5, A8, FUNCT_1:13
.= g . (IncAddr ((s /. m),n)) by A9, Def21
.= (id the InstructionsF of S) . (IncAddr ((s /. m),n)) by A4, A18, FUNCT_4:11
.= IncAddr (((f * s) /. m),n) by A19, FUNCT_1:18 ; ::_thesis: verum
end;
end;
end;
 dom (g * (IncAddr (s,n))) = dom (IncAddr (s,n)) by FUNCT_2:123;
hence  IncAddr ((f * s),n) = ((id the InstructionsF of S) +* ((halt S) .--> (IncAddr (i,n)))) * (IncAddr (s,n)) by A5, A7, Def21; ::_thesis: verum
end;


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)))
proof
let S be COM-Struct ; ::_thesis: for I, J being Program of S holds dom I misses dom (Reloc (J,(card I)))
let I, J be Program of S; ::_thesis: dom I misses dom (Reloc (J,(card I)))
assume A1: dom I meets dom (Reloc (J,(card I))) ; ::_thesis: contradiction
dom (Reloc (J,(card I))) = dom (Shift (J,(card I))) by Th32
.=  {  (l + (card I)) where l is Element of NAT : l in dom J  }  by VALUED_1:def_12 ;
then consider x being set  such that
A2: x in dom I and
A3: x in  {  (l + (card I)) where l is Element of NAT : l in dom J  }  by A1, XBOOLE_0:3;
consider l being Element of NAT  such that
A4: x = l + (card I) and
 l in dom J by A3;
 l + (card I) < card I by A2, A4, AFINSQ_1:66;
hence  contradiction by NAT_1:11; ::_thesis: verum
end;

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
proof
let m be Nat; ::_thesis: for S being COM-Struct
for I being preProgram of S holds card (Reloc (I,m)) = card I
let S be COM-Struct ; ::_thesis: for I being preProgram of S holds card (Reloc (I,m)) = card I
let I be preProgram of S; ::_thesis: card (Reloc (I,m)) = card I
deffunc H1( Nat) ->  Nat = $1;
set B =  {  l where l is Element of NAT : H1(l) in dom I  }  ;
A1: for x being set st x in dom I holds
ex d being Element of NAT st x = H1(d)
proof
let x be set ; ::_thesis: ( x in dom I implies ex d being Element of NAT st x = H1(d) )
assume A2: x in dom I ; ::_thesis: ex d being Element of NAT st x = H1(d)
 dom I c= NAT by RELAT_1:def_18;
then reconsider l = x as Element of NAT by A2;
reconsider d = l as Element of NAT ;
 l = H1(d) ;
hence  ex d being Element of NAT st x = H1(d) ; ::_thesis: verum
end;
A3: for d1, d2 being Element of NAT st H1(d1) = H1(d2) holds
d1 = d2 ;
A4: dom I, {  l where l is Element of NAT : H1(l) in dom I  }  are_equipotent from FUNCT_7:sch_3(A1, A3);
defpred S1[ Nat] means $1 in dom I;
deffunc H2( Nat) ->  set = $1 + m;
defpred S2[ Nat] means H1($1) in dom I;
set D =  {  l where l is Element of NAT : S2[l]  }  ;
set C =  {  H2(l) where l is Element of NAT : l in  {  l where l is Element of NAT : H1(l) in dom I  }   }  ;
defpred S3[ set ] means verum;
  {  l where l is Element of NAT : S2[l]  }  is Subset of NAT from DOMAIN_1:sch_7();
then A5:  {  l where l is Element of NAT : H1(l) in dom I  }  c= NAT ;
A6: for d1, d2 being Element of NAT st H2(d1) = H2(d2) holds
d1 = d2 ;
A7:  {  l where l is Element of NAT : H1(l) in dom I  }  , {  H2(l) where l is Element of NAT : l in  {  l where l is Element of NAT : H1(l) in dom I  }   }  are_equipotent from FUNCT_7:sch_4(A5, A6);
set C =  {  H2(l) where l is Element of NAT : ( l in  {  n where n is Element of NAT : S1[n]  }  & S3[l] )  }  ;
set A =  {  H2(l) where l is Element of NAT : ( S1[l] & S3[l] )  }  ;
A8:  {  H2(l) where l is Element of NAT : ( l in  {  n where n is Element of NAT : S1[n]  }  & S3[l] )  }  =  {  (l + m) where l is Element of NAT : l in  {  l where l is Element of NAT : H1(l) in dom I  }   }
proof
thus   {  H2(l) where l is Element of NAT : ( l in  {  n where n is Element of NAT : S1[n]  }  & S3[l] )  }  c=  {  (l + m) where l is Element of NAT : l in  {  l where l is Element of NAT : H1(l) in dom I  }   }  :: according to XBOOLE_0:def_10 ::_thesis:  {  (l + m) where l is Element of NAT : l in  {  l where l is Element of NAT : H1(l) in dom I  }   }  c=  {  H2(l) where l is Element of NAT : ( l in  {  n where n is Element of NAT : S1[n]  }  & S3[l] )  }
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in  {  H2(l) where l is Element of NAT : ( l in  {  n where n is Element of NAT : S1[n]  }  & S3[l] )  }  or e in  {  (l + m) where l is Element of NAT : l in  {  l where l is Element of NAT : H1(l) in dom I  }   }  )
assume  e in  {  H2(l) where l is Element of NAT : ( l in  {  n where n is Element of NAT : S1[n]  }  & S3[l] )  }  ; ::_thesis: e in  {  (l + m) where l is Element of NAT : l in  {  l where l is Element of NAT : H1(l) in dom I  }   }
then  ex l being Element of NAT st
( e = H2(l) & l in  {  l where l is Element of NAT : H1(l) in dom I  }  ) ;
hence  e in  {  (l + m) where l is Element of NAT : l in  {  l where l is Element of NAT : H1(l) in dom I  }   }  ; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in  {  (l + m) where l is Element of NAT : l in  {  l where l is Element of NAT : H1(l) in dom I  }   }  or e in  {  H2(l) where l is Element of NAT : ( l in  {  n where n is Element of NAT : S1[n]  }  & S3[l] )  }  )
assume  e in  {  (l + m) where l is Element of NAT : l in  {  l where l is Element of NAT : H1(l) in dom I  }   }  ; ::_thesis: e in  {  H2(l) where l is Element of NAT : ( l in  {  n where n is Element of NAT : S1[n]  }  & S3[l] )  }
then  ex l being Element of NAT st
( e = l + m & l in  {  l where l is Element of NAT : H1(l) in dom I  }  ) ;
hence  e in  {  H2(l) where l is Element of NAT : ( l in  {  n where n is Element of NAT : S1[n]  }  & S3[l] )  }  ; ::_thesis: verum
end;
  {  H2(l) where l is Element of NAT : ( S1[l] & S3[l] )  }  =  {  (l + m) where l is Element of NAT : l in dom I  }
proof
thus   {  H2(l) where l is Element of NAT : ( S1[l] & S3[l] )  }  c=  {  (l + m) where l is Element of NAT : l in dom I  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  (l + m) where l is Element of NAT : l in dom I  }  c=  {  H2(l) where l is Element of NAT : ( S1[l] & S3[l] )  }
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in  {  H2(l) where l is Element of NAT : ( S1[l] & S3[l] )  }  or e in  {  (l + m) where l is Element of NAT : l in dom I  }  )
assume  e in  {  H2(l) where l is Element of NAT : ( S1[l] & S3[l] )  }  ; ::_thesis: e in  {  (l + m) where l is Element of NAT : l in dom I  }
then  ex l being Element of NAT st
( e = H2(l) & l in dom I ) ;
hence  e in  {  (l + m) where l is Element of NAT : l in dom I  }  ; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in  {  (l + m) where l is Element of NAT : l in dom I  }  or e in  {  H2(l) where l is Element of NAT : ( S1[l] & S3[l] )  }  )
assume  e in  {  (l + m) where l is Element of NAT : l in dom I  }  ; ::_thesis: e in  {  H2(l) where l is Element of NAT : ( S1[l] & S3[l] )  }
then  ex l being Element of NAT st
( e = l + m & l in dom I ) ;
hence  e in  {  H2(l) where l is Element of NAT : ( S1[l] & S3[l] )  }  ; ::_thesis: verum
end;
then A9: dom (Shift (I,m)) =  {  H2(l) where l is Element of NAT : ( S1[l] & S3[l] )  }  by VALUED_1:def_12;
  {  H2(l) where l is Element of NAT : ( l in  {  n where n is Element of NAT : S1[n]  }  & S3[l] )  }  =  {  H2(l) where l is Element of NAT : ( S1[l] & S3[l] )  }  from FRAENKEL:sch_14();
then A10: dom (Shift (I,m)), dom I are_equipotent by A4, A7, A8, A9, WELLORD2:15;
thus  card (Reloc (I,m)) = card (dom (Reloc (I,m))) by CARD_1:62
.= card (dom (Shift (I,m))) by Th32
.= card (dom I) by A10, CARD_1:5
.= card I by CARD_1:62 ; ::_thesis: verum
end;


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 )
proof
let x be set ; ::_thesis: for S being COM-Struct
for i being Instruction of S holds
( x in dom (Load i) iff x = 0 )
let S be COM-Struct ; ::_thesis: for i being Instruction of S holds
( x in dom (Load i) iff x = 0 )
let i be Instruction of S; ::_thesis: ( x in dom (Load i) iff x = 0 )
 dom (Load i) = {0} by FUNCOP_1:13;
hence  ( x in dom (Load i) iff x = 0 ) by TARSKI:def_1; ::_thesis: verum
end;

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) & (stop I) . loc <> halt S holds
loc in dom I
proof
let S be COM-Struct ; ::_thesis: for I being Program of S
for loc being Nat st loc in dom (stop I) & (stop I) . loc <> halt S holds
loc in dom I
let I be Program of S; ::_thesis: for loc being Nat st loc in dom (stop I) & (stop I) . loc <> halt S holds
loc in dom I
let loc be Nat; ::_thesis: ( loc in dom (stop I) & (stop I) . loc <> halt S implies loc in dom I )
assume that
A1: loc in dom (stop I) and
A2: (stop I) . loc <> halt S ; ::_thesis: loc in dom I
set SS = Stop S;
set S2 = Shift ((Stop S),(card I));
A3: stop I = I +* (Shift ((Stop S),(card I))) by AFINSQ_1:77;
assume  not loc in dom I ; ::_thesis: contradiction
then  loc in dom (Shift ((Stop S),(card I))) by A1, A3, FUNCT_4:12;
then  loc in  {  (l1 + (card I)) where l1 is Element of NAT : l1 in dom (Stop S)  }  by VALUED_1:def_12;
then consider l1 being Element of NAT  such that
A4: loc = l1 + (card I) and
A5: l1 in dom (Stop S) ;
A6: 0 in dom (Stop S) by Th3;
A7: (Stop S) . 0 = halt S by AFINSQ_1:34;
 dom (Stop S) = {0} by AFINSQ_1:33, CARD_1:49;
then  l1 = 0 by A5, TARSKI:def_1;
hence  contradiction by A2, A4, A7, A6, AFINSQ_1:def_3; ::_thesis: verum
end;

theorem :: COMPOS_1:52
for S being COM-Struct
for i being Instruction of S holds
( dom (Load i) = {0} & (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)
proof
let S be COM-Struct ; ::_thesis: for i being Instruction of S holds 0 in dom (Load i)
let i be Instruction of S; ::_thesis: 0 in dom (Load i)
 dom (Load i) = {0} by FUNCOP_1:13;
hence  0 in dom (Load i) by TARSKI:def_1; ::_thesis: verum
end;

theorem Th54: :: COMPOS_1:54
for S being COM-Struct
for i being Instruction of S holds card (Load i) = 1
proof
let S be COM-Struct ; ::_thesis: for i being Instruction of S holds card (Load i) = 1
let i be Instruction of S; ::_thesis: card (Load i) = 1
A1: dom (Load i) = {0} by FUNCOP_1:13;
thus  card (Load i) = card (dom (Load i))
.= 1 by A1, CARD_1:30 ; ::_thesis: verum
end;

theorem Th55: :: COMPOS_1:55
for S being COM-Struct
for I being Program of S holds card (stop I) = (card I) + 1
proof
let S be COM-Struct ; ::_thesis: for I being Program of S holds card (stop I) = (card I) + 1
let I be Program of S; ::_thesis: card (stop I) = (card I) + 1
thus  card (stop I) = (card I) + (card (Stop S)) by AFINSQ_1:17
.= (card I) + 1 by AFINSQ_1:33 ; ::_thesis: verum
end;

theorem Th56: :: COMPOS_1:56
for S being COM-Struct
for i being Instruction of S holds card (Macro i) = 2
proof
let S be COM-Struct ; ::_thesis: for i being Instruction of S holds card (Macro i) = 2
let i be Instruction of S; ::_thesis: card (Macro i) = 2
thus  card (Macro i) = (card (Load i)) + (card (Stop S)) by AFINSQ_1:17
.= (card (Load i)) + 1 by AFINSQ_1:33
.= 1 + 1 by Th54
.= 2 ; ::_thesis: verum
end;

theorem :: COMPOS_1:57
for S being COM-Struct
for i being Instruction of S holds
( 0 in dom (Macro i) & 1 in dom (Macro i) )
proof
let S be COM-Struct ; ::_thesis: for i being Instruction of S holds
( 0 in dom (Macro i) & 1 in dom (Macro i) )
let i be Instruction of S; ::_thesis: ( 0 in dom (Macro i) & 1 in dom (Macro i) )
 card (Macro i) = 2 by Th56;
hence  ( 0 in dom (Macro i) & 1 in dom (Macro i) ) by AFINSQ_1:66; ::_thesis: verum
end;

theorem :: COMPOS_1:58
for S being COM-Struct
for i being Instruction of S holds (Macro i) . 0 = i
proof
let S be COM-Struct ; ::_thesis: for i being Instruction of S holds (Macro i) . 0 = i
let i be Instruction of S; ::_thesis: (Macro i) . 0 = i
set I = Load i;
 0 in dom (Load i) by Th53;
hence (Macro i) . 0 = (Load i) . 0 by AFINSQ_1:def_3
.= i by FUNCOP_1:72 ;
::_thesis: verum
end;

theorem :: COMPOS_1:59
for S being COM-Struct
for i being Instruction of S holds (Macro i) . 1 = halt S
proof
let S be COM-Struct ; ::_thesis: for i being Instruction of S holds (Macro i) . 1 = halt S
let i be Instruction of S; ::_thesis: (Macro i) . 1 = halt S
A1: 0 in dom (Stop S) by Th3;
A2: (Stop S) . 0 = halt S by AFINSQ_1:34;
 1 = 0 + (card (Load i)) by Th54;
hence  (Macro i) . 1 = halt S by A2, A1, AFINSQ_1:def_3; ::_thesis: verum
end;

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 ) )
proof
let x be set ; ::_thesis: for S being COM-Struct
for i being Instruction of S holds
( x in dom (Macro i) iff ( x = 0 or x = 1 ) )
let S be COM-Struct ; ::_thesis: for i being Instruction of S holds
( x in dom (Macro i) iff ( x = 0 or x = 1 ) )
let i be Instruction of S; ::_thesis: ( x in dom (Macro i) iff ( x = 0 or x = 1 ) )
set si = Macro i;
set A = NAT ;
A1: card (Macro i) = 2 by Th56;
hereby  ::_thesis: ( ( x = 0 or x = 1 ) implies x in dom (Macro i) )
assume A2: x in dom (Macro i) ; ::_thesis: ( x = 0 or x = 1 )
reconsider l = x as Element of NAT by A2;
reconsider n = l as Element of NAT ;
 n < 1 + 1 by A1, A2, AFINSQ_1:66;
then  n <= 1 by NAT_1:13;
hence  ( x = 0 or x = 1 ) by NAT_1:25; ::_thesis: verum
end;
thus  ( ( x = 0 or x = 1 ) implies x in dom (Macro i) ) by A1, AFINSQ_1:66; ::_thesis: verum
end;

theorem :: COMPOS_1:61
for S being COM-Struct
for i being Instruction of S holds dom (Macro i) = {0,1}
proof
let S be COM-Struct ; ::_thesis: for i being Instruction of S holds dom (Macro i) = {0,1}
let i be Instruction of S; ::_thesis: dom (Macro i) = {0,1}
 for x being set holds
( x in dom (Macro i) iff ( x = 0 or x = 1 ) ) by Th60;
hence  dom (Macro i) = {0,1} by TARSKI:def_2; ::_thesis: verum
end;

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)
proof
let S be COM-Struct ; ::_thesis: for I being Program of S
for loc being Nat st loc in dom I holds
loc in dom (stop I)
let I be Program of S; ::_thesis: for loc being Nat st loc in dom I holds
loc in dom (stop I)
let loc be Nat; ::_thesis: ( loc in dom I implies loc in dom (stop I) )
 dom I c= dom (I ^ (Stop S)) by AFINSQ_1:21;
hence  ( loc in dom I implies loc in dom (stop I) ) ; ::_thesis: verum
end;

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) & (stop I) . (card I) = halt S )
proof
let S be COM-Struct ; ::_thesis: for I being Program of S holds
( card I in dom (stop I) & (stop I) . (card I) = halt S )
let I be Program of S; ::_thesis: ( card I in dom (stop I) & (stop I) . (card I) = halt S )
A1: (Stop S) . 0 = halt S by AFINSQ_1:34;
A2: 0 in dom (Stop S) by Th3;
set pI = stop I;
 card (stop I) = (card I) + 1 by Th55;
then  card I < card (stop I) by XREAL_1:29;
hence  card I in dom (stop I) by AFINSQ_1:66; ::_thesis: (stop I) . (card I) = halt S
 (stop I) . (0 + (card I)) = halt S by A1, A2, AFINSQ_1:def_3;
hence  (stop I) . (card I) = halt S ; ::_thesis: verum
end;

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)
proof
let n be Nat; ::_thesis: 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)
let S be COM-Struct ; ::_thesis: 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)
let I be Program of S; ::_thesis: for loc being Nat st loc in dom I holds
(Shift ((stop I),n)) . (loc + n) = (Shift (I,n)) . (loc + n)
let loc be Nat; ::_thesis: ( loc in dom I implies (Shift ((stop I),n)) . (loc + n) = (Shift (I,n)) . (loc + n) )
A1: dom I c= dom (stop I) by AFINSQ_1:21;
reconsider l = loc as Element of NAT by ORDINAL1:def_12;
assume A2: loc in dom I ; ::_thesis: (Shift ((stop I),n)) . (loc + n) = (Shift (I,n)) . (loc + n)
hence (Shift (I,n)) . (loc + n) = I . l by VALUED_1:def_12
.= (stop I) . l by A2, AFINSQ_1:def_3
.= (Shift ((stop I),n)) . (loc + n) by A2, A1, VALUED_1:def_12 ;
::_thesis: verum
end;

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
proof
let n be Nat; ::_thesis: for S being COM-Struct
for I being Program of S holds (Shift ((stop I),n)) . n = (Shift (I,n)) . n
let S be COM-Struct ; ::_thesis: for I being Program of S holds (Shift ((stop I),n)) . n = (Shift (I,n)) . n
let I be Program of S; ::_thesis: (Shift ((stop I),n)) . n = (Shift (I,n)) . n
 card I > 0 ;
then A1: 0 in dom I by AFINSQ_1:66;
thus (Shift ((stop I),n)) . n = (Shift (I,n)) . (0 + n) by A1, Th65
.= (Shift (I,n)) . n ; ::_thesis: verum
end;

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
proof
reconsider p = <%> the InstructionsF of S as preProgram of S ;
take  p ; ::_thesis: p is empty
thus  p is empty ; ::_thesis: verum
end;
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
proof
let p be preProgram of S; ::_thesis: ( p is empty implies p is halt-free )
assume  p is empty ; ::_thesis: p is halt-free
hence  not halt S in rng p ; :: according to COMPOS_1:def_11 ::_thesis: verum
end;
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 )
proof
thus  ( IT is halt-free implies for x being Nat st x in dom IT holds
IT . x <> halt S ) ::_thesis: ( ( for x being Nat st x in dom IT holds
IT . x <> halt S ) implies IT is halt-free )
proof
assume A1: IT is halt-free ; ::_thesis: for x being Nat st x in dom IT holds
IT . x <> halt S
let x be Nat; ::_thesis: ( x in dom IT implies IT . x <> halt S )
assume A2: x in dom IT ; ::_thesis: IT . x <> halt S
reconsider n = x as Element of NAT by ORDINAL1:def_12;
 IT . n in rng IT by A2, FUNCT_1:3;
hence  IT . x <> halt S by A1, Def11; ::_thesis: verum
end;
assume A3: for x being Nat st x in dom IT holds
IT . x <> halt S ; ::_thesis: IT is halt-free
assume  halt S in rng IT ; :: according to COMPOS_1:def_11 ::_thesis: contradiction
then consider x being set  such that
A4: x in dom IT and
A5: halt S = IT . x by FUNCT_1:def_3;
thus  contradiction by A4, A5, A3; ::_thesis: verum
end;
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
proof
let p be non empty preProgram of S; ::_thesis: ( p is halt-free implies p is unique-halt )
assume A1: p is halt-free ; ::_thesis: p is unique-halt
let k be Nat; :: according to COMPOS_1:def_15 ::_thesis: ( p . k = halt S & k in dom p implies k = LastLoc p )
assume that
A2: p . k = halt S and
A3: k in dom p ; ::_thesis: k = LastLoc p
thus  k = LastLoc p by A2, Def27, A3, A1; ::_thesis: verum
end;
end;

theorem :: COMPOS_1:67
for S being COM-Struct
for i being Instruction of S holds rng (Macro i) = {i,(halt S)}
proof
let S be COM-Struct ; ::_thesis: for i being Instruction of S holds rng (Macro i) = {i,(halt S)}
let i be Instruction of S; ::_thesis: rng (Macro i) = {i,(halt S)}
thus  rng (Macro i) = (rng (Load i)) \/ (rng (Stop S)) by AFINSQ_1:26
.= {i} \/ (rng (Stop S)) by AFINSQ_1:33
.= {i} \/ {(halt S)} by AFINSQ_1:33
.= {i,(halt S)} by ENUMSET1:1 ; ::_thesis: verum
end;

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
proof
let k be Nat; :: according to COMPOS_1:def_15 ::_thesis: ( (stop p) . k = halt S & k in dom (stop p) implies k = LastLoc (stop p) )
assume that
A1: (stop p) . k = halt S and
A2: k in dom (stop p) ; ::_thesis: k = LastLoc (stop p)
A3: dom (stop p) = (dom (CutLastLoc (stop p))) \/ {(LastLoc (stop p))} by VALUED_1:37;
now__::_thesis:_not_k_in_dom_(CutLastLoc_(stop_p))
assume  k in dom (CutLastLoc (stop p)) ; ::_thesis: contradiction
then A4: k in dom p ;
then  p . k = halt S by AFINSQ_1:def_3, A1;
hence  contradiction by Def27, A4; ::_thesis: verum
end;
then  k in {(LastLoc (stop p))} by A2, A3, XBOOLE_0:def_3;
hence  k = LastLoc (stop p) by TARSKI:def_1; ::_thesis: verum
end;
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;