:: by Andrzej Trybulec

::

:: Received May 20, 2010

:: Copyright (c) 2010-2021 Association of Mizar Users

definition

attr c_{1} is strict ;

struct COM-Struct -> ;

aggr COM-Struct(# InstructionsF #) -> COM-Struct ;

sel InstructionsF c_{1} -> Instructions;

end;
struct COM-Struct -> ;

aggr COM-Struct(# InstructionsF #) -> COM-Struct ;

sel InstructionsF c

definition

ex b_{1} being strict COM-Struct st the InstructionsF of b_{1} = {[0,{},{}]}

for b_{1}, b_{2} being strict COM-Struct st the InstructionsF of b_{1} = {[0,{},{}]} & the InstructionsF of b_{2} = {[0,{},{}]} holds

b_{1} = b_{2}
;

end;

::$CD 7

func Trivial-COM -> strict COM-Struct means :Def1: :: COMPOS_1:def 8

the InstructionsF of it = {[0,{},{}]};

existence the InstructionsF of it = {[0,{},{}]};

ex b

proof end;

uniqueness for b

b

:: deftheorem Def1 defines Trivial-COM COMPOS_1:def 8 :

for b_{1} being strict COM-Struct holds

( b_{1} = Trivial-COM iff the InstructionsF of b_{1} = {[0,{},{}]} );

for b

( b

:: deftheorem defines halt COMPOS_1:def 10 :

for S being COM-Struct holds halt S = halt the InstructionsF of S;

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.

:: halt SCM-Instr, zamiast halt SCM, zreszta wyrzucenie jej

:: spowodowaloby problemy z typowaniem.

:: deftheorem Def3 defines halt-free COMPOS_1:def 11 :

for S being COM-Struct

for I being the InstructionsF of b_{1} -valued Function holds

( I is halt-free iff not halt S in rng I );

for S being COM-Struct

for I being the InstructionsF of b

( I is halt-free iff not halt S in rng I );

definition

let S be COM-Struct ;

mode Instruction-Sequence of S is the InstructionsF of S -valued ManySortedSet of NAT ;

end;
mode Instruction-Sequence of S is the InstructionsF of S -valued ManySortedSet of NAT ;

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

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

definition
end;

:: deftheorem defines halts_at COMPOS_1:def 12 :

for S being COM-Struct

for p being NAT -defined the InstructionsF of b_{1} -valued Function

for l being set holds

( p halts_at l iff ( l in dom p & p . l = halt S ) );

for S being COM-Struct

for p being NAT -defined the InstructionsF of b

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;

compatibility

( s halts_at l iff s . l = halt S )

end;
let s be Instruction-Sequence of S;

let l be Nat;

compatibility

( s halts_at l iff s . l = halt S )

proof 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 );

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

registration

let S be COM-Struct ;

ex b_{1} being Function st

( b_{1} is initial & b_{1} is 1 -element & b_{1} is NAT -defined & b_{1} is the InstructionsF of S -valued )

end;
cluster Relation-like NAT -defined the InstructionsF of S -valued Function-like 1 -element initial for set ;

existence ex b

( b

proof end;

definition

let S be COM-Struct ;

mode preProgram of S is NAT -defined the InstructionsF of S -valued finite Function;

end;
mode preProgram of S is NAT -defined the InstructionsF of S -valued finite Function;

:: 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 . (LastLoc F) = halt S );

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

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 ;

for b_{1} being non empty preProgram of S st b_{1} is halt-ending holds

not b_{1} is halt-free

end;
cluster non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like finite halt-ending -> non empty non halt-free for set ;

coherence for b

not b

proof end;

registration

let S be COM-Struct ;

ex b_{1} being preProgram of S st

( b_{1} is trivial & b_{1} is initial & not b_{1} is empty )

end;
cluster non empty trivial Relation-like NAT -defined the InstructionsF of S -valued Function-like finite initial for set ;

existence ex b

( b

proof end;

::$CT

:: registration

:: let S be COM-Struct;

:: cluster Stop S -> initial non empty;

:: coherence;

:: end;

:: 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;
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 ) ;

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

registration

let S be COM-Struct ;

ex b_{1} being Program of S st

( b_{1} is halt-ending & b_{1} is unique-halt & b_{1} is trivial )

end;
cluster non empty trivial Relation-like NAT -defined the InstructionsF of S -valued Function-like V31() finite initial halt-ending unique-halt for set ;

existence ex b

( b

proof end;

definition
end;

registration

let S be COM-Struct ;

ex b_{1} being preProgram of S st

( b_{1} is initial & not b_{1} is empty )

end;
cluster non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like finite initial for set ;

existence ex b

( b

proof end;

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;

registration

let S be COM-Struct ;

for b_{1} being non empty preProgram of S st b_{1} is trivial holds

b_{1} is unique-halt

end;
cluster non empty trivial Relation-like NAT -defined the InstructionsF of S -valued Function-like finite -> non empty unique-halt for set ;

coherence for b

b

proof end;

::$CT

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;

ex b_{1} being NAT -defined the InstructionsF of S -valued finite Function st

( dom b_{1} = dom p & ( for m being Nat st m in dom p holds

b_{1} . m = IncAddr ((p /. m),k) ) )

for b_{1}, b_{2} being NAT -defined the InstructionsF of S -valued finite Function st dom b_{1} = dom p & ( for m being Nat st m in dom p holds

b_{1} . m = IncAddr ((p /. m),k) ) & dom b_{2} = dom p & ( for m being Nat st m in dom p holds

b_{2} . m = IncAddr ((p /. m),k) ) holds

b_{1} = b_{2}

end;
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 ( dom it = dom p & ( for m being Nat st m in dom p holds

it . m = IncAddr ((p /. m),k) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def9 defines IncAddr COMPOS_1:def 21 :

for S being COM-Struct

for p being preProgram of S

for k being Nat

for b_{4} being NAT -defined the InstructionsF of b_{1} -valued finite Function holds

( b_{4} = IncAddr (p,k) iff ( dom b_{4} = dom p & ( for m being Nat st m in dom p holds

b_{4} . m = IncAddr ((p /. m),k) ) ) );

for S being COM-Struct

for p being preProgram of S

for k being Nat

for b

( b

b

registration

let S be COM-Struct ;

let F be preProgram of S;

let k be Nat;

coherence

( IncAddr (F,k) is NAT -defined & IncAddr (F,k) is the InstructionsF of S -valued ) ;

end;
let F be preProgram of S;

let k be Nat;

coherence

( IncAddr (F,k) is NAT -defined & IncAddr (F,k) is the InstructionsF of S -valued ) ;

registration

let S be COM-Struct ;

let F be empty preProgram of S;

let k be Nat;

coherence

IncAddr (F,k) is empty

end;
let F be empty preProgram of S;

let k be Nat;

coherence

IncAddr (F,k) is empty

proof end;

registration

let S be COM-Struct ;

let F be non empty preProgram of S;

let k be Nat;

coherence

not IncAddr (F,k) is empty

end;
let F be non empty preProgram of S;

let k be Nat;

coherence

not IncAddr (F,k) is empty

proof end;

registration

let S be COM-Struct ;

let F be initial preProgram of S;

let k be Nat;

coherence

IncAddr (F,k) is initial

end;
let F be initial preProgram of S;

let k be Nat;

coherence

IncAddr (F,k) is initial

proof end;

::$CT 6

registration
end;

::$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))

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;

Shift ((IncAddr (p,k)),k) is NAT -defined the InstructionsF of S -valued finite Function ;

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

Shift ((IncAddr (p,k)),k) is NAT -defined the InstructionsF of S -valued finite Function ;

:: 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);

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 (CutLastLoc F) misses dom (Reloc (G,((card F) -' 1)))

for F being Program of S

for G being non empty preProgram of S holds dom (CutLastLoc F) 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 (CutLastLoc F) holds

(CutLastLoc F) . I <> halt S

for F being unique-halt Program of S

for I being Nat st I in dom (CutLastLoc F) holds

(CutLastLoc F) . I <> halt S

proof end;

definition

let S be COM-Struct ;

let F, G be non empty preProgram of S;

(CutLastLoc F) +* (Reloc (G,((card F) -' 1))) is preProgram of S ;

end;
let F, G be non empty preProgram of S;

func F ';' G -> preProgram of S equals :: COMPOS_1:def 23

(CutLastLoc F) +* (Reloc (G,((card F) -' 1)));

coherence (CutLastLoc F) +* (Reloc (G,((card F) -' 1)));

(CutLastLoc F) +* (Reloc (G,((card F) -' 1))) is preProgram of S ;

:: 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)));

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 preProgram of S;

coherence

( not F ';' G is empty & F ';' G is the InstructionsF of S -valued & F ';' G is NAT -defined ) ;

end;
let F, G be non empty preProgram of S;

coherence

( not F ';' G is empty & F ';' G is the InstructionsF of S -valued & F ';' G is NAT -defined ) ;

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 )

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

registration

let S be COM-Struct ;

let F, G be Program of S;

coherence

( F ';' G is initial & not F ';' G is empty ) ;

end;
let F, G be Program of S;

coherence

( F ';' G is initial & not F ';' G is empty ) ;

theorem Th14: :: COMPOS_1:23

for S being COM-Struct

for F, G being Program of S holds (F ';' G) . (LastLoc F) = (IncAddr (G,((card F) -' 1))) . 0

for F, G being Program of S holds (F ';' G) . (LastLoc F) = (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

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

end;
let F be Program of S;

let G be halt-ending Program of S;

coherence

F ';' G is halt-ending

proof 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

end;
let F be MacroInstruction of S;

let G be unique-halt Program of S;

coherence

F ';' G is unique-halt

proof 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;
let F, G be MacroInstruction of S;

:: original: ';'

redefine func F ';' G -> MacroInstruction of S;

coherence

F ';' G is MacroInstruction of S ;

registration
end;

::$CT

registration
end;

theorem :: COMPOS_1:27

registration
end;

theorem :: COMPOS_1:28

theorem :: COMPOS_1:29

for S being COM-Struct

for F, G, H being MacroInstruction of S holds (F ';' G) ';' H = F ';' (G ';' H)

for F, G, H being MacroInstruction of S holds (F ';' G) ';' H = F ';' (G ';' H)

proof end;

theorem Th20: :: COMPOS_1:32

for S being COM-Struct

for k being Nat

for p being NAT -defined the InstructionsF of b_{1} -valued finite Function holds dom (Reloc (p,k)) = dom (Shift (p,k))

for k being Nat

for p being NAT -defined the InstructionsF of b

proof end;

theorem Th21: :: COMPOS_1:33

for S being COM-Struct

for k being Nat

for p being NAT -defined the InstructionsF of b_{1} -valued finite Function holds dom (Reloc (p,k)) = { (j + k) where j is Nat : j in dom p }

for k being Nat

for p being NAT -defined the InstructionsF of b

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 b_{1} -valued finite Function holds Shift ((IncAddr (p,i)),j) = IncAddr ((Shift (p,j)),i)

for i, j being Nat

for p being NAT -defined the InstructionsF of b

proof end;

theorem :: COMPOS_1:35

for S being COM-Struct

for il being Nat

for g being NAT -defined the InstructionsF of b_{1} -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)

for il being Nat

for g being NAT -defined the InstructionsF of b

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;

:: original: Load

redefine func Load i -> preProgram of S;

coherence

Load is preProgram of S ;

end;
let i be Instruction of S;

:: original: Load

redefine func Load i -> preProgram of S;

coherence

Load is preProgram of S ;

definition
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);

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;

correctness

coherence

( stop I is initial & not stop I is empty );

;

end;
let I be initial preProgram of S;

correctness

coherence

( stop I is initial & not stop I is empty );

;

theorem :: COMPOS_1:36

definition
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);

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;

coherence

( Macro i is initial & not Macro i is empty ) ;

end;
let i be Instruction of S;

coherence

( Macro i is initial & not Macro i is empty ) ;

registration
end;

registration

let S be COM-Struct ;

not for b_{1} being Program of S holds b_{1} is halt-free

end;
cluster non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like V31() finite initial non halt-free for set ;

existence not for b

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

coherence

not p +* q is halt-free

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

coherence

not p +* q is halt-free

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

coherence

not Reloc (p,k) is halt-free

end;
let p be NAT -defined the InstructionsF of S -valued finite non halt-free Function;

let k be Nat;

coherence

not Reloc (p,k) is halt-free

proof end;

registration

let S be COM-Struct ;

ex b_{1} being Program of S st

( not b_{1} is halt-free & not b_{1} is empty )

end;
cluster non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like V31() finite initial non halt-free for set ;

existence ex b

( not b

proof end;

::$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 b_{2} -valued finite Function holds IncAddr ((p +* q),n) = (IncAddr (p,n)) +* (IncAddr (q,n))

for S being COM-Struct

for p, q being NAT -defined the InstructionsF of b

proof end;

theorem :: COMPOS_1:42

for S being COM-Struct

for p, q being NAT -defined the InstructionsF of b_{1} -valued finite Function

for k being Nat holds Reloc ((p +* q),k) = (Reloc (p,k)) +* (Reloc (q,k))

for p, q being NAT -defined the InstructionsF of b

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 b_{1} -valued finite Function

for m, n being Nat holds Reloc ((Reloc (p,m)),n) = Reloc (p,(m + n))

for p being NAT -defined the InstructionsF of b

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 b_{1} -valued finite Function

for k being Nat st P c= Q holds

Reloc (P,k) c= Reloc (Q,k)

for P, Q being NAT -defined the InstructionsF of b

for k being Nat st P c= Q holds

Reloc (P,k) c= Reloc (Q,k)

proof end;

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)) )

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 b_{2} -valued finite Function holds IncAddr ((f * s),n) = ((id the InstructionsF of S) +* ((halt S) .--> (IncAddr (i,n)))) * (IncAddr (s,n))

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 b

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

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 ) by TARSKI:def 1;

for x being set

for i being Instruction of S holds

( x in dom (Load i) iff x = 0 ) by TARSKI:def 1;

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

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

theorem Th41: :: 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) )

for i being Instruction of S holds

( 0 in dom (Macro i) & 1 in dom (Macro i) )

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 (Macro i) iff ( x = 0 or x = 1 ) )

for x being set

for i being Instruction of S holds

( x in dom (Macro i) iff ( x = 0 or x = 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)

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;

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 )

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)

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

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 ;

ex b_{1} being preProgram of S st b_{1} is empty

end;
cluster empty Relation-like NAT -defined the InstructionsF of S -valued Function-like finite for set ;

existence ex b

proof end;

registration

let S be COM-Struct ;

for b_{1} being preProgram of S st b_{1} is empty holds

b_{1} is halt-free
;

end;
cluster empty Relation-like NAT -defined the InstructionsF of S -valued Function-like finite -> halt-free for set ;

coherence for b

b

definition

let S be COM-Struct ;

let IT be NAT -defined the InstructionsF of S -valued Function;

( IT is halt-free iff for x being Nat st x in dom IT holds

IT . x <> halt S )

end;
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 for x being Nat st x in dom IT holds

IT . x <> halt S;

( IT is halt-free iff for x being Nat st x in dom IT holds

IT . x <> halt S )

proof end;

:: deftheorem Def14 defines halt-free COMPOS_1:def 27 :

for S being COM-Struct

for IT being NAT -defined the InstructionsF of b_{1} -valued Function holds

( IT is halt-free iff for x being Nat st x in dom IT holds

IT . x <> halt S );

for S being COM-Struct

for IT being NAT -defined the InstructionsF of b

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

for b_{1} being non empty preProgram of S st b_{1} is halt-free holds

b_{1} is unique-halt
;

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

b

registration

let S be COM-Struct ;

let p be initial preProgram of S;

reducibility

CutLastLoc (stop p) = p by AFINSQ_2:83;

end;
let p be initial preProgram of S;

reducibility

CutLastLoc (stop p) = p by AFINSQ_2:83;

theorem :: COMPOS_1:68

registration

let S be COM-Struct ;

let p be initial halt-free preProgram of S;

coherence

stop p is unique-halt

end;
let p be initial halt-free preProgram of S;

coherence

stop p is unique-halt

proof end;

registration

let S be COM-Struct ;

let I be Program of S;

let J be non halt-free Program of S;

coherence

not I ';' J is halt-free ;

end;
let I be Program of S;

let J be non halt-free Program of S;

coherence

not I ';' J is halt-free ;

theorem :: COMPOS_1:69

registration
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 ((Macro i),n)

for n being Nat

for i being Instruction of S holds Macro (IncAddr (i,n)) = IncAddr ((Macro i),n)

proof end;

theorem :: COMPOS_1:75

for S being COM-Struct

for J, I being Program of S holds I ';' J = (CutLastLoc I) ^ (IncAddr (J,((card I) -' 1)))

for J, I being Program of S holds I ';' J = (CutLastLoc I) ^ (IncAddr (J,((card I) -' 1)))

proof end;

theorem :: COMPOS_1:76

for S being COM-Struct

for n being Nat

for i being Instruction of S holds IncAddr ((Macro i),n) = (IncAddr ((Load i),n)) ^ (Stop S)

for n being Nat

for i being Instruction of S holds IncAddr ((Macro i),n) = (IncAddr ((Load i),n)) ^ (Stop S)

proof end;

theorem :: COMPOS_1:77

for S being COM-Struct

for F, G being Program of S

for n being Nat st n < LastLoc F holds

F . n = (F ';' G) . n

for F, G being Program of S

for n being Nat st n < LastLoc F holds

F . n = (F ';' G) . n

proof end;