:: On the compositions of macro instructions
:: by Andrzej Trybulec , Yatsuka Nakamura and Noriko Asamoto
::
:: Received June 20, 1996
:: Copyright (c) 1996-2012 Association of Mizar Users


begin

definition
let P be NAT -defined the InstructionsF of SCM+FSA -valued finite Function;
let l be Element of NAT ;
func Directed (P,l) ->  preProgram of SCM+FSA equals :: SCMFSA6A:def 1
P +~ ((halt SCM+FSA),(goto l));
coherence
 P +~ ((halt SCM+FSA),(goto l)) is preProgram of SCM+FSA ;
end;

:: deftheorem  defines Directed SCMFSA6A:def_1_:_
 for P being NAT -defined the InstructionsF of SCM+FSA -valued finite Function
for l being Element of NAT holds Directed (P,l) = P +~ ((halt SCM+FSA),(goto l));

definition
let P be NAT -defined the InstructionsF of SCM+FSA -valued finite Function;
func Directed P ->  preProgram of SCM+FSA equals :: SCMFSA6A:def 2
 Directed (P,(card P));
coherence
 Directed (P,(card P)) is preProgram of SCM+FSA ;
end;

:: deftheorem  defines Directed SCMFSA6A:def_2_:_
 for P being NAT -defined the InstructionsF of SCM+FSA -valued finite Function holds Directed P = Directed (P,(card P));

registration
let I be Program of ;
cluster Directed I ->  non empty initial ;
coherence
 ( Directed I is initial & not Directed I is empty )
proofend;
end;

theorem :: SCMFSA6A:1
for I being Program of holds not halt SCM+FSA in rng (Directed I) by FUNCT_4:100;

theorem :: SCMFSA6A:2
for m being Element of NAT
for I being Program of holds Reloc ((Directed I),m) = ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto (m + (card I))))) * (Reloc (I,m))
proofend;

set q = (intloc 0) .--> 1;

set f = the_Values_of SCM+FSA;

theorem Th23: :: SCMFSA6A:3
for i being Instruction of SCM+FSA
for s being State of SCM+FSA holds
( InsCode i in {0,6,7,8} or (Exec (i,s)) . (IC ) = succ (IC s) )
proofend;

theorem :: SCMFSA6A:4
canceled;

theorem :: SCMFSA6A:5
canceled;

theorem :: SCMFSA6A:6
canceled;

theorem :: SCMFSA6A:7
canceled;

theorem :: SCMFSA6A:8
for s1, s2 being State of SCM+FSA
for n being Element of NAT
for i being Instruction of SCM+FSA st (IC s1) + n = IC s2 & DataPart s1 = DataPart s2 holds
( (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) & DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) )
proofend;

theorem :: SCMFSA6A:9
canceled;

theorem :: SCMFSA6A:10
canceled;

theorem :: SCMFSA6A:11
canceled;

theorem :: SCMFSA6A:12
canceled;

theorem :: SCMFSA6A:13
canceled;

theorem :: SCMFSA6A:14
canceled;

begin

definition
canceled;
let I, J be Program of ;
funcI ";" J ->  Program of  equals :: SCMFSA6A:def 4
(Directed (CutLastLoc (stop I))) +* (Reloc (J,(card I)));
coherence
 (Directed (CutLastLoc (stop I))) +* (Reloc (J,(card I))) is Program of
proofend;
correctness
;
end;

:: deftheorem  SCMFSA6A:def_3_:_
canceled;

:: deftheorem  defines ";" SCMFSA6A:def_4_:_
 for I, J being Program of holds I ";" J = (Directed (CutLastLoc (stop I))) +* (Reloc (J,(card I)));

registration
let I be Program of ;
let J be non halt-free Program of ;
clusterI ";" J ->  non halt-free ;
coherence
 not I ";" J is halt-free ;
end;

theorem :: SCMFSA6A:15
for I, J being Program of
for l being Element of NAT st l in dom I &amp; I . l <> halt SCM+FSA holds
(I ";" J) . l = I . l
proofend;

theorem :: SCMFSA6A:16
for I, J being Program of holds Directed I c= I ";" J
proofend;

theorem Th56: :: SCMFSA6A:17
for I, J being Program of holds dom I c= dom (I ";" J)
proofend;

theorem :: SCMFSA6A:18
for I, J being Program of holds I +* (I ";" J) = I ";" J
proofend;

begin

definition
let i be Instruction of SCM+FSA;
let J be Program of ;
funci ";" J ->  Program of  equals :: SCMFSA6A:def 5
(Macro i) ";" J;
correctness
coherence
(Macro i) ";" J is Program of ;
;
end;

:: deftheorem  defines ";" SCMFSA6A:def_5_:_
 for i being Instruction of SCM+FSA
for J being Program of holds i ";" J = (Macro i) ";" J;

definition
let I be Program of ;
let j be Instruction of SCM+FSA;
funcI ";" j ->  Program of  equals :: SCMFSA6A:def 6
I ";" (Macro j);
correctness
coherence
I ";" (Macro j) is Program of ;
;
end;

:: deftheorem  defines ";" SCMFSA6A:def_6_:_
 for I being Program of
for j being Instruction of SCM+FSA holds I ";" j = I ";" (Macro j);

definition
let i, j be Instruction of SCM+FSA;
funci ";" j ->  Program of  equals :: SCMFSA6A:def 7
(Macro i) ";" (Macro j);
correctness
coherence
(Macro i) ";" (Macro j) is Program of ;
;
end;

:: deftheorem  defines ";" SCMFSA6A:def_7_:_
 for i, j being Instruction of SCM+FSA holds i ";" j = (Macro i) ";" (Macro j);

theorem :: SCMFSA6A:19
for i, j being Instruction of SCM+FSA holds i ";" j = (Macro i) ";" j ;

theorem :: SCMFSA6A:20
for i, j being Instruction of SCM+FSA holds i ";" j = i ";" (Macro j) ;

theorem Th61: :: SCMFSA6A:21
for I, J being Program of holds card (I ";" J) = (card I) + (card J)
proofend;

registration
let P be preProgram of SCM+FSA;
let l be Element of NAT ;
cluster Directed (P,l) ->  halt-free ;
correctness
coherence
Directed (P,l) is halt-free ;
proofend;
end;

registration
let P be preProgram of SCM+FSA;
cluster Directed P ->  halt-free ;
correctness
coherence
Directed P is halt-free ;
;
end;

theorem Th63: :: SCMFSA6A:22
for I being preProgram of SCM+FSA
for l being Element of NAT st I is halt-free holds
Directed (I,l) = I
proofend;

theorem Th65: :: SCMFSA6A:23
for I being preProgram of SCM+FSA
for k being Element of NAT holds Reloc ((Directed I),k) = Directed ((Reloc (I,k)),((card I) + k))
proofend;

theorem Th66: :: SCMFSA6A:24
for I, J being Program of holds Directed (I ";" J) = I ";" (Directed J)
proofend;

theorem Th67: :: SCMFSA6A:25
for I, J, K being Program of holds (I ";" J) ";" K = I ";" (J ";" K)
proofend;

theorem :: SCMFSA6A:26
for k being Instruction of SCM+FSA
for I, J being Program of holds (I ";" J) ";" k = I ";" (J ";" k) by Th67;

theorem :: SCMFSA6A:27
for j being Instruction of SCM+FSA
for I, K being Program of holds (I ";" j) ";" K = I ";" (j ";" K) by Th67;

theorem :: SCMFSA6A:28
for j, k being Instruction of SCM+FSA
for I being Program of holds (I ";" j) ";" k = I ";" (j ";" k) by Th67;

theorem :: SCMFSA6A:29
for i being Instruction of SCM+FSA
for J, K being Program of holds (i ";" J) ";" K = i ";" (J ";" K) by Th67;

theorem :: SCMFSA6A:30
for i, k being Instruction of SCM+FSA
for J being Program of holds (i ";" J) ";" k = i ";" (J ";" k) by Th67;

theorem :: SCMFSA6A:31
for i, j being Instruction of SCM+FSA
for K being Program of holds (i ";" j) ";" K = i ";" (j ";" K) by Th67;

theorem :: SCMFSA6A:32
for i, j, k being Instruction of SCM+FSA holds (i ";" j) ";" k = i ";" (j ";" k) by Th67;

theorem :: SCMFSA6A:33
for i being Instruction of SCM+FSA
for J being Program of holds card (i ";" J) = (card J) + 2
proofend;

theorem :: SCMFSA6A:34
for j being Instruction of SCM+FSA
for I being Program of holds card (I ";" j) = (card I) + 2
proofend;

theorem :: SCMFSA6A:35
for i, j being Instruction of SCM+FSA holds card (i ";" j) = 4
proofend;