:: by Noriko Asamoto

::

:: Received August 27, 1996

:: Copyright (c) 1996-2012 Association of Mizar Users

begin

set A = NAT ;

theorem :: SCMFSA7B:1

for i being Instruction of SCM+FSA holds

( ( i = halt SCM+FSA implies (Directed (Macro i)) . 0 = goto 2 ) & ( i <> halt SCM+FSA implies (Directed (Macro i)) . 0 = i ) )

( ( i = halt SCM+FSA implies (Directed (Macro i)) . 0 = goto 2 ) & ( i <> halt SCM+FSA implies (Directed (Macro i)) . 0 = i ) )

proof end;

registration

let a be Int-Location;

let k be Integer;

coherence

( a := k is initial & not a := k is empty & a := k is NAT -defined & a := k is the InstructionsF of SCM+FSA -valued )

end;
let k be Integer;

coherence

( a := k is initial & not a := k is empty & a := k is NAT -defined & a := k is the InstructionsF of SCM+FSA -valued )

proof end;

Lm1: for s being State of SCM+FSA st IC s = 0 holds

for P being Instruction-Sequence of SCM+FSA

for a being Int-Location

for k being Integer st a := k c= P holds

P halts_on s

proof end;

registration
end;

theorem :: SCMFSA7B:3

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for a being read-write Int-Location

for k being Integer holds

( (IExec ((a := k),P,s)) . a = k & ( for b being read-write Int-Location st b <> a holds

(IExec ((a := k),P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (IExec ((a := k),P,s)) . f = s . f ) )

for s being State of SCM+FSA

for a being read-write Int-Location

for k being Integer holds

( (IExec ((a := k),P,s)) . a = k & ( for b being read-write Int-Location st b <> a holds

(IExec ((a := k),P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (IExec ((a := k),P,s)) . f = s . f ) )

proof end;

Lm2: for p1, p2, p3, p4 being XFinSequence holds ((p1 ^ p2) ^ p3) ^ p4 = p1 ^ ((p2 ^ p3) ^ p4)

proof end;

Lm3: for c0 being Element of NAT

for s being b

for P being Instruction-Sequence of SCM+FSA

for a being Int-Location

for k being Integer st ( for c being Element of NAT st c < len (aSeq (a,k)) holds

(aSeq (a,k)) . c = P . (c0 + c) ) holds

for i being Element of NAT st i <= len (aSeq (a,k)) holds

IC (Comput (P,s,i)) = c0 + i

proof end;

Lm4: for s being 0 -started State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA

for a being Int-Location

for k being Integer st aSeq (a,k) c= P holds

for i being Element of NAT st i <= len (aSeq (a,k)) holds

IC (Comput (P,s,i)) = i

proof end;

Lm5: for s being 0 -started State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA

for f being FinSeq-Location

for p being FinSequence of INT st f := p c= P holds

P halts_on s

proof end;

registration

let f be FinSeq-Location ;

let p be FinSequence of INT ;

coherence

( f := p is initial & not f := p is empty & f := p is NAT -defined & f := p is the InstructionsF of SCM+FSA -valued ) ;

end;
let p be FinSequence of INT ;

coherence

( f := p is initial & not f := p is empty & f := p is NAT -defined & f := p is the InstructionsF of SCM+FSA -valued ) ;

registration

let f be FinSeq-Location ;

let p be FinSequence of INT ;

correctness

coherence

f := p is parahalting ;

end;
let p be FinSequence of INT ;

correctness

coherence

f := p is parahalting ;

proof end;

theorem :: SCMFSA7B:4

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for f being FinSeq-Location

for p being FinSequence of INT holds

( (IExec ((f := p),P,s)) . f = p & ( for a being read-write Int-Location st a <> intloc 1 & a <> intloc 2 holds

(IExec ((f := p),P,s)) . a = s . a ) & ( for g being FinSeq-Location st g <> f holds

(IExec ((f := p),P,s)) . g = s . g ) )

for s being State of SCM+FSA

for f being FinSeq-Location

for p being FinSequence of INT holds

( (IExec ((f := p),P,s)) . f = p & ( for a being read-write Int-Location st a <> intloc 1 & a <> intloc 2 holds

(IExec ((f := p),P,s)) . a = s . a ) & ( for g being FinSeq-Location st g <> f holds

(IExec ((f := p),P,s)) . g = s . g ) )

proof end;

definition

let i be Instruction of SCM+FSA;

let a be Int-Location;

end;
let a be Int-Location;

pred i refers a means :: SCMFSA7B:def 1

not for b being Int-Location

for l being Element of NAT

for f being FinSeq-Location holds

( b := a <> i & AddTo (b,a) <> i & SubFrom (b,a) <> i & MultBy (b,a) <> i & Divide (b,a) <> i & Divide (a,b) <> i & a =0_goto l <> i & a >0_goto l <> i & b := (f,a) <> i & (f,b) := a <> i & (f,a) := b <> i & f :=<0,...,0> a <> i );

not for b being Int-Location

for l being Element of NAT

for f being FinSeq-Location holds

( b := a <> i & AddTo (b,a) <> i & SubFrom (b,a) <> i & MultBy (b,a) <> i & Divide (b,a) <> i & Divide (a,b) <> i & a =0_goto l <> i & a >0_goto l <> i & b := (f,a) <> i & (f,b) := a <> i & (f,a) := b <> i & f :=<0,...,0> a <> i );

:: deftheorem defines refers SCMFSA7B:def 1 :

for i being Instruction of SCM+FSA

for a being Int-Location holds

( i refers a iff not for b being Int-Location

for l being Element of NAT

for f being FinSeq-Location holds

( b := a <> i & AddTo (b,a) <> i & SubFrom (b,a) <> i & MultBy (b,a) <> i & Divide (b,a) <> i & Divide (a,b) <> i & a =0_goto l <> i & a >0_goto l <> i & b := (f,a) <> i & (f,b) := a <> i & (f,a) := b <> i & f :=<0,...,0> a <> i ) );

for i being Instruction of SCM+FSA

for a being Int-Location holds

( i refers a iff not for b being Int-Location

for l being Element of NAT

for f being FinSeq-Location holds

( b := a <> i & AddTo (b,a) <> i & SubFrom (b,a) <> i & MultBy (b,a) <> i & Divide (b,a) <> i & Divide (a,b) <> i & a =0_goto l <> i & a >0_goto l <> i & b := (f,a) <> i & (f,b) := a <> i & (f,a) := b <> i & f :=<0,...,0> a <> i ) );

definition

let I be preProgram of SCM+FSA;

let a be Int-Location;

end;
let a be Int-Location;

pred I refers a means :: SCMFSA7B:def 2

ex i being Instruction of SCM+FSA st

( i in rng I & i refers a );

ex i being Instruction of SCM+FSA st

( i in rng I & i refers a );

:: deftheorem defines refers SCMFSA7B:def 2 :

for I being preProgram of SCM+FSA

for a being Int-Location holds

( I refers a iff ex i being Instruction of SCM+FSA st

( i in rng I & i refers a ) );

for I being preProgram of SCM+FSA

for a being Int-Location holds

( I refers a iff ex i being Instruction of SCM+FSA st

( i in rng I & i refers a ) );

:: deftheorem Def3 defines destroys SCMFSA7B:def 3 :

for i being Instruction of SCM+FSA

for a being Int-Location holds

( i destroys a iff not for b being Int-Location

for f being FinSeq-Location holds

( a := b <> i & AddTo (a,b) <> i & SubFrom (a,b) <> i & MultBy (a,b) <> i & Divide (a,b) <> i & Divide (b,a) <> i & a := (f,b) <> i & a :=len f <> i ) );

for i being Instruction of SCM+FSA

for a being Int-Location holds

( i destroys a iff not for b being Int-Location

for f being FinSeq-Location holds

( a := b <> i & AddTo (a,b) <> i & SubFrom (a,b) <> i & MultBy (a,b) <> i & Divide (a,b) <> i & Divide (b,a) <> i & a := (f,b) <> i & a :=len f <> i ) );

definition

let I be NAT -defined the InstructionsF of SCM+FSA -valued Function;

let a be Int-Location;

end;
let a be Int-Location;

pred I destroys a means :Def4: :: SCMFSA7B:def 4

ex i being Instruction of SCM+FSA st

( i in rng I & i destroys a );

ex i being Instruction of SCM+FSA st

( i in rng I & i destroys a );

:: deftheorem Def4 defines destroys SCMFSA7B:def 4 :

for I being NAT -defined the InstructionsF of SCM+FSA -valued Function

for a being Int-Location holds

( I destroys a iff ex i being Instruction of SCM+FSA st

( i in rng I & i destroys a ) );

for I being NAT -defined the InstructionsF of SCM+FSA -valued Function

for a being Int-Location holds

( I destroys a iff ex i being Instruction of SCM+FSA st

( i in rng I & i destroys a ) );

:: deftheorem Def5 defines good SCMFSA7B:def 5 :

for I being NAT -defined the InstructionsF of SCM+FSA -valued Function holds

( I is good iff not I destroys intloc 0 );

for I being NAT -defined the InstructionsF of SCM+FSA -valued Function holds

( I is good iff not I destroys intloc 0 );

theorem :: SCMFSA7B:14

for a, b, c being Int-Location

for f being FinSeq-Location st a <> b holds

not b := (f,c) destroys a

for f being FinSeq-Location st a <> b holds

not b := (f,c) destroys a

proof end;

definition

let I be Program of SCM+FSA;

let s be State of SCM+FSA;

let P be Instruction-Sequence of SCM+FSA;

end;
let s be State of SCM+FSA;

let P be Instruction-Sequence of SCM+FSA;

pred I is_closed_on s,P means :Def6: :: SCMFSA7B:def 6

for k being Element of NAT holds IC (Comput ((P +* I),(Initialize s),k)) in dom I;

for k being Element of NAT holds IC (Comput ((P +* I),(Initialize s),k)) in dom I;

:: deftheorem Def6 defines is_closed_on SCMFSA7B:def 6 :

for I being Program of SCM+FSA

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA holds

( I is_closed_on s,P iff for k being Element of NAT holds IC (Comput ((P +* I),(Initialize s),k)) in dom I );

for I being Program of SCM+FSA

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA holds

( I is_closed_on s,P iff for k being Element of NAT holds IC (Comput ((P +* I),(Initialize s),k)) in dom I );

:: deftheorem Def7 defines is_halting_on SCMFSA7B:def 7 :

for I being Program of SCM+FSA

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA holds

( I is_halting_on s,P iff P +* I halts_on Initialize s );

for I being Program of SCM+FSA

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA holds

( I is_halting_on s,P iff P +* I halts_on Initialize s );

theorem Th18: :: SCMFSA7B:18

for I being Program of SCM+FSA holds

( I is paraclosed iff for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA holds I is_closed_on s,P )

( I is paraclosed iff for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA holds I is_closed_on s,P )

proof end;

theorem :: SCMFSA7B:19

for I being Program of SCM+FSA holds

( I is parahalting iff for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA holds I is_halting_on s,P )

( I is parahalting iff for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA holds I is_halting_on s,P )

proof end;

theorem Th20: :: SCMFSA7B:20

for i being Instruction of SCM+FSA

for a being Int-Location

for s being State of SCM+FSA st not i destroys a holds

(Exec (i,s)) . a = s . a

for a being Int-Location

for s being State of SCM+FSA st not i destroys a holds

(Exec (i,s)) . a = s . a

proof end;

theorem Th21: :: SCMFSA7B:21

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA

for I being Program of SCM+FSA

for a being Int-Location st not I destroys a & I is_closed_on s,P holds

for k being Element of NAT holds (Comput ((P +* I),(Initialize s),k)) . a = s . a

for P being Instruction-Sequence of SCM+FSA

for I being Program of SCM+FSA

for a being Int-Location st not I destroys a & I is_closed_on s,P holds

for k being Element of NAT holds (Comput ((P +* I),(Initialize s),k)) . a = s . a

proof end;

registration

ex b_{1} being Program of SCM+FSA st

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

cluster non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial parahalting good for set ;

existence ex b

( b

proof end;

registration

coherence

for b_{1} being Program of SCM+FSA st b_{1} is paraclosed & b_{1} is good holds

b_{1} is keeping_0 ;

end;

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

correctness coherence

for b

b

proof end;

theorem Th22: :: SCMFSA7B:22

for a being Int-Location

for k being Integer holds rng (aSeq (a,k)) c= {(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))}

for k being Integer holds rng (aSeq (a,k)) c= {(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))}

proof end;

theorem Th23: :: SCMFSA7B:23

for a being Int-Location

for k being Integer holds rng (a := k) c= {(halt SCM+FSA),(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))}

for k being Integer holds rng (a := k) c= {(halt SCM+FSA),(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))}

proof end;

registration

let a be read-write Int-Location;

let k be Integer;

correctness

coherence

a := k is good ;

end;
let k be Integer;

correctness

coherence

a := k is good ;

proof end;

registration
end;