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


begin

definition
attr c1 is strict ;
struct COM-Struct -> ;
aggr COM-Struct(# Instructions, haltF #) -> COM-Struct ;
sel Instructions c1 -> non empty set ;
sel haltF c1 -> Element of the Instructions of c1;
end;

definition
func Trivial-COM -> strict COM-Struct means :Def1: :: COMPOS_1:def 1
( the Instructions of it = {[0,{},{}]} & the haltF of it = [0,{},{}] );
existence
ex b1 being strict COM-Struct st
( the Instructions of b1 = {[0,{},{}]} & the haltF of b1 = [0,{},{}] )
proof end;
uniqueness
for b1, b2 being strict COM-Struct st the Instructions of b1 = {[0,{},{}]} & the haltF of b1 = [0,{},{}] & the Instructions of b2 = {[0,{},{}]} & the haltF of b2 = [0,{},{}] holds
b1 = b2 ;
end;

:: deftheorem Def1 defines Trivial-COM COMPOS_1:def 1 :
for b1 being strict COM-Struct holds
( b1 = Trivial-COM iff ( the Instructions of b1 = {[0,{},{}]} & the haltF of b1 = [0,{},{}] ) );

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

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

:: deftheorem defines halt COMPOS_1:def 2 :
for S being COM-Struct holds halt S = the haltF of S;

definition
let S be COM-Struct ;
let I be the Instructions of S -valued Function;
attr I is halt-free means :Def7: :: COMPOS_1:def 3
 not halt S in rng I;
end;

:: deftheorem Def7 defines halt-free COMPOS_1:def 3 :
for S being COM-Struct
for I being the Instructions 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 Instructions 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 func P . k -> Instruction of S;
coherence
P . k is Instruction of S
proof end;
end;

begin

notation
let x be set ;
synonym InsCode x for x `1_3 ;
synonym JumpPart x for x `2_3 ;
synonym AddressPart x for x `3_3 ;
end;

definition
let S be COM-Struct ;
attr S is standard-ins means :Def17: :: COMPOS_1:def 4
 ex X being non empty set st the Instructions of S c= [:NAT,(NAT *),(X *):];
end;

:: deftheorem Def17 defines standard-ins COMPOS_1:def 4 :
for S being COM-Struct holds
( S is standard-ins iff ex X being non empty set st the Instructions of S c= [:NAT,(NAT *),(X *):] );

registration
cluster Trivial-COM -> strict standard-ins ;
coherence
Trivial-COM is standard-ins
proof end;
end;

registration
cluster strict standard-ins for COM-Struct ;
existence
ex b1 being COM-Struct st
( b1 is standard-ins & b1 is strict )
proof end;
end;

registration
let S be standard-ins COM-Struct ;
cluster the Instructions of S -> non empty Relation-like ;
coherence
the Instructions of S is Relation-like
proof end;
end;

registration
let S be standard-ins COM-Struct ;
let x be Instruction of S;
cluster InsCode x -> natural ;
coherence
InsCode x is natural
proof end;
end;

definition
let S be standard-ins COM-Struct ;
func InsCodes S -> set equals :: COMPOS_1:def 5
 proj1 (proj1 the Instructions of S);
correctness
coherence
proj1 (proj1 the Instructions of S) is set ;
;
end;

:: deftheorem defines InsCodes COMPOS_1:def 5 :
for S being standard-ins COM-Struct holds InsCodes S = proj1 (proj1 the Instructions of S);

registration
let S be standard-ins COM-Struct ;
cluster InsCodes S -> non empty ;
coherence
not InsCodes S is empty
proof end;
end;

definition
let S be standard-ins COM-Struct ;
mode InsType of S is Element of InsCodes S;
end;

definition
let S be standard-ins COM-Struct ;
let I be Element of the Instructions of S;
:: original: InsCode
redefine func InsCode I -> InsType of S;
coherence
InsCode I is InsType of S
proof end;
end;

begin

theorem Th7: :: COMPOS_1:1
for S being standard-ins COM-Struct
for I, J being Instruction of S st InsCode I = InsCode J & JumpPart I = JumpPart J & AddressPart I = AddressPart J holds
I = J
proof end;

definition
let S be COM-Struct ;
let p be NAT -defined the Instructions of S -valued Function;
let l be set ;
pred p halts_at l means :Def19: :: COMPOS_1:def 6
( l in dom p & p . l = halt S );
end;

:: deftheorem Def19 defines halts_at COMPOS_1:def 6 :
for S being COM-Struct
for p being NAT -defined the Instructions 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 7
s . l = halt S;
compatibility
( s halts_at l iff s . l = halt S )
proof end;
end;

:: deftheorem defines halts_at COMPOS_1:def 7 :
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 Instructions 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 Instructions of S -valued )
proof end;
end;

Lm7: now
let S be COM-Struct ; :: thesis: ( <%(halt S)%> . (LastLoc <%(halt S)%>) = halt S & ( for l being Element of NAT st <%(halt S)%> . l = halt S & l in dom <%(halt S)%> holds
l = LastLoc <%(halt S)%> ) )
set F = <%(halt S)%>;
A1: dom <%(halt S)%> = {0} by FUNCOP_1:13;
then A2: card (dom <%(halt S)%>) = 1 by CARD_1:30;
A3: LastLoc <%(halt S)%> = (card <%(halt S)%>) -' 1 by AFINSQ_1:70
.= 0 by A2, XREAL_1:232 ;
hence <%(halt S)%> . (LastLoc <%(halt S)%>) = halt S by FUNCOP_1:72; :: thesis: for l being Element of NAT st <%(halt S)%> . l = halt S & l in dom <%(halt S)%> holds
l = LastLoc <%(halt S)%>
let l be Element of NAT ; :: thesis: ( <%(halt S)%> . l = halt S & l in dom <%(halt S)%> implies l = LastLoc <%(halt S)%> )
assume <%(halt S)%> . l = halt S ; :: thesis: ( l in dom <%(halt S)%> implies l = LastLoc <%(halt S)%> )
assume l in dom <%(halt S)%> ; :: thesis: l = LastLoc <%(halt S)%>
hence l = LastLoc <%(halt S)%> by A1, A3, TARSKI:def 1; :: thesis: verum
end;

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

definition
let S be COM-Struct ;
let F be non empty preProgram of S;
attr F is halt-ending means :Def25: :: COMPOS_1:def 8
F . (LastLoc F) = halt S;
attr F is unique-halt means :Def26: :: COMPOS_1:def 9
 for f being Nat st F . f = halt S & f in dom F holds
f = LastLoc F;
end;

:: deftheorem Def25 defines halt-ending COMPOS_1:def 8 :
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 Def26 defines unique-halt COMPOS_1:def 9 :
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 Instructions of S -valued Function-like T-Sequence-like finite countable V91() 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 end;
end;

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

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

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

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

theorem :: COMPOS_1:2
for ins being Element of the Instructions of Trivial-COM holds InsCode ins = 0
proof end;

begin

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

:: deftheorem defines Stop COMPOS_1:def 10 :
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 non empty Relation-like NAT -defined the Instructions of S -valued Function-like finite countable V91() initial for set ;
existence
ex b1 being preProgram of S st
( b1 is initial & not b1 is empty )
proof end;
end;

theorem Th3: :: 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:33;

Lm8: for k being natural number holds - 1 < k
;

Lm9: for k being natural number
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;

begin

definition
let S be standard-ins COM-Struct ;
let T be InsType of S;
func JumpParts T -> set equals :: COMPOS_1:def 11
 { (JumpPart I) where I is Instruction of S : InsCode I = T } ;
coherence
{ (JumpPart I) where I is Instruction of S : InsCode I = T } is set ;
end;

:: deftheorem defines JumpParts COMPOS_1:def 11 :
for S being standard-ins COM-Struct
for T being InsType of S holds JumpParts T = { (JumpPart I) where I is Instruction of S : InsCode I = T } ;

registration
let S be standard-ins COM-Struct ;
let I be Element of the Instructions of S;
cluster AddressPart I -> Relation-like Function-like ;
coherence
( AddressPart I is Function-like & AddressPart I is Relation-like )
proof end;
cluster JumpPart I -> Relation-like Function-like ;
coherence
( JumpPart I is Function-like & JumpPart I is Relation-like )
proof end;
end;

registration
let S be standard-ins COM-Struct ;
let I be Element of the Instructions of S;
cluster AddressPart I -> FinSequence-like ;
coherence
AddressPart I is FinSequence-like
proof end;
cluster JumpPart I -> FinSequence-like ;
coherence
JumpPart I is FinSequence-like
proof end;
end;

definition
let S be standard-ins COM-Struct ;
attr S is homogeneous means :Def33: :: COMPOS_1:def 12
 for I, J being Instruction of S st InsCode I = InsCode J holds
dom (JumpPart I) = dom (JumpPart J);
end;

:: deftheorem Def33 defines homogeneous COMPOS_1:def 12 :
for S being standard-ins COM-Struct holds
( S is homogeneous iff for I, J being Instruction of S st InsCode I = InsCode J holds
dom (JumpPart I) = dom (JumpPart J) );

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

definition
let S be standard-ins COM-Struct ;
let T be InsType of S;
func AddressParts T -> set equals :: COMPOS_1:def 13
 { (AddressPart I) where I is Instruction of S : InsCode I = T } ;
coherence
{ (AddressPart I) where I is Instruction of S : InsCode I = T } is set ;
end;

:: deftheorem defines AddressParts COMPOS_1:def 13 :
for S being standard-ins COM-Struct
for T being InsType of S holds AddressParts T = { (AddressPart I) where I is Instruction of S : InsCode I = T } ;

registration
let S be standard-ins COM-Struct ;
let T be InsType of S;
cluster AddressParts T -> functional ;
coherence
AddressParts T is functional
proof end;
cluster JumpParts T -> non empty functional ;
coherence
( not JumpParts T is empty & JumpParts T is functional )
proof end;
end;

definition
let S be standard-ins COM-Struct ;
attr S is regular means :Def35: :: COMPOS_1:def 14
 for I being Instruction of S
for k being set st k in dom (JumpPart I) holds
(product" (JumpParts (InsCode I))) . k = NAT ;
attr S is J/A-independent means :Def36: :: COMPOS_1:def 15
 for T being InsType of S
for f1, f2 being Function
for p being set st f1 in JumpParts T & f2 in product (product" (JumpParts T)) & [T,f1,p] in the Instructions of S holds
[T,f2,p] in the Instructions of S;
end;

:: deftheorem Def35 defines regular COMPOS_1:def 14 :
for S being standard-ins COM-Struct holds
( S is regular iff for I being Instruction of S
for k being set st k in dom (JumpPart I) holds
(product" (JumpParts (InsCode I))) . k = NAT );

:: deftheorem Def36 defines J/A-independent COMPOS_1:def 15 :
for S being standard-ins COM-Struct holds
( S is J/A-independent iff for T being InsType of S
for f1, f2 being Function
for p being set st f1 in JumpParts T & f2 in product (product" (JumpParts T)) & [T,f1,p] in the Instructions of S holds
[T,f2,p] in the Instructions of S );

theorem Th86: :: COMPOS_1:6
for T being InsType of Trivial-COM holds JumpParts T = {0}
proof end;

Lm10: for I being Instruction of Trivial-COM holds JumpPart I = 0
proof end;

Lm11: for T being InsType of Trivial-COM holds JumpParts T = {0}
proof end;

registration
cluster Trivial-COM -> strict homogeneous regular J/A-independent ;
coherence
( Trivial-COM is homogeneous & Trivial-COM is regular & Trivial-COM is J/A-independent )
proof end;
end;

registration
cluster strict standard-ins homogeneous regular J/A-independent for COM-Struct ;
existence
ex b1 being strict standard-ins COM-Struct st
( b1 is regular & b1 is J/A-independent & b1 is homogeneous )
proof end;
end;

registration
let S be standard-ins homogeneous regular COM-Struct ;
let T be InsType of S;
cluster JumpParts T -> with_common_domain ;
coherence
JumpParts T is with_common_domain
proof end;
end;

registration
let S be standard-ins homogeneous regular COM-Struct ;
let I be Instruction of S;
cluster JumpPart I -> NAT -valued for Function;
coherence
for b1 being Function st b1 = JumpPart I holds
b1 is NAT -valued
proof end;
end;

registration
let S be standard-ins homogeneous regular J/A-independent COM-Struct ;
let T be InsType of S;
cluster JumpParts T -> product-like ;
coherence
JumpParts T is product-like
proof end;
end;

registration
cluster Trivial-COM -> strict regular J/A-independent ;
coherence
( Trivial-COM is regular & Trivial-COM is J/A-independent ) ;
end;

registration
let S be standard-ins homogeneous COM-Struct ;
let T be InsType of S;
cluster JumpParts T -> with_common_domain ;
coherence
JumpParts T is with_common_domain
proof end;
end;

theorem :: COMPOS_1:7
for S being standard-ins homogeneous regular COM-Struct
for I being Instruction of S
for x being set st x in dom (JumpPart I) holds
(JumpPart I) . x is Element of NAT
proof end;

registration
let S be COM-Struct ;
cluster non empty trivial Relation-like NAT -defined the Instructions 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 end;
end;

definition
let S be standard-ins COM-Struct ;
let I be Instruction of S;
attr I is ins-loc-free means :Def37: :: COMPOS_1:def 16
 JumpPart I is empty ;
end;

:: deftheorem Def37 defines ins-loc-free COMPOS_1:def 16 :
for S being standard-ins COM-Struct
for I being Instruction of S holds
( I is ins-loc-free iff JumpPart I is empty );

Lm12: now
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;

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 Instructions of S -valued & Stop S is trivial ) ;
end;

theorem Th89: :: COMPOS_1:8
for S being COM-Struct
for F being pre-Macro of S st card F = 1 holds
F = Stop S
proof end;

Lm13: for S being COM-Struct holds (card (Stop S)) -' 1 = 0
proof end;

theorem Th90: :: COMPOS_1:9
for S being COM-Struct holds LastLoc (Stop S) = 0
proof 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 end;
end;

begin

registration
let S be standard-ins homogeneous regular J/A-independent COM-Struct ;
let I be Element of the Instructions of S;
cluster JumpPart I -> natural-valued for Function;
coherence
for b1 being Function st b1 = JumpPart I holds
b1 is natural-valued ;
end;

definition
let S be standard-ins homogeneous regular J/A-independent COM-Struct ;
let I be Element of the Instructions of S;
let k be natural number ;
func IncAddr (I,k) -> Instruction of S means :Def38: :: COMPOS_1:def 17
( InsCode it = InsCode I & AddressPart it = AddressPart I & JumpPart it = k + (JumpPart I) );
existence
ex b1 being Instruction of S st
( InsCode b1 = InsCode I & AddressPart b1 = AddressPart I & JumpPart b1 = k + (JumpPart I) )
proof end;
uniqueness
for b1, b2 being Instruction of S st InsCode b1 = InsCode I & AddressPart b1 = AddressPart I & JumpPart b1 = k + (JumpPart I) & InsCode b2 = InsCode I & AddressPart b2 = AddressPart I & JumpPart b2 = k + (JumpPart I) holds
b1 = b2 by Th7;
end;

:: deftheorem Def38 defines IncAddr COMPOS_1:def 17 :
for S being standard-ins homogeneous regular J/A-independent COM-Struct
for I being Element of the Instructions of S
for k being natural number
for b4 being Instruction of S holds
( b4 = IncAddr (I,k) iff ( InsCode b4 = InsCode I & AddressPart b4 = AddressPart I & JumpPart b4 = k + (JumpPart I) ) );

theorem Th91: :: COMPOS_1:10
for S being standard-ins homogeneous regular J/A-independent COM-Struct
for I being Element of the Instructions of S holds IncAddr (I,0) = I
proof end;

theorem Th92: :: COMPOS_1:11
for k being natural number
for S being standard-ins homogeneous regular J/A-independent COM-Struct
for I being Instruction of S st I is ins-loc-free holds
IncAddr (I,k) = I
proof end;

definition
let S be standard-ins COM-Struct ;
attr S is proper-halt means :Def39: :: COMPOS_1:def 18
 halt S is ins-loc-free ;
end;

:: deftheorem Def39 defines proper-halt COMPOS_1:def 18 :
for S being standard-ins COM-Struct holds
( S is proper-halt iff halt S is ins-loc-free );

registration
cluster Trivial-COM -> strict proper-halt ;
coherence
Trivial-COM is proper-halt
proof end;
end;

registration
cluster standard-ins homogeneous regular J/A-independent proper-halt for COM-Struct ;
existence
ex b1 being standard-ins COM-Struct st
( b1 is proper-halt & b1 is regular & b1 is homogeneous & b1 is J/A-independent )
proof end;
end;

registration
let S be standard-ins proper-halt COM-Struct ;
cluster halt S -> ins-loc-free ;
coherence
halt S is ins-loc-free by Def39;
end;

registration
let S be standard-ins proper-halt COM-Struct ;
cluster ins-loc-free for Element of the Instructions of S;
existence
ex b1 being Instruction of S st b1 is ins-loc-free
proof end;
end;

registration
let S be standard-ins proper-halt COM-Struct ;
let I be ins-loc-free Instruction of S;
cluster JumpPart I -> empty ;
coherence
JumpPart I is empty by Def37;
end;

theorem :: COMPOS_1:12
for k being natural number
for S being standard-ins homogeneous regular J/A-independent COM-Struct
for I being Instruction of S holds JumpParts (InsCode I) = JumpParts (InsCode (IncAddr (I,k)))
proof end;

theorem Th95: :: COMPOS_1:13
for S being standard-ins homogeneous regular J/A-independent COM-Struct
for I, J being Instruction of S st ex k being natural number st IncAddr (I,k) = IncAddr (J,k) holds
I = J
proof end;

theorem Th96: :: COMPOS_1:14
for k being natural number
for S being standard-ins homogeneous regular J/A-independent proper-halt COM-Struct
for I being Instruction of S st IncAddr (I,k) = halt S holds
I = halt S
proof end;

theorem Th97: :: COMPOS_1:15
for k, m being natural number
for S being standard-ins homogeneous regular J/A-independent COM-Struct
for I being Instruction of S holds IncAddr ((IncAddr (I,k)),m) = IncAddr (I,(k + m))
proof end;

definition
let S be standard-ins homogeneous regular J/A-independent COM-Struct ;
let p be NAT -defined the Instructions of S -valued finite Function;
let k be natural number ;
A1: dom p c= NAT by RELAT_1:def 18;
func IncAddr (p,k) -> NAT -defined the Instructions of S -valued finite Function means :Def40: :: COMPOS_1:def 19
( dom it = dom p & ( for m being natural number st m in dom p holds
it . m = IncAddr ((p /. m),k) ) );
existence
ex b1 being NAT -defined the Instructions of S -valued finite Function st
( dom b1 = dom p & ( for m being natural number st m in dom p holds
b1 . m = IncAddr ((p /. m),k) ) )
proof end;
uniqueness
for b1, b2 being NAT -defined the Instructions of S -valued finite Function st dom b1 = dom p & ( for m being natural number st m in dom p holds
b1 . m = IncAddr ((p /. m),k) ) & dom b2 = dom p & ( for m being natural number st m in dom p holds
b2 . m = IncAddr ((p /. m),k) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def40 defines IncAddr COMPOS_1:def 19 :
for S being standard-ins homogeneous regular J/A-independent COM-Struct
for p being NAT -defined the Instructions of b1 -valued finite Function
for k being natural number
for b4 being NAT -defined the Instructions of b1 -valued finite Function holds
( b4 = IncAddr (p,k) iff ( dom b4 = dom p & ( for m being natural number st m in dom p holds
b4 . m = IncAddr ((p /. m),k) ) ) );

registration
let S be standard-ins homogeneous regular J/A-independent COM-Struct ;
let F be NAT -defined the Instructions of S -valued finite Function;
let k be natural number ;
cluster IncAddr (F,k) -> NAT -defined the Instructions of S -valued finite ;
coherence
( IncAddr (F,k) is NAT -defined & IncAddr (F,k) is the Instructions of S -valued ) ;
end;

registration
let S be standard-ins homogeneous regular J/A-independent COM-Struct ;
let F be empty NAT -defined the Instructions of S -valued finite Function;
let k be natural number ;
cluster IncAddr (F,k) -> empty NAT -defined the Instructions of S -valued finite ;
coherence
IncAddr (F,k) is empty
proof end;
end;

registration
let S be standard-ins homogeneous regular J/A-independent COM-Struct ;
let F be non empty NAT -defined the Instructions of S -valued finite Function;
let k be natural number ;
cluster IncAddr (F,k) -> non empty NAT -defined the Instructions of S -valued finite ;
coherence
not IncAddr (F,k) is empty
proof end;
end;

registration
let S be standard-ins homogeneous regular J/A-independent COM-Struct ;
let F be NAT -defined the Instructions of S -valued finite initial Function;
let k be natural number ;
cluster IncAddr (F,k) -> NAT -defined the Instructions of S -valued finite initial ;
coherence
IncAddr (F,k) is initial
proof end;
end;

theorem Th98: :: COMPOS_1:16
for S being standard-ins homogeneous regular J/A-independent COM-Struct
for F being NAT -defined the Instructions of b1 -valued finite Function holds IncAddr (F,0) = F
proof end;

theorem Th99: :: COMPOS_1:17
for k, m being natural number
for S being standard-ins homogeneous regular J/A-independent COM-Struct
for F being NAT -defined the Instructions of b3 -valued finite Function holds IncAddr ((IncAddr (F,k)),m) = IncAddr (F,(k + m))
proof end;

definition
let S be standard-ins homogeneous regular J/A-independent COM-Struct ;
let p be NAT -defined the Instructions of S -valued finite Function;
let k be Nat;
func Reloc (p,k) -> NAT -defined the Instructions of S -valued finite Function equals :: COMPOS_1:def 20
 IncAddr ((Shift (p,k)),k);
coherence
IncAddr ((Shift (p,k)),k) is NAT -defined the Instructions of S -valued finite Function ;
end;

:: deftheorem defines Reloc COMPOS_1:def 20 :
for S being standard-ins homogeneous regular J/A-independent COM-Struct
for p being NAT -defined the Instructions of b1 -valued finite Function
for k being Nat holds Reloc (p,k) = IncAddr ((Shift (p,k)),k);

theorem Th100: :: COMPOS_1:18
for S being standard-ins homogeneous regular J/A-independent COM-Struct
for F being non empty initial preProgram of S
for G being non empty NAT -defined the Instructions of b1 -valued finite Function holds dom (CutLastLoc F) misses dom (Shift ((IncAddr (G,((card F) -' 1))),((card F) -' 1)))
proof end;

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

definition
let S be standard-ins homogeneous regular J/A-independent COM-Struct ;
let F, G be non empty preProgram of S;
func F ';' G -> preProgram of S equals :: COMPOS_1:def 21
(CutLastLoc F) +* (Shift ((IncAddr (G,((card F) -' 1))),((card F) -' 1)));
coherence
(CutLastLoc F) +* (Shift ((IncAddr (G,((card F) -' 1))),((card F) -' 1))) is preProgram of S ;
end;

:: deftheorem defines ';' COMPOS_1:def 21 :
for S being standard-ins homogeneous regular J/A-independent COM-Struct
for F, G being non empty preProgram of S holds F ';' G = (CutLastLoc F) +* (Shift ((IncAddr (G,((card F) -' 1))),((card F) -' 1)));

registration
let S be standard-ins homogeneous regular J/A-independent COM-Struct ;
let F, G be non empty NAT -defined the Instructions of S -valued finite Function;
cluster F ';' G -> non empty ;
coherence
( not F ';' G is empty & F ';' G is the Instructions of S -valued & F ';' G is NAT -defined ) ;
end;

theorem Th102: :: COMPOS_1:20
for S being standard-ins homogeneous regular J/A-independent COM-Struct
for F being non empty initial preProgram of S
for G being non empty NAT -defined the Instructions of b1 -valued finite Function holds
( card (F ';' G) = ((card F) + (card G)) - 1 & card (F ';' G) = ((card F) + (card G)) -' 1 )
proof end;

registration
let S be standard-ins homogeneous regular J/A-independent COM-Struct ;
let F, G be non empty initial preProgram of S;
cluster F ';' G -> initial ;
coherence
F ';' G is initial
proof end;
end;

theorem :: COMPOS_1:21
for S being standard-ins homogeneous regular J/A-independent COM-Struct
for F, G being non empty initial preProgram of S holds dom F c= dom (F ';' G)
proof end;

registration
let S be standard-ins homogeneous regular J/A-independent COM-Struct ;
let F, G be non empty initial preProgram of S;
cluster F ';' G -> non empty initial ;
coherence
( F ';' G is initial & not F ';' G is empty ) ;
end;

theorem Th104: :: COMPOS_1:22
for S being standard-ins homogeneous regular J/A-independent COM-Struct
for F, G being non empty initial preProgram of S holds CutLastLoc F c= CutLastLoc (F ';' G)
proof end;

theorem Th105: :: COMPOS_1:23
for S being standard-ins homogeneous regular J/A-independent COM-Struct
for F, G being non empty initial preProgram of S holds (F ';' G) . (LastLoc F) = (IncAddr (G,((card F) -' 1))) . 0
proof end;

theorem :: COMPOS_1:24
for S being standard-ins homogeneous regular J/A-independent 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 end;

registration
let S be standard-ins homogeneous regular J/A-independent proper-halt COM-Struct ;
let F be non empty NAT -defined the Instructions of S -valued finite initial Function;
let G be non empty NAT -defined the Instructions of S -valued finite initial halt-ending Function;
cluster F ';' G -> halt-ending ;
coherence
F ';' G is halt-ending
proof end;
end;

registration
let S be standard-ins homogeneous regular J/A-independent proper-halt COM-Struct ;
let F, G be non empty NAT -defined the Instructions of S -valued finite initial halt-ending unique-halt Function;
cluster F ';' G -> unique-halt ;
coherence
F ';' G is unique-halt
proof end;
end;

definition
let S be standard-ins homogeneous regular J/A-independent proper-halt COM-Struct ;
let F, G be pre-Macro of S;
:: original: ';'
redefine func F ';' G -> pre-Macro of S;
coherence
F ';' G is pre-Macro of S ;
end;

theorem Th107: :: COMPOS_1:25
for k being natural number
for S being standard-ins homogeneous regular J/A-independent proper-halt COM-Struct holds IncAddr ((Stop S),k) = Stop S
proof end;

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

theorem Th109: :: COMPOS_1:27
for S being standard-ins homogeneous regular J/A-independent proper-halt COM-Struct
for F being pre-Macro of S holds F ';' (Stop S) = F
proof end;

theorem Th110: :: COMPOS_1:28
for S being standard-ins homogeneous regular J/A-independent COM-Struct
for F being pre-Macro of S holds (Stop S) ';' F = F
proof end;

theorem :: COMPOS_1:29
for S being standard-ins homogeneous regular J/A-independent proper-halt COM-Struct
for F, G, H being pre-Macro of S holds (F ';' G) ';' H = F ';' (G ';' H)
proof end;

theorem :: COMPOS_1:30
for S being standard-ins homogeneous regular COM-Struct
for I being Instruction of S
for x being set st x in dom (JumpPart I) holds
(JumpPart I) . x in (product" (JumpParts (InsCode I))) . x
proof end;

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

theorem :: COMPOS_1:32
for T being InsType of Trivial-COM holds JumpParts T = {0} by Lm11;

begin

theorem Th117: :: COMPOS_1:33
for S being standard-ins homogeneous regular J/A-independent COM-Struct
for k being Nat
for p being NAT -defined the Instructions of b1 -valued finite Function holds dom (Reloc (p,k)) = { (j + k) where j is Element of NAT : j in dom p }
proof end;

theorem Th121: :: COMPOS_1:34
for S being standard-ins homogeneous regular J/A-independent COM-Struct
for i, j being Nat
for p being NAT -defined the Instructions of b1 -valued finite Function holds Shift ((IncAddr (p,i)),j) = IncAddr ((Shift (p,j)),i)
proof end;

theorem :: COMPOS_1:35
for il being Nat
for S being standard-ins homogeneous regular J/A-independent COM-Struct
for g being NAT -defined the Instructions 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 end;

begin

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 22
I ^ (Stop S);
coherence
I ^ (Stop S) is preProgram of S ;
end;

:: deftheorem defines stop COMPOS_1:def 22 :
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;

begin

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

:: deftheorem defines Macro COMPOS_1:def 23 :
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 end;
end;

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

registration
let S be COM-Struct ;
let p be NAT -defined the Instructions of S -valued Function;
let q be NAT -defined the Instructions 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 standard-ins homogeneous regular J/A-independent proper-halt COM-Struct ;
let p be NAT -defined the Instructions of S -valued finite non halt-free Function;
let k be Nat;
cluster Reloc (p,k) -> NAT -defined the Instructions of S -valued finite non halt-free ;
coherence
not Reloc (p,k) is halt-free
proof end;
end;

registration
let S be COM-Struct ;
cluster non empty Relation-like NAT -defined the Instructions of S -valued Function-like T-Sequence-like finite countable V91() initial non halt-free for set ;
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;

theorem Th153: :: COMPOS_1:41
for n being Nat
for S being standard-ins homogeneous regular J/A-independent COM-Struct
for p, q being NAT -defined the Instructions 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 standard-ins homogeneous regular J/A-independent COM-Struct
for p, q being NAT -defined the Instructions 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 standard-ins homogeneous regular J/A-independent COM-Struct
for p being NAT -defined the Instructions 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 standard-ins homogeneous regular J/A-independent COM-Struct
for P, Q being NAT -defined the Instructions of b1 -valued finite Function
for k being Nat st P c= Q holds
Reloc (P,k) c= Reloc (Q,k)
proof end;

theorem :: COMPOS_1:45
for S being standard-ins homogeneous regular J/A-independent COM-Struct
for P being preProgram of S holds Reloc (P,0) = P
proof end;

theorem :: COMPOS_1:46
for il being Nat
for S being standard-ins homogeneous regular J/A-independent 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 standard-ins homogeneous regular J/A-independent proper-halt COM-Struct
for i being Instruction of S
for f being Function of the Instructions of S, the Instructions of S st f = (id the Instructions of S) +* ((halt S) .--> i) holds
for s being NAT -defined the Instructions of b2 -valued finite Function holds IncAddr ((f * s),n) = ((id the Instructions of S) +* ((halt S) .--> (IncAddr (i,n)))) * (IncAddr (s,n))
proof end;

theorem :: COMPOS_1:48
for S being standard-ins homogeneous regular J/A-independent 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 m being Nat
for S being standard-ins homogeneous regular J/A-independent COM-Struct
for I being preProgram of S holds card (Reloc (I,m)) = card I
proof 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 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) = {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 end;

theorem Th54: :: COMPOS_1:54
for S being COM-Struct
for i being Instruction of S holds card (Load i) = 1
proof 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 end;

theorem Th56: :: COMPOS_1:56
for S being COM-Struct
for i being Instruction of S holds card (Macro i) = 2
proof 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 end;

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

theorem :: COMPOS_1:59
for S being COM-Struct
for i being Instruction of S holds (Macro i) . 1 = halt S
proof 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 end;

theorem :: COMPOS_1:61
for S being COM-Struct
for i being Instruction of S holds dom (Macro i) = {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 Th63: :: 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 end;

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

definition
let S be COM-Struct ;
let i be Instruction of S;
attr i is No-StopCode means :: COMPOS_1:def 24
i <> halt S;
end;

:: deftheorem defines No-StopCode COMPOS_1:def 24 :
for S being COM-Struct
for i being Instruction of S holds
( i is No-StopCode iff i <> halt S );

registration
let S be COM-Struct ;
cluster empty Relation-like NAT -defined the Instructions of S -valued Function-like finite countable V91() for set ;
existence
ex b1 being preProgram of S st b1 is empty
proof end;
end;

registration
let S be COM-Struct ;
cluster empty Relation-like NAT -defined the Instructions 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 end;
end;

definition
let S be COM-Struct ;
let IT be NAT -defined the Instructions of S -valued Function;
redefine attr IT is halt-free means :Def25: :: COMPOS_1:def 25
 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 Def25 defines halt-free COMPOS_1:def 25 :
for S being COM-Struct
for IT being NAT -defined the Instructions 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 Instructions 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 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 end;

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

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