:: Constant assignment macro instructions of SCM+FSA, Part II
:: by Noriko Asamoto
::
:: Received August 27, 1996
:: Copyright (c) 1996-2021 Association of Mizar Users

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

proof end;

theorem :: SCMFSA7B:2

for i being Instruction of SCM+FSA holds (Directed (Macro i)) . 1 = goto 2

proof end;

registration

let a be Int-Location;
let k be Integer;

cluster a := k -> non empty initial ;

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;

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

let a be Int-Location;
let k be Integer;

cluster a := k -> parahalting ;

correctness
coherence
a := k is parahalting ;

proof end;

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

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₁ -started State of SCM+FSA
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 ;

cluster f := p -> non empty initial ;

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;

registration

let f be FinSeq-Location ;
let p be FinSequence of INT ;

cluster f := p -> parahalting ;

correctness
coherence
f := p is parahalting ;
by Lm5;

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

proof end;

definition

let i be Instruction of SCM+FSA;
let a be Int-Location;

pred i refers a means :: SCMFSA7B:def 1
not for b being Int-Location
for l being 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 );

end;

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

pred I refers a means :: SCMFSA7B:def 2
ex i being Instruction of SCM+FSA st
( i in rng I & i refers a );

end;

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

definition

let i be Instruction of SCM+FSA;
let a be Int-Location;

pred i destroys a means :: SCMFSA7B:def 3
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 );

end;

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

definition

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

pred I destroys a means :: SCMFSA7B:def 4
ex i being Instruction of SCM+FSA st
( i in rng I & i destroys a );

end;

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

definition

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

attr I is good means :: SCMFSA7B:def 5
not I destroys intloc 0;

end;

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

theorem :: SCMFSA7B:5

for a being Int-Location holds not halt SCM+FSA destroys a ;

theorem Th6: :: SCMFSA7B:6

for a, b, c being Int-Location st a <> b holds
not b := c destroys a

proof end;

theorem Th7: :: SCMFSA7B:7

for a, b, c being Int-Location st a <> b holds
not AddTo (b,c) destroys a

proof end;

theorem Th8: :: SCMFSA7B:8

for a, b, c being Int-Location st a <> b holds
not SubFrom (b,c) destroys a

proof end;

theorem :: SCMFSA7B:9

for a, b, c being Int-Location st a <> b holds
not MultBy (b,c) destroys a

proof end;

theorem :: SCMFSA7B:10

for a, b, c being Int-Location st a <> b & a <> c holds
not Divide (b,c) destroys a

proof end;

theorem :: SCMFSA7B:11

for a being Int-Location
for l being Nat holds not goto l destroys a ;

theorem :: SCMFSA7B:12

for a, b being Int-Location
for l being Nat holds not b =0_goto l destroys a ;

theorem :: SCMFSA7B:13

for a, b being Int-Location
for l being Nat holds not b >0_goto l destroys a ;

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

proof end;

theorem :: SCMFSA7B:15

for a, b, c being Int-Location
for f being FinSeq-Location holds not (f,c) := b destroys a

proof end;

theorem :: SCMFSA7B:16

for a, b being Int-Location
for f being FinSeq-Location st a <> b holds
not b :=len f destroys a

proof end;

theorem :: SCMFSA7B:17

for a, b being Int-Location
for f being FinSeq-Location holds not f :=<0,...,0> b destroys a

proof end;

canceled;

::$CD

definition

let I be Program of ;
let s be State of SCM+FSA;
let P be Instruction-Sequence of SCM+FSA;

pred I is_halting_on s,P means :: SCMFSA7B:def 6
P +* I halts_on Initialize s;

end;

:: deftheorem defines is_halting_on SCMFSA7B:def 6 :
for I being Program of
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 :: SCMFSA7B:18

canceled;

::$CT

theorem :: SCMFSA7B:19

for I being Program of 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 )

proof end;

theorem Th19: :: 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

proof end;

theorem Th20: :: SCMFSA7B:21

for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being really-closed Program of
for a being Int-Location st not I destroys a holds
for k being Nat holds (Comput ((P +* I),(Initialize s),k)) . a = s . a

proof end;

registration

cluster Stop SCM+FSA -> parahalting good ;

coherence
( Stop SCM+FSA is parahalting & Stop SCM+FSA is good )

proof end;

end;

registration

cluster Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty V16() Function-like V31() initial halt-ending unique-halt parahalting good for set ;

existence
ex b₁ being Program of st
( b₁ is parahalting & b₁ is good & b₁ is halt-ending & b₁ is unique-halt )

proof end;

end;

registration

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

correctness
coherence
for b₁ being Program of st b₁ is really-closed & b₁ is good holds
b₁ is keeping_0 ;

proof end;

end;

theorem Th21: :: 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)))}

proof end;

theorem Th22: :: 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)))}

proof end;

registration

let a be read-write Int-Location;
let k be Integer;

cluster a := k -> good ;

correctness
coherence
a := k is good ;

proof end;

end;

registration

let a be read-write Int-Location;
let k be Integer;

cluster a := k -> really-closed ;

correctness
coherence
a := k is really-closed ;

proof end;

end;

registration

let a be read-write Int-Location;
let k be Integer;

cluster a := k -> keeping_0 ;

correctness
coherence
a := k is keeping_0 ;
;

end;