:: 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-2021 Association of Mizar Users


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 ;
::$CD 2
attr I is keeping_0 means :Def2: :: 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 Nat holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0);
end;

:: deftheorem SCMFSA6B:def 2 :
canceled;

:: deftheorem SCMFSA6B:def 3 :
canceled;

:: deftheorem Def2 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 Nat holds (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) );

registration
cluster Stop SCM+FSA -> parahalting keeping_0 ;
coherence
( Stop SCM+FSA is parahalting & Stop SCM+FSA is keeping_0 )
proof end;
end;

registration
cluster Relation-like NAT -defined the InstructionsF of SCM+FSA -valued V13() non empty Function-like V37() V55() non halt-free halt-ending unique-halt really-closed parahalting V154() keeping_0 for set ;
existence
ex b1 being MacroInstruction of SCM+FSA st
( b1 is really-closed & b1 is parahalting & b1 is keeping_0 )
proof end;
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
proof end;

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

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

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 really-closed parahalting Program of st not f in UsedI*Loc I holds
(IExec (I,P,s)) . f = s . f
proof end;

theorem :: SCMFSA6B:5
for l being 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
proof end;

registration
cluster Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V37() V55() 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 really-closed parahalting Program of st J c= P holds
for n being Nat st Reloc (J,n) c= Q & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being 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)) )
proof end;

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 really-closed parahalting Program of st I c= P1 & I c= P2 holds
for k being Nat holds
( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) )
proof end;

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 really-closed parahalting Program of st I c= P1 & I c= P2 holds
( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) )
proof end;

theorem :: SCMFSA6B:9
canceled;

theorem :: SCMFSA6B:10
canceled;

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

theorem Th10: :: SCMFSA6B:12
for s being 0 -started State of SCM+FSA
for I being really-closed 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 Nat st m <= LifeSpan (P,s) holds
Comput (P,s,m) = Comput ((P +* (I ";" J)),s,m)
proof end;

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

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

theorem Th13: :: SCMFSA6B:15
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being really-closed parahalting Program of st I c= P & Initialize ((intloc 0) .--> 1) c= s holds
for k being Nat st k <= LifeSpan (P,s) holds
CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),s,k))) <> halt SCM+FSA
proof end;

theorem Th14: :: SCMFSA6B:16
for s being 0 -started State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being really-closed Program of st P +* I halts_on s holds
for J being Program of
for k being Nat st k <= LifeSpan ((P +* I),s) holds
Comput ((P +* I),s,k) = Comput ((P +* (I ";" J)),s,k)
proof end;

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

registration
let I, J be really-closed parahalting Program of ;
cluster I ";" J -> parahalting ;
coherence
I ";" J is parahalting
proof end;
end;

theorem Th15: :: SCMFSA6B:17
for P being Instruction-Sequence of SCM+FSA
for s being 0 -started State of SCM+FSA
for I being really-closed keeping_0 Program of st not P +* I halts_on s holds
for J being Program of
for k being Nat holds Comput ((P +* I),s,k) = Comput ((P +* (I ";" J)),s,k)
proof end;

theorem Th16: :: SCMFSA6B:18
for P being Instruction-Sequence of SCM+FSA
for s being 0 -started State of SCM+FSA
for I being really-closed keeping_0 Program of st P +* I halts_on s holds
for J being really-closed 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))
proof end;

registration
let I, J be really-closed keeping_0 Program of ;
cluster I ";" J -> keeping_0 ;
coherence
I ";" J is keeping_0
proof end;
end;

theorem Th17: :: SCMFSA6B:19
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being really-closed parahalting keeping_0 Program of
for J being really-closed 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)))))
proof end;

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

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;