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

coherence

Result ((P +* I),(Initialized s)) is State of SCM+FSA ;

end;
let s be State of SCM+FSA;

let P be Instruction-Sequence of SCM+FSA;

coherence

Result ((P +* I),(Initialized s)) is State of SCM+FSA ;

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

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

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

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

ex b_{1} being Program of st

( b_{1} is parahalting & b_{1} is keeping_0 )
end;

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 b

( b

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

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

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;

registration

for b_{1} being Program of st b_{1} is parahalting holds

b_{1} is paraclosed

for b_{1} being Program of st b_{1} is keeping_0 holds

b_{1} is paraclosed
end;

cluster Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() parahalting -> paraclosed for set ;

coherence for b

b

proof end;

cluster Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() keeping_0 -> paraclosed for set ;

coherence for b

b

proof 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

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

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 parahalting Program of st not f in UsedInt*Loc I holds

(IExec (I,P,s)) . f = s . f

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

proof end;

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

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

for b_{1} being Program of st b_{1} is parahalting holds

not b_{1} is empty
;

end;

cluster Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() parahalting -> for set ;

coherence for b

not b

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

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

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

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

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 parahalting Program of st I c= P1 & I c= P2 holds

( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) )

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

proof end;

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

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;

begin

registration

ex b_{1} being Program of st b_{1} is paraclosed
end;

cluster Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() paraclosed V144() for set ;

existence ex b

proof 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)

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)

proof end;

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 & Directed I c= P holds

IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I

for P being Instruction-Sequence of SCM+FSA

for I being paraclosed 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 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 & Directed I c= P holds

DataPart (Comput (P,s,(LifeSpan ((P +* I),s)))) = DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1)))

for P being Instruction-Sequence of SCM+FSA

for I being paraclosed 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 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 & 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

for P being Instruction-Sequence of SCM+FSA

for I being parahalting Program of st I c= P & 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

proof end;

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)

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)

proof end;

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

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)

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)

proof end;

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

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

proof 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)))))

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

proof end;

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

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

proof end;

theorem :: SCMFSA6B:21