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


begin

registration
cluster with_non_trivial_Instructions for COM-Struct ;
existence
 ex b1 being COM-Struct st b1 is with_non_trivial_Instructions
proofend;
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
proofend;
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 )
proofend;
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
proofend;

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

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

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

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

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

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

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

theorem Th17: :: COMPOS_2:17
for F being non empty NAT -defined finite Function holds not LastLoc F in dom (CutLastLoc F)
proofend;

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

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

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 &amp; J <= K holds
I <= K
proofend;

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

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

theorem :: COMPOS_2:22
for S being with_non_trivial_Instructions COM-Struct
for I, J being MacroInstruction of S st I <= J &amp; J <= I holds
I = J
proofend;

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

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

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

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

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

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 &amp; I <= J holds
I . k = J . k
proofend;

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

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

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

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

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

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

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

:: dla zerowej pozycji nie mamy inkrementpwania adresow.
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
proofend;

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

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

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

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

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

::theorem :: COMPOS_1:23
:: for S being COM-Struct,
:: F, G being initial non empty finite preProgram of S
:: holds (F ';' G).LastLoc F = IncAddr(G,card F -' 1).0;
::theorem :: COMPOS_1:24
:: for S being COM-Struct,
:: F, G being initial non empty finite preProgram of S,
:: f being Nat st f < card F - 1
:: holds IncAddr(F,card F -' 1).f = IncAddr(F ';' G, card F -' 1).f;
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
proofend;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

:: Zeby moc mowic o tym, ze Reloc(I,k) jest closed
:: trzebaby ten atrybut zdefiniowac ogolniej
:: ale wtedy trzeba wykorzystac fakt, ze sekwencyjnie
:: przejscie nie moze sie cofac. Czyli maszyna
:: musi byc standard.
:: Potrzeba nam wiec raczej to, ze tak psedomakroinstrukcja
:: jest "contigious" a niekoniecznie "initial"
:: Definicje moze bez trudu zrobic ogolniejsza.
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
proofend;
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
proofend;
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
proofend;

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