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

definition end;

definition
::$CD 7 func Trivial-COM -> strict COM-Struct means :Def1: :: COMPOS_1:def 8 the InstructionsF of it = ; existence ex b1 being strict COM-Struct st the InstructionsF of b1 = proof end; uniqueness for b1, b2 being strict COM-Struct st the InstructionsF of b1 = & the InstructionsF of b2 = 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 Def1 defines Trivial-COM COMPOS_1:def 8 : for b1 being strict COM-Struct holds ( b1 = Trivial-COM iff the InstructionsF of b1 = ); definition let S be COM-Struct ; mode Instruction of S is Element of the InstructionsF of S; end; definition let S be COM-Struct ; func halt S -> Instruction of S equals :: COMPOS_1:def 10 halt the InstructionsF of S; coherence halt the InstructionsF of S is Instruction of S ; end; :: deftheorem COMPOS_1:def 9 : canceled; :: deftheorem defines halt COMPOS_1:def 10 : for S being COM-Struct holds halt S = halt the InstructionsF of S; :: Definicje musi zachowac, zeby nie musiec pisac :: halt SCM-Instr, zamiast halt SCM, zreszta wyrzucenie jej :: spowodowaloby problemy z typowaniem. definition let S be COM-Struct ; let I be the InstructionsF of S -valued Function; attr I is halt-free means :Def3: :: COMPOS_1:def 11 not halt S in rng I; end; :: deftheorem Def3 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 ); definition end; definition let S be COM-Struct ; let P be Instruction-Sequence of S; let k be Nat; :: original: . redefine func P . k -> Instruction of S; coherence P . k is Instruction of S proof end; end; definition let S be COM-Struct ; let p be NAT -defined the InstructionsF of S -valued Function; let l be set ; pred p halts_at l means :: COMPOS_1:def 12 ( l in dom p & p . l = halt S ); end; :: deftheorem 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 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 ); notation let S be COM-Struct ; let i be Instruction of S; synonym Load i for <%S%>; end; registration let S be COM-Struct ; 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 end; end; definition end; definition let S be COM-Struct ; let F be non empty preProgram of S; attr F is halt-ending means :Def6: :: COMPOS_1:def 14 F . () = halt S; attr F is unique-halt means :Def7: :: COMPOS_1:def 15 for f being Nat st F . f = halt S & f in dom F holds f = LastLoc F; end; :: deftheorem Def6 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 . () = halt S ); :: deftheorem Def7 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 ; coherence for b1 being non empty preProgram of S st b1 is halt-ending holds not b1 is halt-free proof end; end; registration let S be COM-Struct ; existence ex b1 being preProgram of S st ( b1 is trivial & b1 is initial & not b1 is empty ) proof 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; ::$CT
theorem :: COMPOS_1:2
for ins being Element of the InstructionsF of Trivial-COM holds InsCode ins = 0
proof end;

definition
let S be COM-Struct ;
func Stop S -> preProgram of S equals :: COMPOS_1:def 16
coherence
;
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 -> initial non empty;
:: coherence;
:: end;
registration
let S be COM-Struct ;
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 in dom (Stop S) )
let S be COM-Struct ; :: thesis: ( dom (Stop S) = & 0 in dom (Stop S) )
thus dom (Stop S) = ; :: thesis: 0 in dom (Stop S)
thus 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 end;

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

registration
let S be COM-Struct ;
coherence
( Stop S is halt-ending & Stop S is unique-halt )
proof end;
end;

registration
let S be COM-Struct ;
existence
ex b1 being Program of S st
( b1 is halt-ending & b1 is unique-halt & b1 is trivial )
proof end;
end;

definition end;

registration
let S be COM-Struct ;
existence
ex b1 being preProgram of S st
( b1 is initial & not b1 is empty )
proof end;
end;

theorem Th2: :: COMPOS_1:3
for S being COM-Struct holds 0 in dom (Stop S)
proof end;

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

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 end;

theorem Th4: :: COMPOS_1:5
for I being Instruction of Trivial-COM holds JumpPart I = 0
proof end;

theorem :: COMPOS_1:6
for T being InsType of the InstructionsF of Trivial-COM holds JumpParts T =
proof end;

registration
let S be COM-Struct ;
coherence
for b1 being non empty preProgram of S st b1 is trivial holds
b1 is unique-halt
proof end;
end;

theorem :: COMPOS_1:7
canceled;

::$CT theorem Th6: :: COMPOS_1:8 for S being COM-Struct for F being MacroInstruction of S st card F = 1 holds F = Stop S proof end; theorem :: COMPOS_1:9 for S being COM-Struct holds LastLoc (Stop S) = 0 by Lm3; definition let S be COM-Struct ; let p be preProgram of S; 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 :Def9: :: 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 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 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 Def9 defines IncAddr COMPOS_1:def 21 : for S being COM-Struct for p being preProgram of S 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 preProgram of S; 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 preProgram of S; let k be Nat; cluster IncAddr (F,k) -> empty NAT -defined the InstructionsF of S -valued finite ; coherence IncAddr (F,k) is empty proof end; end; registration let S be COM-Struct ; let F be non empty preProgram of S; 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 end; end; registration let S be COM-Struct ; let F be initial preProgram of S; let k be Nat; coherence IncAddr (F,k) is initial proof 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; ::$CT 6
registration
let S be COM-Struct ;
let F be preProgram of S;
reducibility
proof end;
end;

theorem :: COMPOS_1:16
canceled;

::$CT theorem Th8: :: COMPOS_1:17 for k, m being Nat for S being COM-Struct for F being preProgram of S holds IncAddr ((IncAddr (F,k)),m) = IncAddr (F,(k + m)) proof end; definition let S be COM-Struct ; let p be preProgram of S; 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 preProgram of S for k being Nat holds Reloc (p,k) = Shift ((IncAddr (p,k)),k); theorem Th9: :: COMPOS_1:18 for S being COM-Struct for F being Program of S for G being non empty preProgram of S holds dom () misses dom (Reloc (G,((card F) -' 1))) proof end; theorem Th10: :: COMPOS_1:19 for S being COM-Struct for F being unique-halt Program of S for I being Nat st I in dom () holds () . I <> halt S proof end; definition let S be COM-Struct ; let F, G be non empty preProgram of S; func F ';' G -> preProgram of S equals :: COMPOS_1:def 23 () +* (Reloc (G,((card F) -' 1))); coherence () +* (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 = () +* (Reloc (G,((card F) -' 1))); registration let S be COM-Struct ; let F, G be non empty preProgram of S; cluster F ';' G -> non empty ; coherence ( not F ';' G is empty & F ';' G is the InstructionsF of S -valued & F ';' G is NAT -defined ) ; end; theorem Th11: :: COMPOS_1:20 for S being COM-Struct for F being Program of S for G being non empty preProgram of S holds ( card (F ';' G) = ((card F) + (card G)) - 1 & card (F ';' G) = ((card F) + (card G)) -' 1 ) proof end; registration let S be COM-Struct ; let F, G be Program of S; cluster F ';' G -> initial ; coherence F ';' G is initial proof end; end; theorem :: COMPOS_1:21 for S being COM-Struct for F, G being Program of S holds dom F c= dom (F ';' G) proof end; registration let S be COM-Struct ; let F, G be Program of S; cluster F ';' G -> non empty initial ; coherence ( F ';' G is initial & not F ';' G is empty ) ; end; theorem Th13: :: COMPOS_1:22 for S being COM-Struct for F, G being Program of S holds CutLastLoc F c= CutLastLoc (F ';' G) proof end; theorem Th14: :: COMPOS_1:23 for S being COM-Struct for F, G being Program of S holds (F ';' G) . () = (IncAddr (G,((card F) -' 1))) . 0 proof end; Lm6: for S being COM-Struct for F, G being Program of S for f being Nat st f < (card F) - 1 holds F . f = (F ';' G) . f proof end; theorem :: COMPOS_1:24 for S being COM-Struct for F, G being Program 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 end; registration let S be COM-Struct ; let F be Program of S; let G be halt-ending Program of S; coherence F ';' G is halt-ending proof end; end; registration let S be COM-Struct ; let F be MacroInstruction of S; let G be unique-halt Program of S; coherence F ';' G is unique-halt proof end; end; definition let S be COM-Struct ; let F, G be MacroInstruction of S; :: original: ';' redefine func F ';' 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 end; end; theorem :: COMPOS_1:25 canceled; ::$CT
theorem Th16: :: COMPOS_1:26
for k being Nat
for S being COM-Struct holds Shift ((Stop S),k) = k .--> (halt S)
proof end;

registration
let S be COM-Struct ;
let F be MacroInstruction of S;
reduce F ';' (Stop S) to F;
reducibility
F ';' (Stop S) = F
proof 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 end;
end;

theorem :: 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 end;

theorem :: COMPOS_1:30
canceled;

theorem :: COMPOS_1:31
canceled;

theorem Th20: :: 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 end;

theorem Th21: :: 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 Nat : j in dom p }
proof end;

theorem Th22: :: 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 end;

theorem :: COMPOS_1:35
for S being COM-Struct
for il being Nat
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)
proof end;

definition
let S be COM-Struct ;
let i be Instruction of S;
redefine func Load i -> preProgram of S;
coherence
;
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 end;

definition
let S be COM-Struct ;
let i be Instruction of S;
func Macro i -> preProgram of S equals :: COMPOS_1:def 25
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;

registration
let S be COM-Struct ;
coherence
proof end;
end;

registration
let S be COM-Struct ;
existence
not for b1 being Program of S holds b1 is halt-free
proof 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;
cluster p +* q -> non halt-free ;
coherence
not p +* q is halt-free
proof 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 end;
end;

registration
let S be COM-Struct ;
existence
ex b1 being Program of S st
( not b1 is halt-free & not b1 is empty )
proof end;
end;

theorem :: COMPOS_1:37
canceled;

theorem :: COMPOS_1:38
canceled;

theorem :: COMPOS_1:39
canceled;

theorem :: COMPOS_1:40
canceled;

::\$CT 4
theorem Th25: :: 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 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 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 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 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 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 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 end;

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

theorem :: COMPOS_1:50
for S being COM-Struct
for x being set
for i being Instruction of S holds
( x in dom (Load i) iff x = 0 )
proof 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 end;

theorem :: COMPOS_1:52
for S being COM-Struct
for i being Instruction of S holds
( dom (Load i) = & (Load i) . 0 = i ) ;

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

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

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

theorem Th40: :: COMPOS_1:56
for S being COM-Struct
for i being Instruction of S holds card () = 2
proof end;

theorem Th41: :: COMPOS_1:57
for S being COM-Struct
for i being Instruction of S holds
( 0 in dom () & 1 in dom () )
proof end;

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

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

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

theorem Th45: :: COMPOS_1:61
for S being COM-Struct
for i being Instruction of S holds dom () = {0,1}
proof 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 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 Th48: :: 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 end;

:: from SCMPDS_7, 2011.05.27, A.T.
theorem Th49: :: COMPOS_1:65
for S being COM-Struct
for n being Nat
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 end;

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

:: from SCMPDS_5, 2011.05.27,A.T.
registration
let S be COM-Struct ;
existence
ex b1 being preProgram of S st b1 is empty
proof end;
end;

registration
let S be COM-Struct ;
coherence
for b1 being preProgram of S st b1 is empty holds
b1 is halt-free
;
end;

definition
let S be COM-Struct ;
let IT be NAT -defined the InstructionsF of S -valued Function;
redefine attr IT is halt-free means :Def14: :: 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 end;
end;

:: deftheorem COMPOS_1:def 26 :
canceled;

:: deftheorem Def14 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 ;
coherence
for b1 being non empty preProgram of S st b1 is halt-free holds
b1 is unique-halt
;
end;

theorem :: COMPOS_1:67
for S being COM-Struct
for i being Instruction of S holds rng () = {i,(halt S)}
proof 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;
coherence
proof end;
end;

registration
let S be COM-Struct ;
let I be Program of S;
let J be non halt-free Program of S;
cluster I ';' 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 ;

theorem Th55: :: COMPOS_1:71
for S being COM-Struct
for I being initial preProgram of S holds (card (stop I)) -' 1 = card I
proof end;

theorem :: COMPOS_1:72
for S being COM-Struct
for I being initial preProgram of S holds card (stop I) = (card I) + 1
proof end;

theorem Th57: :: COMPOS_1:73
for S being COM-Struct
for I being Program of S holds LastLoc (stop I) = card I
proof end;

registration
let S be COM-Struct ;
let I be Program of S;
coherence
proof end;
end;

theorem :: COMPOS_1:74
for S being COM-Struct
for n being Nat
for i being Instruction of S holds Macro (IncAddr (i,n)) = IncAddr ((),n)
proof end;

theorem :: COMPOS_1:75
for S being COM-Struct
for J, I being Program of S holds I ';' J = () ^ (IncAddr (J,((card I) -' 1)))
proof end;

theorem :: COMPOS_1:76
for S being COM-Struct
for n being Nat