:: 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-2019 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),());
coherence
Result ((P +* I),()) 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),());

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)) . () = s . (); 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)) . () = s . () ); registration coherence proof end; end; registration 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 (() .--> 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 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)) . () = 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 (() .--> 1) c= s holds
for k being Nat st k <= LifeSpan (P,s) holds
CurInstr ((P +* ()),(Comput ((P +* ()),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 (() .--> 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 (() .--> 1))) & Reloc (J,(card I)) c= P & (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) . () = 1 & P halts_on s & LifeSpan (P,s) = ((LifeSpan ((P +* I),s)) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),s)) +* (Initialize (() .--> 1))))) & ( J is keeping_0 implies (Result (P,s)) . () = 1 ) )

proof end;

registration
let I, J be really-closed parahalting Program of ;
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 (() .--> 1)))) = ((LifeSpan ((P +* I),(s +* (Initialize (() .--> 1))))) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize (() .--> 1))))) +* (Initialize (() .--> 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;