:: The Elementary Macroinstructions
:: by Andrzej Trybulec
::
:: Received October 1, 2011
:: Copyright (c) 2011-2021 Association of Mizar Users


registration
cluster with_non_trivial_Instructions for COM-Struct ;
existence
ex b1 being COM-Struct st b1 is with_non_trivial_Instructions
proof 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 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 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;
func i ';' 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;
func I ';' 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;
func i ';' 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 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 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 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 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 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 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 end;

definition
let I be non empty NAT -defined finite Function;
let J be set ;
pred I <= 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 pred I <= J;
reflexivity
for I being non empty NAT -defined finite Function holds (b1,b1) ;
end;

theorem Th17: :: COMPOS_2:17
for F being non empty NAT -defined finite Function holds not LastLoc F in dom (CutLastLoc F)
proof 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 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 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 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 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))
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
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
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
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
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
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) )
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
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
proof end;

theorem :: COMPOS_2:29
canceled;

::$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
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
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
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
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
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
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
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
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
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
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
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
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
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)
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))
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)
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)
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)
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)
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)
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))
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
proof end;

definition
let S be with_non_trivial_Instructions COM-Struct ;
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;
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 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 V28() finite V49() non halt-free halt-ending unique-halt closed for set ;
existence
ex b1 being MacroInstruction of S st b1 is closed
proof end;
end;

:: Nie mozemy bez dodatkowych zalozen zarejestrowac
:: 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
proof 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 end;
end;

registration
let S be with_non_trivial_Instructions COM-Struct ;
let I, J be closed MacroInstruction of S;
cluster I ';' J -> closed ;
coherence
I ';' J is closed
proof 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 V28() finite V49() halt-free for set ;
existence
ex b1 being Program of S st b1 is halt-free
proof end;
end;

registration
let S be with_non_trivial_Instructions COM-Struct ;
let I, J be halt-free Program of S;
cluster I ^ J -> halt-free ;
coherence
I ^ J is halt-free
proof end;
end;

registration
let S be with_non_trivial_Instructions COM-Struct ;
let i be No-StopCode Instruction of S;
cluster Load -> halt-free ;
coherence
Load i is halt-free
proof end;
end;