:: On the compositions of macro instructions, Part II
:: by Noriko Asamoto , Yatsuka Nakamura , Piotr Rudnicki and Andrzej Trybulec
::
:: Received July 22, 1996
:: Copyright (c) 1996-2012 Association of Mizar Users


begin

set SA0 = Start-At (0,SCM+FSA);

definition
let I be Program of ;
let s be State of SCM+FSA;
let P be Instruction-Sequence of SCM+FSA;
func IExec (I,P,s) ->  State of SCM+FSA equals :: SCMFSA6B:def 1
 Result ((P +* I),(Initialized s));
coherence
 Result ((P +* I),(Initialized s)) is State of SCM+FSA ;
end;

:: deftheorem  defines IExec SCMFSA6B:def_1_:_
 for I being Program of
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds IExec (I,P,s) = Result ((P +* I),(Initialized s));

definition
let I be Program of ;
canceled;
canceled;
attrI is keeping_0  means :Def4: :: SCMFSA6B:def 4
 for s being 0 -started State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st I c= P holds
for k being Element of NAT holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0);
end;

:: deftheorem  SCMFSA6B:def_2_:_
canceled;

:: deftheorem  SCMFSA6B:def_3_:_
canceled;

:: deftheorem Def4 defines keeping_0 SCMFSA6B:def_4_:_
 for I being Program of holds
( I is keeping_0 iff for s being 0 -started State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st I c= P holds
for k being Element of NAT holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) );

registration
cluster Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() parahalting V144() keeping_0 for set ;
existence
 ex b1 being Program of st
( b1 is parahalting & b1 is keeping_0 )
proofend;
end;

theorem Th1: :: SCMFSA6B:1
for s being 0 -started State of SCM+FSA
for I being parahalting Program of
for P being Instruction-Sequence of SCM+FSA st I c= P holds
P halts_on s by AMISTD_1:def_11;

theorem Th2: :: SCMFSA6B:2
for s being State of SCM+FSA
for I being parahalting Program of st Initialize ((intloc 0) .--> 1) c= s holds
for P being Instruction-Sequence of SCM+FSA st I c= P holds
P halts_on s
proofend;

Lm1:  for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds not P +* ((IC s),(goto (IC s))) halts_on s
proofend;

registration
cluster Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() parahalting  ->  paraclosed for set ;
coherence
 for b1 being Program of st b1 is parahalting holds
b1 is paraclosed
proofend;
cluster Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() keeping_0  ->  paraclosed for set ;
coherence
 for b1 being Program of st b1 is keeping_0 holds
b1 is paraclosed
proofend;
end;

theorem :: SCMFSA6B:3
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being parahalting Program of
for a being read-write Int-Location st not a in UsedIntLoc I holds
(IExec (I,P,s)) . a = s . a
proofend;

theorem :: SCMFSA6B:4
for f being FinSeq-Location
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being parahalting Program of st not f in UsedInt*Loc I holds
(IExec (I,P,s)) . f = s . f
proofend;

theorem :: SCMFSA6B:5
for l being Element of NAT
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st IC s = l & P . l = goto l holds
not P halts_on s
proofend;

registration
cluster Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() parahalting  ->  for set ;
coherence
 for b1 being Program of st b1 is parahalting holds
not b1 is empty ;
end;

theorem Th6: :: SCMFSA6B:6
for s2 being State of SCM+FSA
for s1 being 0 -started State of SCM+FSA
for P, Q being Instruction-Sequence of SCM+FSA
for J being parahalting Program of st J c= P holds
for n being Element of NAT st Reloc (J,n) c= Q & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( (IC (Comput (P,s1,i))) + n = IC (Comput (Q,s2,i)) & IncAddr ((CurInstr (P,(Comput (P,s1,i)))),n) = CurInstr (Q,(Comput (Q,s2,i))) & DataPart (Comput (P,s1,i)) = DataPart (Comput (Q,s2,i)) )
proofend;

theorem Th7: :: SCMFSA6B:7
for P1, P2 being Instruction-Sequence of SCM+FSA
for s being 0 -started State of SCM+FSA
for I being parahalting Program of st I c= P1 & I c= P2 holds
for k being Element of NAT holds
( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) )
proofend;

theorem Th8: :: SCMFSA6B:8
for P1, P2 being Instruction-Sequence of SCM+FSA
for s being 0 -started State of SCM+FSA
for I being parahalting Program of st I c= P1 & I c= P2 holds
( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) )
proofend;

theorem :: SCMFSA6B:9
canceled;

theorem :: SCMFSA6B:10
canceled;

theorem :: SCMFSA6B:11
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being parahalting keeping_0 Program of holds (IExec (I,P,s)) . (intloc 0) = 1
proofend;

begin

registration
cluster Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() paraclosed V144() for set ;
existence
 ex b1 being Program of st b1 is paraclosed
proofend;
end;

theorem Th12: :: SCMFSA6B:12
for s being 0 -started State of SCM+FSA
for I being paraclosed Program of
for J being Program of
for P being Instruction-Sequence of SCM+FSA st I c= P & P halts_on s holds
for m being Element of NAT st m <= LifeSpan (P,s) holds
Comput (P,s,m) = Comput ((P +* (I ";" J)),s,m)
proofend;

theorem Th13: :: SCMFSA6B:13
for s being 0 -started State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being paraclosed Program of st P +* I halts_on s &amp; Directed I c= P holds
IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I
proofend;

theorem Th14: :: SCMFSA6B:14
for s being 0 -started State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being paraclosed Program of st P +* I halts_on s &amp; Directed I c= P holds
DataPart (Comput (P,s,(LifeSpan ((P +* I),s)))) = DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1)))
proofend;

theorem Th15: :: SCMFSA6B:15
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being parahalting Program of st I c= P &amp; Initialize ((intloc 0) .--> 1) c= s holds
for k being Element of NAT st k <= LifeSpan (P,s) holds
CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),s,k))) <> halt SCM+FSA
proofend;

theorem Th16: :: SCMFSA6B:16
for s being 0 -started State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being paraclosed Program of st P +* I halts_on s holds
for J being Program of
for k being Element of NAT st k <= LifeSpan ((P +* I),s) holds
Comput ((P +* I),s,k) = Comput ((P +* (I ";" J)),s,k)
proofend;

Lm2:  for P being Instruction-Sequence of SCM+FSA
for I being parahalting keeping_0 Program of
for J being parahalting Program of
for s being State of SCM+FSA st I ";" J c= P &amp; Initialize ((intloc 0) .--> 1) c= s holds
( IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I &amp; DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = DataPart ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) &amp; Reloc (J,(card I)) c= P &amp; (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) . (intloc 0) = 1 &amp; P halts_on s &amp; LifeSpan (P,s) = ((LifeSpan ((P +* I),s)) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),s)) +* (Initialize ((intloc 0) .--> 1))))) &amp; ( J is keeping_0 implies (Result (P,s)) . (intloc 0) = 1 ) )
proofend;

registration
let I, J be parahalting Program of ;
clusterI ";" J ->  parahalting ;
coherence
 I ";" J is parahalting
proofend;
end;

theorem Th17: :: SCMFSA6B:17
for P being Instruction-Sequence of SCM+FSA
for s being 0 -started State of SCM+FSA
for I being keeping_0 Program of st not P +* I halts_on s holds
for J being Program of
for k being Element of NAT holds Comput ((P +* I),s,k) = Comput ((P +* (I ";" J)),s,k)
proofend;

theorem Th18: :: SCMFSA6B:18
for P being Instruction-Sequence of SCM+FSA
for s being 0 -started State of SCM+FSA
for I being keeping_0 Program of st P +* I halts_on s holds
for J being paraclosed Program of st I ";" J c= P holds
for k being Element of NAT holds IncIC ((Comput (((P +* I) +* J),(Initialize (Result ((P +* I),s))),k)),(card I)) = Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + k))
proofend;

registration
let I, J be keeping_0 Program of ;
clusterI ";" J ->  keeping_0 ;
coherence
 I ";" J is keeping_0
proofend;
end;

theorem Th19: :: SCMFSA6B:19
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being parahalting keeping_0 Program of
for J being parahalting Program of holds LifeSpan ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1)))) = ((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)))))
proofend;

theorem :: SCMFSA6B:20
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being parahalting keeping_0 Program of
for J being parahalting Program of holds IExec ((I ";" J),P,s) = IncIC ((IExec (J,P,(IExec (I,P,s)))),(card I))
proofend;

theorem :: SCMFSA6B:21
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds not P +* ((IC s),(goto (IC s))) halts_on s by Lm1;