:: by Andrzej Trybulec

::

:: Received October 1, 2011

:: Copyright (c) 2011-2016 Association of Mizar Users

registration
end;

registration

let S be with_non_trivial_Instructions COM-Struct ;

existence

ex b_{1} being Instruction of S st b_{1} is No-StopCode

end;
existence

ex b

proof end;

registration

let S be with_non_trivial_Instructions COM-Struct ;

let i be No-StopCode Instruction of S;

coherence

( Macro i is halt-ending & Macro i is unique-halt )

end;
let i be No-StopCode Instruction of S;

coherence

( Macro i is halt-ending & Macro i is unique-halt )

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

correctness

coherence

(Macro i) ';' J is MacroInstruction of S;

;

end;
let i be No-StopCode Instruction of S;

let J be MacroInstruction of S;

correctness

coherence

(Macro i) ';' J is MacroInstruction of S;

;

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

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;

correctness

coherence

I ';' (Macro j) is MacroInstruction of S;

;

end;
let I be MacroInstruction of S;

let j be No-StopCode Instruction of S;

correctness

coherence

I ';' (Macro j) is MacroInstruction of S;

;

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

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;

correctness

coherence

(Macro i) ';' (Macro j) is MacroInstruction of S;

;

end;
let i, j be No-StopCode Instruction of S;

correctness

coherence

(Macro i) ';' (Macro j) is MacroInstruction of S;

;

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

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;

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;

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;

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;

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;

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;

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;

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 ;

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

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

for i being No-StopCode Instruction of S

for J being MacroInstruction of S holds card (i ';' J) = (card J) + 1

proof 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

for j being No-StopCode Instruction of S

for I being MacroInstruction of S holds card (I ';' j) = (card I) + 1

proof 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

for i, j being No-StopCode Instruction of S holds card (i ';' j) = 3

proof 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

for i, j, k being No-StopCode Instruction of S holds card ((i ';' j) ';' k) = 4

proof 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

for i1, i2, i3, i4 being No-StopCode Instruction of S holds card (((i1 ';' i2) ';' i3) ';' i4) = 5

proof 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

for i1, i2, i3, i4, i5 being No-StopCode Instruction of S holds card ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) = 6

proof 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

for i1, i2, i3, i4, i5, i6 being No-StopCode Instruction of S holds card (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) = 7

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

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 pred I <= J;

reflexivity

for I being non empty NAT -defined finite Function holds (b_{1},b_{1})
;

end;
:: original: <=

redefine pred I <= J;

reflexivity

for I being non empty NAT -defined finite Function holds (b

registration

let S be with_non_trivial_Instructions COM-Struct ;

let I be non empty unique-halt preProgram of S;

coherence

CutLastLoc I is halt-free

end;
let I be non empty unique-halt preProgram of S;

coherence

CutLastLoc I is halt-free

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

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

for I, J being MacroInstruction of S

for K being set st I <= J & J <= K holds

I <= K

proof end;

theorem Th20: :: COMPOS_2:20

for S being with_non_trivial_Instructions COM-Struct

for I being halt-ending Program of S holds I = (CutLastLoc I) +* ((LastLoc I) .--> (halt S))

for I being halt-ending Program of S holds I = (CutLastLoc I) +* ((LastLoc I) .--> (halt S))

proof end;

theorem Th21: :: COMPOS_2:21

for S being with_non_trivial_Instructions COM-Struct

for J being MacroInstruction of S

for I being halt-ending Program of S st CutLastLoc I = CutLastLoc J holds

I = J

for J being MacroInstruction of S

for I being halt-ending Program of S st CutLastLoc I = CutLastLoc J holds

I = J

proof 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

for I, J being MacroInstruction of S st I <= J & J <= I holds

I = J

proof 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

for I, J being MacroInstruction of S holds I <= I ';' J

proof end;

:: Potrzebne chyba beda trywialne twierdzenia, jak

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

for I being MacroInstruction of S

for X being set st I c= X holds

I <= X

proof 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

for I, J being MacroInstruction of S st I <= J holds

for X being set st J c= X holds

I <= X

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

for I being MacroInstruction of S

for k being Nat holds

( k < LastLoc I iff k in dom (CutLastLoc I) )

proof 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

for I being MacroInstruction of S

for k being Nat st k < LastLoc I holds

(CutLastLoc I) . k = I . k

proof 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

for I, J being MacroInstruction of S

for k being Nat st k < LastLoc I & I <= J holds

I . k = J . k

proof end;

::$CT

theorem Th29: :: 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

for i being No-StopCode Instruction of S holds LastLoc (Macro i) = 1

proof end;

theorem Th30: :: 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

for i, j being No-StopCode Instruction of S holds LastLoc (i ';' j) = 2

proof end;

theorem Th31: :: 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

for i, j, k being No-StopCode Instruction of S holds LastLoc ((i ';' j) ';' k) = 3

proof end;

theorem Th32: :: 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

for i1, i2, i3, i4 being No-StopCode Instruction of S holds LastLoc (((i1 ';' i2) ';' i3) ';' i4) = 4

proof end;

theorem Th33: :: 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

for i1, i2, i3, i4, i5 being No-StopCode Instruction of S holds LastLoc ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) = 5

proof end;

theorem Th34: :: 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

for i1, i2, i3, i4, i5, i6 being No-StopCode Instruction of S holds LastLoc (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) = 6

proof end;

:: dla zerowej pozycji nie mamy inkrementpwania adresow.

theorem Th35: :: 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

for i being No-StopCode Instruction of S

for J being MacroInstruction of S holds (i ';' J) . 0 = i

proof end;

theorem Th36: :: 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

for i, j being No-StopCode Instruction of S

for K being MacroInstruction of S holds ((i ';' j) ';' K) . 0 = i

proof end;

theorem Th37: :: 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

for i, j, k being No-StopCode Instruction of S

for K being MacroInstruction of S holds (((i ';' j) ';' k) ';' K) . 0 = i

proof end;

theorem Th38: :: 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

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

theorem Th39: :: 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

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

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

for I, J being MacroInstruction of S

for k being Nat st k < LastLoc I holds

(I ';' J) . k = I . k

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

for I, J being MacroInstruction of S holds LastLoc (I ';' J) = (LastLoc I) + (LastLoc J)

proof end;

theorem Th43: :: COMPOS_2:44

for S being with_non_trivial_Instructions COM-Struct

for I, J being MacroInstruction of S

for j being Nat st j <= LastLoc J holds

(I ';' J) . ((LastLoc I) + j) = IncAddr ((J /. j),(LastLoc I))

for I, J being MacroInstruction of S

for j being Nat st j <= LastLoc J holds

(I ';' J) . ((LastLoc I) + j) = IncAddr ((J /. j),(LastLoc I))

proof end;

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

for i, j being No-StopCode Instruction of S holds (i ';' j) . 1 = IncAddr (j,1)

proof end;

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

for i, j, k being No-StopCode Instruction of S holds ((i ';' j) ';' k) . 1 = IncAddr (j,1)

proof end;

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

for i1, i2, i3, i4 being No-StopCode Instruction of S holds (((i1 ';' i2) ';' i3) ';' i4) . 1 = IncAddr (i2,1)

proof end;

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

for i1, i2, i3, i4, i5 being No-StopCode Instruction of S holds ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 1 = IncAddr (i2,1)

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

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

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

for j being No-StopCode Instruction of S

for I being MacroInstruction of S holds (I ';' j) . (LastLoc I) = IncAddr (j,(LastLoc I))

proof end;

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

for i1, i2, i3 being No-StopCode Instruction of S holds ((i1 ';' i2) ';' i3) . 2 = IncAddr (i3,2)

proof end;

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

for i1, i2, i3, i4 being No-StopCode Instruction of S holds (((i1 ';' i2) ';' i3) ';' i4) . 2 = IncAddr (i3,2)

proof end;

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

for i1, i2, i3, i4, i5 being No-StopCode Instruction of S holds ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 2 = IncAddr (i3,2)

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

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

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

for i1, i2, i3, i4 being No-StopCode Instruction of S holds (((i1 ';' i2) ';' i3) ';' i4) . 3 = IncAddr (i4,3)

proof end;

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

for i1, i2, i3, i4, i5 being No-StopCode Instruction of S holds ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 3 = IncAddr (i4,3)

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

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

for i1, i2, i3, i4, i5 being No-StopCode Instruction of S holds ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 4 = IncAddr (i5,4)

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

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

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

definition

let S be with_non_trivial_Instructions COM-Struct ;

let I be preProgram of S;

end;
let I be preProgram of S;

attr I 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;

for i being Instruction of S st i in rng I holds

rng (JumpPart i) c= dom I;

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

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

registration

let S be with_non_trivial_Instructions COM-Struct ;

ex b_{1} being MacroInstruction of S st b_{1} is closed

end;
cluster non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like V28() finite V49() non halt-free halt-ending unique-halt closed for set ;

existence ex b

proof end;

:: Nie mozemy bez dodatkowych zalozen zarejestrowac

:: ins-loc-free No-StopCode dowodzimy twierdzenie

:: rejestracje mozna zrobic dla konkretnych komputerow.

:: ins-loc-free No-StopCode dowodzimy twierdzenie

:: rejestracje mozna zrobic dla konkretnych komputerow.

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

for i being No-StopCode Instruction of S st i is ins-loc-free holds

Macro i is closed

proof end;

registration

let S be with_non_trivial_Instructions COM-Struct ;

let I be closed MacroInstruction of S;

let k be Nat;

coherence

Reloc (I,k) is closed

end;
let I be closed MacroInstruction of S;

let k be Nat;

coherence

Reloc (I,k) is closed

proof end;

registration

let S be with_non_trivial_Instructions COM-Struct ;

let I, J be closed MacroInstruction of S;

coherence

I ';' J is closed

end;
let I, J be closed MacroInstruction of S;

coherence

I ';' J is closed

proof end;

registration

let S be with_non_trivial_Instructions COM-Struct ;

ex b_{1} being Program of S st b_{1} is halt-free

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

existence ex b

proof end;

registration

let S be with_non_trivial_Instructions COM-Struct ;

let I, J be halt-free Program of S;

coherence

I ^ J is halt-free

end;
let I, J be halt-free Program of S;

coherence

I ^ J is halt-free

proof end;

registration

let S be with_non_trivial_Instructions COM-Struct ;

let i be No-StopCode Instruction of S;

coherence

Load i is halt-free

end;
let i be No-StopCode Instruction of S;

coherence

Load i is halt-free

proof end;