:: COMPOS_2 semantic presentation

begin

registration
cluster with_non_trivial_Instructions for COM-Struct ;
existence
 ex b1 being COM-Struct st b1 is with_non_trivial_Instructions
proof
take C = COM-Struct(# the non trivial Instructions #); ::_thesis: C is with_non_trivial_Instructions
thus  not the InstructionsF of C is trivial ; :: according to AMISTD_4:def_1 ::_thesis: verum
end;
end;

registration
let S be with_non_trivial_Instructions COM-Struct ;
cluster No-StopCode for Element of the InstructionsF of S;
existence
 ex b1 being Instruction of S st b1 is No-StopCode
proof
 not the InstructionsF of S is trivial by AMISTD_4:def_1;
then consider x, y being set  such that
W1: ( x in the InstructionsF of S & y in the InstructionsF of S ) and
W2: x <> y by ZFMISC_1:def_10;
 ( x <> halt S or y <> halt S ) by W2;
then consider i being Instruction of S such that
W3: i <> halt S by W1;
take  i ; ::_thesis: i is No-StopCode
thus  i is No-StopCode by W3, COMPOS_0:def_12; ::_thesis: verum
end;
end;

registration
let S be with_non_trivial_Instructions COM-Struct ;
let i be No-StopCode Instruction of S;
cluster Macro i ->  halt-ending unique-halt ;
coherence
 ( Macro i is halt-ending & Macro i is unique-halt )
proof
B: LastLoc (Macro i) = (card (Macro i)) -' 1 by AFINSQ_1:70
.= 2 -' 1 by COMPOS_1:56
.= 2 - 1 by XREAL_1:233
.= 1 ;
hence  (Macro i) . (LastLoc (Macro i)) = halt S by COMPOS_1:59; :: according to COMPOS_1:def_14 ::_thesis: Macro i is unique-halt
thus  Macro i is unique-halt ::_thesis: verum
proof
let f be Nat; :: according to COMPOS_1:def_15 ::_thesis: ( not (Macro i) . f = halt S or not f in dom (Macro i) or f = LastLoc (Macro i) )
assume Z1: (Macro i) . f = halt S ; ::_thesis: ( not f in dom (Macro i) or f = LastLoc (Macro i) )
assume Z2: f in dom (Macro i) ; ::_thesis: f = LastLoc (Macro i)
now__::_thesis:_not_f_=_0
assume  f = 0 ; ::_thesis: contradiction
then  (Macro i) . f = i by COMPOS_1:58;
hence  contradiction by Z1, COMPOS_0:def_12; ::_thesis: verum
end;
hence  f = LastLoc (Macro i) by Z2, B, COMPOS_1:60; ::_thesis: verum
end;
end;
end;

definition
let S be with_non_trivial_Instructions COM-Struct ;
let i be No-StopCode Instruction of S;
let J be MacroInstruction of S;
funci ';' J ->  MacroInstruction of S equals :: COMPOS_2:def 1
(Macro i) ';' J;
correctness
coherence
(Macro i) ';' J is MacroInstruction of S;
;
end;

:: deftheorem  defines ';' COMPOS_2:def_1_:_
 for S being with_non_trivial_Instructions COM-Struct
for i being No-StopCode Instruction of S
for J being MacroInstruction of S holds i ';' J = (Macro i) ';' J;

definition
let S be with_non_trivial_Instructions COM-Struct ;
let I be MacroInstruction of S;
let j be No-StopCode Instruction of S;
funcI ';' j ->  MacroInstruction of S equals :: COMPOS_2:def 2
I ';' (Macro j);
correctness
coherence
I ';' (Macro j) is MacroInstruction of S;
;
end;

:: deftheorem  defines ';' COMPOS_2:def_2_:_
 for S being with_non_trivial_Instructions COM-Struct
for I being MacroInstruction of S
for j being No-StopCode Instruction of S holds I ';' j = I ';' (Macro j);

definition
let S be with_non_trivial_Instructions COM-Struct ;
let i, j be No-StopCode Instruction of S;
funci ';' j ->  MacroInstruction of S equals :: COMPOS_2:def 3
(Macro i) ';' (Macro j);
correctness
coherence
(Macro i) ';' (Macro j) is MacroInstruction of S;
;
end;

:: deftheorem  defines ';' COMPOS_2:def_3_:_
 for S being with_non_trivial_Instructions COM-Struct
for i, j being No-StopCode Instruction of S holds i ';' j = (Macro i) ';' (Macro j);


theorem :: COMPOS_2:1
for S being with_non_trivial_Instructions COM-Struct
for k being No-StopCode Instruction of S
for I, J being MacroInstruction of S holds (I ';' J) ';' k = I ';' (J ';' k) by COMPOS_1:29;

theorem :: COMPOS_2:2
for S being with_non_trivial_Instructions COM-Struct
for j being No-StopCode Instruction of S
for I, K being MacroInstruction of S holds (I ';' j) ';' K = I ';' (j ';' K) by COMPOS_1:29;

theorem :: COMPOS_2:3
for S being with_non_trivial_Instructions COM-Struct
for j, k being No-StopCode Instruction of S
for I being MacroInstruction of S holds (I ';' j) ';' k = I ';' (j ';' k) by COMPOS_1:29;

theorem :: COMPOS_2:4
for S being with_non_trivial_Instructions COM-Struct
for i being No-StopCode Instruction of S
for J, K being MacroInstruction of S holds (i ';' J) ';' K = i ';' (J ';' K) by COMPOS_1:29;

theorem :: COMPOS_2:5
for S being with_non_trivial_Instructions COM-Struct
for i, k being No-StopCode Instruction of S
for J being MacroInstruction of S holds (i ';' J) ';' k = i ';' (J ';' k) by COMPOS_1:29;

theorem :: COMPOS_2:6
for S being with_non_trivial_Instructions COM-Struct
for i, j being No-StopCode Instruction of S
for K being MacroInstruction of S holds (i ';' j) ';' K = i ';' (j ';' K) by COMPOS_1:29;

theorem :: COMPOS_2:7
for S being with_non_trivial_Instructions COM-Struct
for i, j, k being No-StopCode Instruction of S holds (i ';' j) ';' k = i ';' (j ';' k) by COMPOS_1:29;

theorem :: COMPOS_2:8
for S being with_non_trivial_Instructions COM-Struct
for i, j being No-StopCode Instruction of S holds i ';' j = (Macro i) ';' j ;

theorem :: COMPOS_2:9
for S being with_non_trivial_Instructions COM-Struct
for i, j being No-StopCode Instruction of S holds i ';' j = i ';' (Macro j) ;

theorem :: COMPOS_2:10
for S being with_non_trivial_Instructions COM-Struct
for i being No-StopCode Instruction of S
for J being MacroInstruction of S holds card (i ';' J) = (card J) + 1
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for i being No-StopCode Instruction of S
for J being MacroInstruction of S holds card (i ';' J) = (card J) + 1
let i be No-StopCode Instruction of S; ::_thesis: for J being MacroInstruction of S holds card (i ';' J) = (card J) + 1
let J be MacroInstruction of S; ::_thesis: card (i ';' J) = (card J) + 1
thus  card (i ';' J) = ((card (Macro i)) + (card J)) - 1 by COMPOS_1:20
.= (2 + (card J)) - 1 by COMPOS_1:56
.= (card J) + 1 ; ::_thesis: verum
end;

theorem Th11: :: COMPOS_2:11
for S being with_non_trivial_Instructions COM-Struct
for j being No-StopCode Instruction of S
for I being MacroInstruction of S holds card (I ';' j) = (card I) + 1
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for j being No-StopCode Instruction of S
for I being MacroInstruction of S holds card (I ';' j) = (card I) + 1
let j be No-StopCode Instruction of S; ::_thesis: for I being MacroInstruction of S holds card (I ';' j) = (card I) + 1
let I be MacroInstruction of S; ::_thesis: card (I ';' j) = (card I) + 1
thus  card (I ';' j) = ((card I) + (card (Macro j))) - 1 by COMPOS_1:20
.= (2 + (card I)) - 1 by COMPOS_1:56
.= (card I) + 1 ; ::_thesis: verum
end;

theorem Th12: :: COMPOS_2:12
for S being with_non_trivial_Instructions COM-Struct
for i, j being No-StopCode Instruction of S holds card (i ';' j) = 3
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for i, j being No-StopCode Instruction of S holds card (i ';' j) = 3
let i, j be No-StopCode Instruction of S; ::_thesis: card (i ';' j) = 3
thus  card (i ';' j) = ((card (Macro i)) + (card (Macro j))) - 1 by COMPOS_1:20
.= (2 + (card (Macro i))) - 1 by COMPOS_1:56
.= (2 + 2) - 1 by COMPOS_1:56
.= 3 ; ::_thesis: verum
end;

theorem Th13: :: COMPOS_2:13
for S being with_non_trivial_Instructions COM-Struct
for i, j, k being No-StopCode Instruction of S holds card ((i ';' j) ';' k) = 4
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for i, j, k being No-StopCode Instruction of S holds card ((i ';' j) ';' k) = 4
let i, j, k be No-StopCode Instruction of S; ::_thesis: card ((i ';' j) ';' k) = 4
thus  card ((i ';' j) ';' k) = (card (i ';' j)) + 1 by Th11
.= 3 + 1 by Th12
.= 4 ; ::_thesis: verum
end;


theorem Th14: :: COMPOS_2:14
for S being with_non_trivial_Instructions COM-Struct
for i1, i2, i3, i4 being No-StopCode Instruction of S holds card (((i1 ';' i2) ';' i3) ';' i4) = 5
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for i1, i2, i3, i4 being No-StopCode Instruction of S holds card (((i1 ';' i2) ';' i3) ';' i4) = 5
let i1, i2, i3, i4 be No-StopCode Instruction of S; ::_thesis: card (((i1 ';' i2) ';' i3) ';' i4) = 5
thus  card (((i1 ';' i2) ';' i3) ';' i4) = (card ((i1 ';' i2) ';' i3)) + 1 by Th11
.= 4 + 1 by Th13
.= 5 ; ::_thesis: verum
end;

theorem Th15: :: COMPOS_2:15
for S being with_non_trivial_Instructions COM-Struct
for i1, i2, i3, i4, i5 being No-StopCode Instruction of S holds card ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) = 6
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for i1, i2, i3, i4, i5 being No-StopCode Instruction of S holds card ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) = 6
let i1, i2, i3, i4, i5 be No-StopCode Instruction of S; ::_thesis: card ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) = 6
thus  card ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) = (card (((i1 ';' i2) ';' i3) ';' i4)) + 1 by Th11
.= 5 + 1 by Th14
.= 6 ; ::_thesis: verum
end;

theorem Th16: :: COMPOS_2:16
for S being with_non_trivial_Instructions COM-Struct
for i1, i2, i3, i4, i5, i6 being No-StopCode Instruction of S holds card (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) = 7
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for i1, i2, i3, i4, i5, i6 being No-StopCode Instruction of S holds card (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) = 7
let i1, i2, i3, i4, i5, i6 be No-StopCode Instruction of S; ::_thesis: card (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) = 7
thus  card (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) = (card ((((i1 ';' i2) ';' i3) ';' i4) ';' i5)) + 1 by Th11
.= 6 + 1 by Th15
.= 7 ; ::_thesis: verum
end;


definition
let I be non empty NAT -defined finite Function;
let J be set ;
predI <= J means :: COMPOS_2:def 4
 CutLastLoc I c= J;
end;

:: deftheorem  defines <= COMPOS_2:def_4_:_
 for I being non empty NAT -defined finite Function
for J being set holds
( I <= J iff CutLastLoc I c= J );

definition
let I, J be non empty NAT -defined finite Function;
:: original: <=
redefine predI <= J;
reflexivity
 for I being non empty NAT -defined finite Function holds (b1,b1)
proof
let I be non empty NAT -defined finite Function; ::_thesis: (I,I)
thus  CutLastLoc I c= I ; :: according to COMPOS_2:def_4 ::_thesis: verum
end;
end;

theorem Th17: :: COMPOS_2:17
for F being non empty NAT -defined finite Function holds not LastLoc F in dom (CutLastLoc F)
proof
let F be non empty NAT -defined finite Function; ::_thesis: not LastLoc F in dom (CutLastLoc F)
 LastLoc F in dom F by VALUED_1:30;
then  F | {(LastLoc F)} = (LastLoc F) .--> (F . (LastLoc F)) by FUNCT_7:6;
then A: dom (CutLastLoc F) = (dom F) \ {(LastLoc F)} by RELAT_1:177;
 LastLoc F in {(LastLoc F)} by TARSKI:def_1;
hence  not LastLoc F in dom (CutLastLoc F) by A, XBOOLE_0:def_5; ::_thesis: verum
end;

registration
let S be with_non_trivial_Instructions COM-Struct ;
let I be non empty unique-halt preProgram of S;
cluster CutLastLoc I ->  halt-free ;
coherence
 CutLastLoc I is halt-free
proof
now__::_thesis:_not_halt_S_in_rng_(CutLastLoc_I)
assume  halt S in rng (CutLastLoc I) ; ::_thesis: contradiction
then consider x being set  such that
W1: x in dom (CutLastLoc I) and
W2: (CutLastLoc I) . x = halt S by FUNCT_1:def_3;
 dom (CutLastLoc I) c= dom I by RELAT_1:11;
then B: x in dom I by W1;
D: dom I c= NAT by RELAT_1:def_18;
 I . x = halt S by W2, W1, GRFUNC_1:2;
then  x = LastLoc I by B, D, COMPOS_1:def_15;
hence  contradiction by W1, Th17; ::_thesis: verum
end;
hence  CutLastLoc I is halt-free by COMPOS_1:def_11; ::_thesis: verum
end;
end;

Lm1:  for f, g being Function st f c= g holds
for x, y being set st not x in rng f holds
f c= g \ (y .--> x)
proof
let f, g be Function; ::_thesis: ( f c= g implies for x, y being set st not x in rng f holds
f c= g \ (y .--> x) )
assume Z1: f c= g ; ::_thesis: for x, y being set st not x in rng f holds
f c= g \ (y .--> x)
let x, y be set ; ::_thesis: ( not x in rng f implies f c= g \ (y .--> x) )
assume  not x in rng f ; ::_thesis: f c= g \ (y .--> x)
then A: not [y,x] in f by XTUPLE_0:def_13;
 y .--> x = {[y,x]} by ZFMISC_1:29;
hence  f c= g \ (y .--> x) by A, Z1, ZFMISC_1:34; ::_thesis: verum
end;

theorem Th18: :: COMPOS_2:18
for S being with_non_trivial_Instructions COM-Struct
for I being unique-halt Program of S
for J being halt-ending Program of S st CutLastLoc I c= J holds
CutLastLoc I c= CutLastLoc J
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for I being unique-halt Program of S
for J being halt-ending Program of S st CutLastLoc I c= J holds
CutLastLoc I c= CutLastLoc J
let I be unique-halt Program of S; ::_thesis: for J being halt-ending Program of S st CutLastLoc I c= J holds
CutLastLoc I c= CutLastLoc J
let J be halt-ending Program of S; ::_thesis: ( CutLastLoc I c= J implies CutLastLoc I c= CutLastLoc J )
assume Z: CutLastLoc I c= J ; ::_thesis: CutLastLoc I c= CutLastLoc J
A: not halt S in rng (CutLastLoc I) by COMPOS_1:def_11;
 J . (LastLoc J) = halt S by COMPOS_1:def_14;
hence  CutLastLoc I c= CutLastLoc J by A, Z, Lm1; ::_thesis: verum
end;


theorem :: COMPOS_2:19
for S being with_non_trivial_Instructions COM-Struct
for I, J being MacroInstruction of S
for K being set st I <= J & J <= K holds
I <= K
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for I, J being MacroInstruction of S
for K being set st I <= J & J <= K holds
I <= K
let I, J be MacroInstruction of S; ::_thesis: for K being set st I <= J & J <= K holds
I <= K
let K be set ; ::_thesis: ( I <= J & J <= K implies I <= K )
assume that
Z1: CutLastLoc I c= J and
Z2: CutLastLoc J c= K ; :: according to COMPOS_2:def_4 ::_thesis: I <= K
 CutLastLoc I c= CutLastLoc J by Z1, Th18;
hence  CutLastLoc I c= K by Z2, XBOOLE_1:1; :: according to COMPOS_2:def_4 ::_thesis: verum
end;

theorem Thx: :: COMPOS_2:20
for S being with_non_trivial_Instructions COM-Struct
for I being MacroInstruction of S holds I = (CutLastLoc I) +* ((LastLoc I) .--> (halt S))
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for I being MacroInstruction of S holds I = (CutLastLoc I) +* ((LastLoc I) .--> (halt S))
let I be MacroInstruction of S; ::_thesis: I = (CutLastLoc I) +* ((LastLoc I) .--> (halt S))
E: LastLoc I in dom I by VALUED_1:30;
D: {(LastLoc I)} misses dom (CutLastLoc I) by Th17, ZFMISC_1:50;
A: dom ((LastLoc I) .--> (I . (LastLoc I))) = {(LastLoc I)} by FUNCOP_1:13;
I = (CutLastLoc I) \/ ((LastLoc I) .--> (I . (LastLoc I))) by E, FUNCOP_1:84, XBOOLE_1:45
.= (CutLastLoc I) +* ((LastLoc I) .--> (I . (LastLoc I))) by A, D, FUNCT_4:31 ;
hence  I = (CutLastLoc I) +* ((LastLoc I) .--> (halt S)) by COMPOS_1:def_14; ::_thesis: verum
end;

theorem Th21: :: COMPOS_2:21
for S being with_non_trivial_Instructions COM-Struct
for I, J being MacroInstruction of S st CutLastLoc I = CutLastLoc J holds
I = J
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for I, J being MacroInstruction of S st CutLastLoc I = CutLastLoc J holds
I = J
let I, J be MacroInstruction of S; ::_thesis: ( CutLastLoc I = CutLastLoc J implies I = J )
assume Z: CutLastLoc I = CutLastLoc J ; ::_thesis: I = J
(card I) - 1 = card (CutLastLoc J) by Z, VALUED_1:38
.= (card J) - 1 by VALUED_1:38 ;
then  LastLoc I = (card J) -' 1 by AFINSQ_1:70
.= LastLoc J by AFINSQ_1:70 ;
hence I = (CutLastLoc I) +* ((LastLoc J) .--> (halt S)) by Thx
.= J by Z, Thx ;
::_thesis: verum
end;

theorem :: COMPOS_2:22
for S being with_non_trivial_Instructions COM-Struct
for I, J being MacroInstruction of S st I <= J & J <= I holds
I = J
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for I, J being MacroInstruction of S st I <= J & J <= I holds
I = J
let I, J be MacroInstruction of S; ::_thesis: ( I <= J & J <= I implies I = J )
assume  CutLastLoc I c= J ; :: according to COMPOS_2:def_4 ::_thesis: ( not J <= I or I = J )
then Z1: CutLastLoc I c= CutLastLoc J by Th18;
assume  CutLastLoc J c= I ; :: according to COMPOS_2:def_4 ::_thesis: I = J
then  CutLastLoc J c= CutLastLoc I by Th18;
then  CutLastLoc I = CutLastLoc J by Z1, XBOOLE_0:def_10;
hence  I = J by Th21; ::_thesis: verum
end;

theorem Th23: :: COMPOS_2:23
for S being with_non_trivial_Instructions COM-Struct
for I, J being MacroInstruction of S holds I <= I ';' J
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for I, J being MacroInstruction of S holds I <= I ';' J
let I, J be MacroInstruction of S; ::_thesis: I <= I ';' J
 dom (CutLastLoc I) misses dom (Reloc (J,((card I) -' 1))) by COMPOS_1:18;
hence  CutLastLoc I c= I ';' J by FUNCT_4:32; :: according to COMPOS_2:def_4 ::_thesis: verum
end;

theorem :: COMPOS_2:24
for S being with_non_trivial_Instructions COM-Struct
for I being MacroInstruction of S
for X being set st I c= X holds
I <= X
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for I being MacroInstruction of S
for X being set st I c= X holds
I <= X
let I be MacroInstruction of S; ::_thesis: for X being set st I c= X holds
I <= X
let X be set ; ::_thesis: ( I c= X implies I <= X )
assume Z: I c= X ; ::_thesis: I <= X
thus  CutLastLoc I c= X by Z, XBOOLE_1:1; :: according to COMPOS_2:def_4 ::_thesis: verum
end;

theorem :: COMPOS_2:25
for S being with_non_trivial_Instructions COM-Struct
for I, J being MacroInstruction of S st I <= J holds
for X being set st J c= X holds
I <= X
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for I, J being MacroInstruction of S st I <= J holds
for X being set st J c= X holds
I <= X
let I, J be MacroInstruction of S; ::_thesis: ( I <= J implies for X being set st J c= X holds
I <= X )
assume Z1: CutLastLoc I c= J ; :: according to COMPOS_2:def_4 ::_thesis: for X being set st J c= X holds
I <= X
let X be set ; ::_thesis: ( J c= X implies I <= X )
assume  J c= X ; ::_thesis: I <= X
hence  CutLastLoc I c= X by Z1, XBOOLE_1:1; :: according to COMPOS_2:def_4 ::_thesis: verum
end;

theorem Th26: :: COMPOS_2:26
for S being with_non_trivial_Instructions COM-Struct
for I being MacroInstruction of S
for k being Nat holds
( k < LastLoc I iff k in dom (CutLastLoc I) )
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for I being MacroInstruction of S
for k being Nat holds
( k < LastLoc I iff k in dom (CutLastLoc I) )
let I be MacroInstruction of S; ::_thesis: for k being Nat holds
( k < LastLoc I iff k in dom (CutLastLoc I) )
let k be Nat; ::_thesis: ( k < LastLoc I iff k in dom (CutLastLoc I) )
 card I > 0 by NAT_1:3;
then A: card I >= 0 + 1 by NAT_1:13;
card (CutLastLoc I) = (card I) - 1 by VALUED_1:38
.= (card I) -' 1 by A, XREAL_1:233
.= LastLoc I by AFINSQ_1:70 ;
hence  ( k < LastLoc I iff k in dom (CutLastLoc I) ) by NAT_1:44; ::_thesis: verum
end;

theorem Th27: :: COMPOS_2:27
for S being with_non_trivial_Instructions COM-Struct
for I being MacroInstruction of S
for k being Nat st k < LastLoc I holds
(CutLastLoc I) . k = I . k
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for I being MacroInstruction of S
for k being Nat st k < LastLoc I holds
(CutLastLoc I) . k = I . k
let I be MacroInstruction of S; ::_thesis: for k being Nat st k < LastLoc I holds
(CutLastLoc I) . k = I . k
let k be Nat; ::_thesis: ( k < LastLoc I implies (CutLastLoc I) . k = I . k )
assume  k < LastLoc I ; ::_thesis: (CutLastLoc I) . k = I . k
then A: k in dom (CutLastLoc I) by Th26;
thus  (CutLastLoc I) . k = I . k by A, GRFUNC_1:2; ::_thesis: verum
end;

theorem Th28: :: COMPOS_2:28
for S being with_non_trivial_Instructions COM-Struct
for I, J being MacroInstruction of S
for k being Nat st k < LastLoc I & I <= J holds
I . k = J . k
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for I, J being MacroInstruction of S
for k being Nat st k < LastLoc I & I <= J holds
I . k = J . k
let I, J be MacroInstruction of S; ::_thesis: for k being Nat st k < LastLoc I & I <= J holds
I . k = J . k
let k be Nat; ::_thesis: ( k < LastLoc I & I <= J implies I . k = J . k )
assume Z1: k < LastLoc I ; ::_thesis: ( not I <= J or I . k = J . k )
assume Z2: CutLastLoc I c= J ; :: according to COMPOS_2:def_4 ::_thesis: I . k = J . k
B: k in dom (CutLastLoc I) by Z1, Th26;
thus I . k = (CutLastLoc I) . k by Z1, Th27
.= J . k by Z2, B, GRFUNC_1:2 ; ::_thesis: verum
end;

theorem Th29: :: COMPOS_2:29
for S being with_non_trivial_Instructions COM-Struct
for I being MacroInstruction of S holds LastLoc I = (card I) - 1
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for I being MacroInstruction of S holds LastLoc I = (card I) - 1
let I be MacroInstruction of S; ::_thesis: LastLoc I = (card I) - 1
 card I > 0 by NAT_1:3;
then A: card I >= 0 + 1 by NAT_1:13;
thus  LastLoc I = (card I) -' 1 by AFINSQ_1:70
.= (card I) - 1 by A, XREAL_1:233 ; ::_thesis: verum
end;

theorem Th30: :: COMPOS_2:30
for S being with_non_trivial_Instructions COM-Struct
for i being No-StopCode Instruction of S holds LastLoc (Macro i) = 1
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for i being No-StopCode Instruction of S holds LastLoc (Macro i) = 1
let i be No-StopCode Instruction of S; ::_thesis: LastLoc (Macro i) = 1
thus  LastLoc (Macro i) = (card (Macro i)) - 1 by Th29
.= 2 - 1 by COMPOS_1:56
.= 1 ; ::_thesis: verum
end;

theorem Th31: :: COMPOS_2:31
for S being with_non_trivial_Instructions COM-Struct
for i, j being No-StopCode Instruction of S holds LastLoc (i ';' j) = 2
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for i, j being No-StopCode Instruction of S holds LastLoc (i ';' j) = 2
let i, j be No-StopCode Instruction of S; ::_thesis: LastLoc (i ';' j) = 2
thus  LastLoc (i ';' j) = (card (i ';' j)) - 1 by Th29
.= 3 - 1 by Th12
.= 2 ; ::_thesis: verum
end;

theorem Th32: :: COMPOS_2:32
for S being with_non_trivial_Instructions COM-Struct
for i, j, k being No-StopCode Instruction of S holds LastLoc ((i ';' j) ';' k) = 3
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for i, j, k being No-StopCode Instruction of S holds LastLoc ((i ';' j) ';' k) = 3
let i, j, k be No-StopCode Instruction of S; ::_thesis: LastLoc ((i ';' j) ';' k) = 3
thus  LastLoc ((i ';' j) ';' k) = (card ((i ';' j) ';' k)) - 1 by Th29
.= 4 - 1 by Th13
.= 3 ; ::_thesis: verum
end;

theorem Th33: :: COMPOS_2:33
for S being with_non_trivial_Instructions COM-Struct
for i1, i2, i3, i4 being No-StopCode Instruction of S holds LastLoc (((i1 ';' i2) ';' i3) ';' i4) = 4
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for i1, i2, i3, i4 being No-StopCode Instruction of S holds LastLoc (((i1 ';' i2) ';' i3) ';' i4) = 4
let i1, i2, i3, i4 be No-StopCode Instruction of S; ::_thesis: LastLoc (((i1 ';' i2) ';' i3) ';' i4) = 4
thus  LastLoc (((i1 ';' i2) ';' i3) ';' i4) = (card (((i1 ';' i2) ';' i3) ';' i4)) - 1 by Th29
.= 5 - 1 by Th14
.= 4 ; ::_thesis: verum
end;

theorem Th34: :: COMPOS_2:34
for S being with_non_trivial_Instructions COM-Struct
for i1, i2, i3, i4, i5 being No-StopCode Instruction of S holds LastLoc ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) = 5
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for i1, i2, i3, i4, i5 being No-StopCode Instruction of S holds LastLoc ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) = 5
let i1, i2, i3, i4, i5 be No-StopCode Instruction of S; ::_thesis: LastLoc ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) = 5
thus  LastLoc ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) = (card ((((i1 ';' i2) ';' i3) ';' i4) ';' i5)) - 1 by Th29
.= 6 - 1 by Th15
.= 5 ; ::_thesis: verum
end;

theorem Th35: :: COMPOS_2:35
for S being with_non_trivial_Instructions COM-Struct
for i1, i2, i3, i4, i5, i6 being No-StopCode Instruction of S holds LastLoc (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) = 6
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for i1, i2, i3, i4, i5, i6 being No-StopCode Instruction of S holds LastLoc (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) = 6
let i1, i2, i3, i4, i5, i6 be No-StopCode Instruction of S; ::_thesis: LastLoc (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) = 6
thus  LastLoc (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) = (card (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6)) - 1 by Th29
.= 7 - 1 by Th16
.= 6 ; ::_thesis: verum
end;

theorem Th36: :: COMPOS_2:36
for S being with_non_trivial_Instructions COM-Struct
for i being No-StopCode Instruction of S
for J being MacroInstruction of S holds (i ';' J) . 0 = i
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for i being No-StopCode Instruction of S
for J being MacroInstruction of S holds (i ';' J) . 0 = i
let i be No-StopCode Instruction of S; ::_thesis: for J being MacroInstruction of S holds (i ';' J) . 0 = i
let J be MacroInstruction of S; ::_thesis: (i ';' J) . 0 = i
 LastLoc (Macro i) = 1 by Th30;
hence (i ';' J) . 0 = (Macro i) . 0 by Th23, Th28
.= i by COMPOS_1:58 ;
::_thesis: verum
end;

theorem Th37: :: COMPOS_2:37
for S being with_non_trivial_Instructions COM-Struct
for i, j being No-StopCode Instruction of S
for K being MacroInstruction of S holds ((i ';' j) ';' K) . 0 = i
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for i, j being No-StopCode Instruction of S
for K being MacroInstruction of S holds ((i ';' j) ';' K) . 0 = i
let i, j be No-StopCode Instruction of S; ::_thesis: for K being MacroInstruction of S holds ((i ';' j) ';' K) . 0 = i
let K be MacroInstruction of S; ::_thesis: ((i ';' j) ';' K) . 0 = i
 LastLoc (i ';' j) = 2 by Th31;
hence ((i ';' j) ';' K) . 0 = (i ';' j) . 0 by Th23, Th28
.= (i ';' (Macro j)) . 0
.= i by Th36 ;
::_thesis: verum
end;

theorem Th38: :: COMPOS_2:38
for S being with_non_trivial_Instructions COM-Struct
for i, j, k being No-StopCode Instruction of S
for K being MacroInstruction of S holds (((i ';' j) ';' k) ';' K) . 0 = i
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for i, j, k being No-StopCode Instruction of S
for K being MacroInstruction of S holds (((i ';' j) ';' k) ';' K) . 0 = i
let i, j, k be No-StopCode Instruction of S; ::_thesis: for K being MacroInstruction of S holds (((i ';' j) ';' k) ';' K) . 0 = i
let K be MacroInstruction of S; ::_thesis: (((i ';' j) ';' k) ';' K) . 0 = i
 LastLoc ((i ';' j) ';' k) = 3 by Th32;
hence (((i ';' j) ';' k) ';' K) . 0 = ((i ';' j) ';' k) . 0 by Th23, Th28
.= ((i ';' j) ';' (Macro k)) . 0
.= i by Th37 ;
::_thesis: verum
end;

theorem Th39: :: COMPOS_2:39
for S being with_non_trivial_Instructions COM-Struct
for K being MacroInstruction of S
for i1, i2, i3, i4 being No-StopCode Instruction of S holds ((((i1 ';' i2) ';' i3) ';' i4) ';' K) . 0 = i1
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for K being MacroInstruction of S
for i1, i2, i3, i4 being No-StopCode Instruction of S holds ((((i1 ';' i2) ';' i3) ';' i4) ';' K) . 0 = i1
let K be MacroInstruction of S; ::_thesis: for i1, i2, i3, i4 being No-StopCode Instruction of S holds ((((i1 ';' i2) ';' i3) ';' i4) ';' K) . 0 = i1
let i1, i2, i3, i4 be No-StopCode Instruction of S; ::_thesis: ((((i1 ';' i2) ';' i3) ';' i4) ';' K) . 0 = i1
 LastLoc (((i1 ';' i2) ';' i3) ';' i4) = 4 by Th33;
hence ((((i1 ';' i2) ';' i3) ';' i4) ';' K) . 0 = (((i1 ';' i2) ';' i3) ';' i4) . 0 by Th23, Th28
.= (((i1 ';' i2) ';' i3) ';' (Macro i4)) . 0
.= i1 by Th38 ;
::_thesis: verum
end;

theorem Th40: :: COMPOS_2:40
for S being with_non_trivial_Instructions COM-Struct
for K being MacroInstruction of S
for i1, i2, i3, i4, i5 being No-StopCode Instruction of S holds (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' K) . 0 = i1
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for K being MacroInstruction of S
for i1, i2, i3, i4, i5 being No-StopCode Instruction of S holds (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' K) . 0 = i1
let K be MacroInstruction of S; ::_thesis: for i1, i2, i3, i4, i5 being No-StopCode Instruction of S holds (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' K) . 0 = i1
let i1, i2, i3, i4, i5 be No-StopCode Instruction of S; ::_thesis: (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' K) . 0 = i1
 LastLoc ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) = 5 by Th34;
hence (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' K) . 0 = ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 0 by Th23, Th28
.= ((((i1 ';' i2) ';' i3) ';' i4) ';' (Macro i5)) . 0
.= i1 by Th39 ;
::_thesis: verum
end;

theorem :: COMPOS_2:41
for S being with_non_trivial_Instructions COM-Struct
for K being MacroInstruction of S
for i1, i2, i3, i4, i5, i6 being No-StopCode Instruction of S holds ((((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) ';' K) . 0 = i1
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for K being MacroInstruction of S
for i1, i2, i3, i4, i5, i6 being No-StopCode Instruction of S holds ((((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) ';' K) . 0 = i1
let K be MacroInstruction of S; ::_thesis: for i1, i2, i3, i4, i5, i6 being No-StopCode Instruction of S holds ((((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) ';' K) . 0 = i1
let i1, i2, i3, i4, i5, i6 be No-StopCode Instruction of S; ::_thesis: ((((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) ';' K) . 0 = i1
 LastLoc (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) = 6 by Th35;
hence ((((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) ';' K) . 0 = (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) . 0 by Th23, Th28
.= (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' (Macro i6)) . 0
.= i1 by Th40 ;
::_thesis: verum
end;

theorem :: COMPOS_2:42
for S being with_non_trivial_Instructions COM-Struct
for I, J being MacroInstruction of S
for k being Nat st k < LastLoc I holds
(I ';' J) . k = I . k
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for I, J being MacroInstruction of S
for k being Nat st k < LastLoc I holds
(I ';' J) . k = I . k
let I, J be MacroInstruction of S; ::_thesis: for k being Nat st k < LastLoc I holds
(I ';' J) . k = I . k
let k be Nat; ::_thesis: ( k < LastLoc I implies (I ';' J) . k = I . k )
assume  k < LastLoc I ; ::_thesis: (I ';' J) . k = I . k
then A: k in dom (CutLastLoc I) by Th26;
 dom (CutLastLoc I) misses dom (Reloc (J,((card I) -' 1))) by COMPOS_1:18;
then  not k in dom (Reloc (J,((card I) -' 1))) by A, XBOOLE_0:3;
hence (I ';' J) . k = (CutLastLoc I) . k by FUNCT_4:11
.= I . k by A, GRFUNC_1:2 ;
::_thesis: verum
end;

theorem :: COMPOS_2:43
for S being with_non_trivial_Instructions COM-Struct
for I, J being MacroInstruction of S holds LastLoc (I ';' J) = (LastLoc I) + (LastLoc J)
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for I, J being MacroInstruction of S holds LastLoc (I ';' J) = (LastLoc I) + (LastLoc J)
let I, J be MacroInstruction of S; ::_thesis: LastLoc (I ';' J) = (LastLoc I) + (LastLoc J)
thus  LastLoc (I ';' J) = (card (I ';' J)) - 1 by Th29
.= (((card I) + (card J)) - 1) - 1 by COMPOS_1:20
.= ((card I) - 1) + ((card J) - 1)
.= (LastLoc I) + ((card J) - 1) by Th29
.= (LastLoc I) + (LastLoc J) by Th29 ; ::_thesis: verum
end;

theorem Th44: :: COMPOS_2:44
for S being with_non_trivial_Instructions COM-Struct
for J, I being MacroInstruction of S
for j being Nat st j <= LastLoc J holds
(I ';' J) . ((LastLoc I) + j) = IncAddr ((J /. j),(LastLoc I))
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for J, I being MacroInstruction of S
for j being Nat st j <= LastLoc J holds
(I ';' J) . ((LastLoc I) + j) = IncAddr ((J /. j),(LastLoc I))
let J, I be MacroInstruction of S; ::_thesis: for j being Nat st j <= LastLoc J holds
(I ';' J) . ((LastLoc I) + j) = IncAddr ((J /. j),(LastLoc I))
let j be Nat; ::_thesis: ( j <= LastLoc J implies (I ';' J) . ((LastLoc I) + j) = IncAddr ((J /. j),(LastLoc I)) )
assume Z0: j <= LastLoc J ; ::_thesis: (I ';' J) . ((LastLoc I) + j) = IncAddr ((J /. j),(LastLoc I))
set k = (LastLoc I) + j;
F: LastLoc I = (card I) -' 1 by AFINSQ_1:70;
X: j <= (card J) - 1 by Z0, Th29;
 (card J) - 1 < card J by XREAL_1:44;
then  j < card J by X, XXREAL_0:2;
then D: j in dom J by NAT_1:44;
then C: j in dom (IncAddr (J,(LastLoc I))) by COMPOS_1:def_21;
E: (LastLoc I) + j in dom (Reloc (J,(LastLoc I))) by D, COMPOS_1:46;
reconsider j = j as Element of NAT by ORDINAL1:def_12;
(I ';' J) . ((LastLoc I) + j) = (Reloc (J,(LastLoc I))) . ((LastLoc I) + j) by E, F, FUNCT_4:13
.= (IncAddr (J,(LastLoc I))) . j by C, VALUED_1:def_12
.= IncAddr ((J /. j),(LastLoc I)) by D, COMPOS_1:def_21 ;
hence  (I ';' J) . ((LastLoc I) + j) = IncAddr ((J /. j),(LastLoc I)) ; ::_thesis: verum
end;

theorem Th45: :: COMPOS_2:45
for S being with_non_trivial_Instructions COM-Struct
for i, j being No-StopCode Instruction of S holds (i ';' j) . 1 = IncAddr (j,1)
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for i, j being No-StopCode Instruction of S holds (i ';' j) . 1 = IncAddr (j,1)
let i, j be No-StopCode Instruction of S; ::_thesis: (i ';' j) . 1 = IncAddr (j,1)
 0 in dom (Macro j) by COMPOS_1:57;
then C: (Macro j) /. 0 = (Macro j) . 0 by PARTFUN1:def_6
.= j by COMPOS_1:58 ;
A: LastLoc (Macro j) = 1 by Th30;
thus (i ';' j) . 1 = (i ';' (Macro j)) . ((LastLoc (Macro i)) + 0) by Th30
.= IncAddr (((Macro j) /. 0),(LastLoc (Macro i))) by A, Th44
.= IncAddr (j,1) by C, Th30 ; ::_thesis: verum
end;

theorem Th46: :: COMPOS_2:46
for S being with_non_trivial_Instructions COM-Struct
for i, j, k being No-StopCode Instruction of S holds ((i ';' j) ';' k) . 1 = IncAddr (j,1)
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for i, j, k being No-StopCode Instruction of S holds ((i ';' j) ';' k) . 1 = IncAddr (j,1)
let i, j, k be No-StopCode Instruction of S; ::_thesis: ((i ';' j) ';' k) . 1 = IncAddr (j,1)
 LastLoc (i ';' j) = 2 by Th31;
hence ((i ';' j) ';' k) . 1 = (i ';' j) . 1 by Th23, Th28
.= IncAddr (j,1) by Th45 ;
::_thesis: verum
end;

theorem Th47: :: COMPOS_2:47
for S being with_non_trivial_Instructions COM-Struct
for i1, i2, i3, i4 being No-StopCode Instruction of S holds (((i1 ';' i2) ';' i3) ';' i4) . 1 = IncAddr (i2,1)
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for i1, i2, i3, i4 being No-StopCode Instruction of S holds (((i1 ';' i2) ';' i3) ';' i4) . 1 = IncAddr (i2,1)
let i1, i2, i3, i4 be No-StopCode Instruction of S; ::_thesis: (((i1 ';' i2) ';' i3) ';' i4) . 1 = IncAddr (i2,1)
 LastLoc ((i1 ';' i2) ';' i3) = 3 by Th32;
hence (((i1 ';' i2) ';' i3) ';' i4) . 1 = ((i1 ';' i2) ';' i3) . 1 by Th23, Th28
.= IncAddr (i2,1) by Th46 ;
::_thesis: verum
end;

theorem Th48: :: COMPOS_2:48
for S being with_non_trivial_Instructions COM-Struct
for i1, i2, i3, i4, i5 being No-StopCode Instruction of S holds ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 1 = IncAddr (i2,1)
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for i1, i2, i3, i4, i5 being No-StopCode Instruction of S holds ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 1 = IncAddr (i2,1)
let i1, i2, i3, i4, i5 be No-StopCode Instruction of S; ::_thesis: ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 1 = IncAddr (i2,1)
 LastLoc (((i1 ';' i2) ';' i3) ';' i4) = 4 by Th33;
hence ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 1 = (((i1 ';' i2) ';' i3) ';' i4) . 1 by Th23, Th28
.= IncAddr (i2,1) by Th47 ;
::_thesis: verum
end;

theorem :: COMPOS_2:49
for S being with_non_trivial_Instructions COM-Struct
for i1, i2, i3, i4, i5, i6 being No-StopCode Instruction of S holds (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) . 1 = IncAddr (i2,1)
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for i1, i2, i3, i4, i5, i6 being No-StopCode Instruction of S holds (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) . 1 = IncAddr (i2,1)
let i1, i2, i3, i4, i5, i6 be No-StopCode Instruction of S; ::_thesis: (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) . 1 = IncAddr (i2,1)
 LastLoc ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) = 5 by Th34;
hence (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) . 1 = ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 1 by Th23, Th28
.= IncAddr (i2,1) by Th48 ;
::_thesis: verum
end;

theorem Th50: :: COMPOS_2:50
for S being with_non_trivial_Instructions COM-Struct
for j being No-StopCode Instruction of S
for I being MacroInstruction of S holds (I ';' j) . (LastLoc I) = IncAddr (j,(LastLoc I))
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for j being No-StopCode Instruction of S
for I being MacroInstruction of S holds (I ';' j) . (LastLoc I) = IncAddr (j,(LastLoc I))
let j be No-StopCode Instruction of S; ::_thesis: for I being MacroInstruction of S holds (I ';' j) . (LastLoc I) = IncAddr (j,(LastLoc I))
let I be MacroInstruction of S; ::_thesis: (I ';' j) . (LastLoc I) = IncAddr (j,(LastLoc I))
A: 0 <= LastLoc (Macro j) by NAT_1:2;
 0 in dom (Macro j) by COMPOS_1:57;
then C: (Macro j) /. 0 = (Macro j) . 0 by PARTFUN1:def_6
.= j by COMPOS_1:58 ;
thus (I ';' j) . (LastLoc I) = (I ';' (Macro j)) . ((LastLoc I) + 0)
.= IncAddr (((Macro j) /. 0),(LastLoc I)) by A, Th44
.= IncAddr (j,(LastLoc I)) by C ; ::_thesis: verum
end;

theorem Th51: :: COMPOS_2:51
for S being with_non_trivial_Instructions COM-Struct
for i1, i2, i3 being No-StopCode Instruction of S holds ((i1 ';' i2) ';' i3) . 2 = IncAddr (i3,2)
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for i1, i2, i3 being No-StopCode Instruction of S holds ((i1 ';' i2) ';' i3) . 2 = IncAddr (i3,2)
let i1, i2, i3 be No-StopCode Instruction of S; ::_thesis: ((i1 ';' i2) ';' i3) . 2 = IncAddr (i3,2)
 LastLoc (i1 ';' i2) = 2 by Th31;
hence  ((i1 ';' i2) ';' i3) . 2 = IncAddr (i3,2) by Th50; ::_thesis: verum
end;

theorem Th52: :: COMPOS_2:52
for S being with_non_trivial_Instructions COM-Struct
for i1, i2, i3, i4 being No-StopCode Instruction of S holds (((i1 ';' i2) ';' i3) ';' i4) . 2 = IncAddr (i3,2)
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for i1, i2, i3, i4 being No-StopCode Instruction of S holds (((i1 ';' i2) ';' i3) ';' i4) . 2 = IncAddr (i3,2)
let i1, i2, i3, i4 be No-StopCode Instruction of S; ::_thesis: (((i1 ';' i2) ';' i3) ';' i4) . 2 = IncAddr (i3,2)
 LastLoc ((i1 ';' i2) ';' i3) = 3 by Th32;
hence (((i1 ';' i2) ';' i3) ';' i4) . 2 = ((i1 ';' i2) ';' i3) . 2 by Th23, Th28
.= IncAddr (i3,2) by Th51 ;
::_thesis: verum
end;

theorem Th53: :: COMPOS_2:53
for S being with_non_trivial_Instructions COM-Struct
for i1, i2, i3, i4, i5 being No-StopCode Instruction of S holds ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 2 = IncAddr (i3,2)
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for i1, i2, i3, i4, i5 being No-StopCode Instruction of S holds ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 2 = IncAddr (i3,2)
let i1, i2, i3, i4, i5 be No-StopCode Instruction of S; ::_thesis: ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 2 = IncAddr (i3,2)
 LastLoc (((i1 ';' i2) ';' i3) ';' i4) = 4 by Th33;
hence ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 2 = (((i1 ';' i2) ';' i3) ';' i4) . 2 by Th23, Th28
.= IncAddr (i3,2) by Th52 ;
::_thesis: verum
end;

theorem :: COMPOS_2:54
for S being with_non_trivial_Instructions COM-Struct
for i1, i2, i3, i4, i5, i6 being No-StopCode Instruction of S holds (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) . 2 = IncAddr (i3,2)
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for i1, i2, i3, i4, i5, i6 being No-StopCode Instruction of S holds (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) . 2 = IncAddr (i3,2)
let i1, i2, i3, i4, i5, i6 be No-StopCode Instruction of S; ::_thesis: (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) . 2 = IncAddr (i3,2)
 LastLoc ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) = 5 by Th34;
hence (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) . 2 = ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 2 by Th23, Th28
.= IncAddr (i3,2) by Th53 ;
::_thesis: verum
end;

theorem Th55: :: COMPOS_2:55
for S being with_non_trivial_Instructions COM-Struct
for i1, i2, i3, i4 being No-StopCode Instruction of S holds (((i1 ';' i2) ';' i3) ';' i4) . 3 = IncAddr (i4,3)
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for i1, i2, i3, i4 being No-StopCode Instruction of S holds (((i1 ';' i2) ';' i3) ';' i4) . 3 = IncAddr (i4,3)
let i1, i2, i3, i4 be No-StopCode Instruction of S; ::_thesis: (((i1 ';' i2) ';' i3) ';' i4) . 3 = IncAddr (i4,3)
 LastLoc ((i1 ';' i2) ';' i3) = 3 by Th32;
hence  (((i1 ';' i2) ';' i3) ';' i4) . 3 = IncAddr (i4,3) by Th50; ::_thesis: verum
end;

theorem Th56: :: COMPOS_2:56
for S being with_non_trivial_Instructions COM-Struct
for i1, i2, i3, i4, i5 being No-StopCode Instruction of S holds ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 3 = IncAddr (i4,3)
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for i1, i2, i3, i4, i5 being No-StopCode Instruction of S holds ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 3 = IncAddr (i4,3)
let i1, i2, i3, i4, i5 be No-StopCode Instruction of S; ::_thesis: ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 3 = IncAddr (i4,3)
B: LastLoc (((i1 ';' i2) ';' i3) ';' i4) = 4 by Th33;
thus ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 3 = (((i1 ';' i2) ';' i3) ';' i4) . 3 by Th23, B, Th28
.= IncAddr (i4,3) by Th55 ; ::_thesis: verum
end;

theorem :: COMPOS_2:57
for S being with_non_trivial_Instructions COM-Struct
for i1, i2, i3, i4, i5, i6 being No-StopCode Instruction of S holds (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) . 3 = IncAddr (i4,3)
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for i1, i2, i3, i4, i5, i6 being No-StopCode Instruction of S holds (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) . 3 = IncAddr (i4,3)
let i1, i2, i3, i4, i5, i6 be No-StopCode Instruction of S; ::_thesis: (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) . 3 = IncAddr (i4,3)
B: LastLoc ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) = 5 by Th34;
thus (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) . 3 = ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 3 by Th23, B, Th28
.= IncAddr (i4,3) by Th56 ; ::_thesis: verum
end;

theorem Th57: :: COMPOS_2:58
for S being with_non_trivial_Instructions COM-Struct
for i1, i2, i3, i4, i5 being No-StopCode Instruction of S holds ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 4 = IncAddr (i5,4)
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for i1, i2, i3, i4, i5 being No-StopCode Instruction of S holds ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 4 = IncAddr (i5,4)
let i1, i2, i3, i4, i5 be No-StopCode Instruction of S; ::_thesis: ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 4 = IncAddr (i5,4)
 LastLoc (((i1 ';' i2) ';' i3) ';' i4) = 4 by Th33;
hence  ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 4 = IncAddr (i5,4) by Th50; ::_thesis: verum
end;

theorem :: COMPOS_2:59
for S being with_non_trivial_Instructions COM-Struct
for i1, i2, i3, i4, i5, i6 being No-StopCode Instruction of S holds (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) . 4 = IncAddr (i5,4)
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for i1, i2, i3, i4, i5, i6 being No-StopCode Instruction of S holds (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) . 4 = IncAddr (i5,4)
let i1, i2, i3, i4, i5, i6 be No-StopCode Instruction of S; ::_thesis: (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) . 4 = IncAddr (i5,4)
B: LastLoc ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) = 5 by Th34;
thus (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) . 4 = ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 4 by Th23, B, Th28
.= IncAddr (i5,4) by Th57 ; ::_thesis: verum
end;

theorem :: COMPOS_2:60
for S being with_non_trivial_Instructions COM-Struct
for i1, i2, i3, i4, i5, i6 being No-StopCode Instruction of S holds (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) . 5 = IncAddr (i6,5)
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for i1, i2, i3, i4, i5, i6 being No-StopCode Instruction of S holds (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) . 5 = IncAddr (i6,5)
let i1, i2, i3, i4, i5, i6 be No-StopCode Instruction of S; ::_thesis: (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) . 5 = IncAddr (i6,5)
 LastLoc ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) = 5 by Th34;
hence  (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) . 5 = IncAddr (i6,5) by Th50; ::_thesis: verum
end;

definition
let S be with_non_trivial_Instructions COM-Struct ;
let I be preProgram of S;
attrI is closed  means :Def5: :: COMPOS_2:def 5
 for i being Instruction of S st i in rng I holds
rng (JumpPart i) c= dom I;
end;

:: deftheorem Def5 defines closed COMPOS_2:def_5_:_
 for S being with_non_trivial_Instructions COM-Struct
for I being preProgram of S holds
( I is closed iff for i being Instruction of S st i in rng I holds
rng (JumpPart i) c= dom I );

registration
let S be with_non_trivial_Instructions COM-Struct ;
cluster Stop S ->  closed ;
coherence
 Stop S is closed
proof
let i be Instruction of S; :: according to COMPOS_2:def_5 ::_thesis: ( i in rng (Stop S) implies rng (JumpPart i) c= dom (Stop S) )
assume Z: i in rng (Stop S) ; ::_thesis: rng (JumpPart i) c= dom (Stop S)
 rng (Stop S) = {(halt S)} by AFINSQ_1:33;
then  i = halt S by Z, TARSKI:def_1;
then  rng (JumpPart i) = {} ;
hence  rng (JumpPart i) c= dom (Stop S) by XBOOLE_1:2; ::_thesis: verum
end;
end;

registration
let S be with_non_trivial_Instructions COM-Struct ;
cluster non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt closed for set ;
existence
 ex b1 being MacroInstruction of S st b1 is closed
proof
take  Stop S ; ::_thesis: Stop S is closed
thus  Stop S is closed ; ::_thesis: verum
end;
end;

theorem :: COMPOS_2:61
for S being with_non_trivial_Instructions COM-Struct
for i being No-StopCode Instruction of S st i is ins-loc-free holds
Macro i is closed
proof
let S be with_non_trivial_Instructions COM-Struct ; ::_thesis: for i being No-StopCode Instruction of S st i is ins-loc-free holds
Macro i is closed
let i be No-StopCode Instruction of S; ::_thesis: ( i is ins-loc-free implies Macro i is closed )
assume Z: i is ins-loc-free ; ::_thesis: Macro i is closed
let i1 be Instruction of S; :: according to COMPOS_2:def_5 ::_thesis: ( i1 in rng (Macro i) implies rng (JumpPart i1) c= dom (Macro i) )
assume  i1 in rng (Macro i) ; ::_thesis: rng (JumpPart i1) c= dom (Macro i)
then  i1 in {i,(halt S)} by COMPOS_1:67;
then  ( i1 = i or i1 = halt S ) by TARSKI:def_2;
then  rng (JumpPart i1) = {} by Z;
hence  rng (JumpPart i1) c= dom (Macro i) by XBOOLE_1:2; ::_thesis: verum
end;

registration
let S be with_non_trivial_Instructions COM-Struct ;
let I be closed MacroInstruction of S;
let k be Nat;
cluster Reloc (I,k) ->  closed ;
coherence
 Reloc (I,k) is closed
proof
let i be Instruction of S; :: according to COMPOS_2:def_5 ::_thesis: ( i in rng (Reloc (I,k)) implies rng (JumpPart i) c= dom (Reloc (I,k)) )
assume  i in rng (Reloc (I,k)) ; ::_thesis: rng (JumpPart i) c= dom (Reloc (I,k))
then consider n being set  such that
W1: n in dom (Reloc (I,k)) and
W2: (Reloc (I,k)) . n = i by FUNCT_1:def_3;
 dom (Reloc (I,k)) c= NAT by RELAT_1:def_18;
then reconsider n = n as Nat by W1;
B: dom (Reloc (I,k)) = dom (Shift (I,k)) by COMPOS_1:32;
then consider j being Nat such that
W3: j in dom I and
W4: n = j + k by W1, VALUED_1:39;
 I . j = I /. j by W3, PARTFUN1:def_6;
then reconsider i1 = I . j as Instruction of S ;
A: IncAddr (i1,k) = i by W2, W3, W4, COMPOS_1:35;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (JumpPart i) or x in dom (Reloc (I,k)) )
assume C: x in rng (JumpPart i) ; ::_thesis: x in dom (Reloc (I,k))
then consider y being set  such that
W5: y in dom (JumpPart i) and
W6: (JumpPart i) . y = x by FUNCT_1:def_3;
 dom (JumpPart i) c= NAT by RELAT_1:def_18;
then reconsider y = y as Nat by W5;
H: JumpPart i = (JumpPart i1) + k by A, COMPOS_0:def_9;
then E: dom (JumpPart i) = dom (JumpPart i1) by VALUED_1:def_2;
 rng (JumpPart i) c= NAT by RELAT_1:def_19;
then reconsider m = x as Nat by C;
reconsider n = (JumpPart i1) . y as Nat ;
D: m = n + k by W6, H, W5, VALUED_1:def_2;
G: n in rng (JumpPart i1) by W5, E, FUNCT_1:3;
 i1 in rng I by W3, FUNCT_1:3;
then  rng (JumpPart i1) c= dom I by Def5;
hence  x in dom (Reloc (I,k)) by B, D, G, VALUED_1:24; ::_thesis: verum
end;
end;

registration
let S be with_non_trivial_Instructions COM-Struct ;
let I, J be closed MacroInstruction of S;
clusterI ';' J ->  closed ;
coherence
 I ';' J is closed
proof
let i be Instruction of S; :: according to COMPOS_2:def_5 ::_thesis: ( i in rng (I ';' J) implies rng (JumpPart i) c= dom (I ';' J) )
assume Z: i in rng (I ';' J) ; ::_thesis: rng (JumpPart i) c= dom (I ';' J)
 rng (I ';' J) c= (rng (CutLastLoc I)) \/ (rng (Reloc (J,((card I) -' 1)))) by FUNCT_4:17;
percasesthen  ( i in rng (CutLastLoc I) or i in rng (Reloc (J,((card I) -' 1))) ) by Z, XBOOLE_0:def_3;
supposeS: i in rng (CutLastLoc I) ; ::_thesis: rng (JumpPart i) c= dom (I ';' J)
 rng (CutLastLoc I) c= rng I by RELAT_1:11;
then A: rng (JumpPart i) c= dom I by S, Def5;
 dom I c= dom (I ';' J) by COMPOS_1:21;
hence  rng (JumpPart i) c= dom (I ';' J) by A, XBOOLE_1:1; ::_thesis: verum
end;
suppose i in rng (Reloc (J,((card I) -' 1))) ; ::_thesis: rng (JumpPart i) c= dom (I ';' J)
then A: rng (JumpPart i) c= dom (Reloc (J,((card I) -' 1))) by Def5;
 dom (Reloc (J,((card I) -' 1))) c= dom (I ';' J) by FUNCT_4:10;
hence  rng (JumpPart i) c= dom (I ';' J) by A, XBOOLE_1:1; ::_thesis: verum
end;
end;
end;
end;