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

begin

set A = NAT ;

theorem :: SCMFSA7B:1

canceled;

theorem :: SCMFSA7B:2

canceled;

theorem :: SCMFSA7B:3

canceled;

theorem :: SCMFSA7B:4

canceled;

theorem :: SCMFSA7B:5

canceled;

theorem :: SCMFSA7B:6

canceled;

theorem :: SCMFSA7B:7

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

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 NAT -defined the Instructions of SCM+FSA -valued initial ;
coherence
( a := k is initial & not a := k is empty & a := k is NAT -defined & a := k is the Instructions of SCM+FSA -valued )

proof end;

end;

Lm1: for s being State of SCM+FSA st IC s = 0 holds
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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:9

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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 the Instructions of SCM+FSA -valued ManySortedSet of NAT
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 the Instructions of SCM+FSA -valued ManySortedSet of NAT
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 the Instructions of SCM+FSA -valued ManySortedSet of NAT
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 NAT -defined the Instructions of SCM+FSA -valued initial ;
coherence
( f := p is initial & not f := p is empty & f := p is NAT -defined & f := p is the Instructions 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 ;

proof end;

end;

theorem :: SCMFSA7B:10

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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 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 );

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 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 ;
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 :Def3: :: 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 & a :==1 <> i );

end;

:: 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 & a :==1 <> i ) );

definition

let I be NAT -defined the Instructions of SCM+FSA -valued Function;
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 );

end;

:: deftheorem Def4 defines destroys SCMFSA7B:def 4 :
for I being NAT -defined the Instructions 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 Instructions of SCM+FSA -valued Function;
attr I is good means :Def5: :: SCMFSA7B:def 5
not I destroys intloc 0;

end;

:: deftheorem Def5 defines good SCMFSA7B:def 5 :
for I being NAT -defined the Instructions of SCM+FSA -valued Function holds
( I is good iff not I destroys intloc 0 );

theorem Th11: :: SCMFSA7B:11

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

proof end;

theorem Th12: :: SCMFSA7B:12

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

proof end;

theorem Th13: :: SCMFSA7B:13

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

proof end;

theorem Th14: :: SCMFSA7B:14

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

proof end;

theorem :: SCMFSA7B:15

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

proof end;

theorem :: SCMFSA7B:16

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

proof end;

theorem :: SCMFSA7B:17

for a being Int-Location
for l being Element of NAT holds not goto l destroys a

proof end;

theorem :: SCMFSA7B:18

for a, b being Int-Location
for l being Element of NAT holds not b =0_goto l destroys a

proof end;

theorem :: SCMFSA7B:19

for a, b being Int-Location
for l being Element of NAT holds not b >0_goto l destroys a

proof end;

theorem :: SCMFSA7B:20

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

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

proof end;

theorem :: SCMFSA7B:22

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

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

proof end;

definition

canceled;
let I be Program of SCM+FSA;
let s be State of SCM+FSA;
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ;
pred I is_closed_on s,P means :Def7: :: SCMFSA7B:def 7
for k being Element of NAT holds IC (Comput ((P +* I),(Initialize s),k)) in dom I;
pred I is_halting_on s,P means :Def8: :: SCMFSA7B:def 8
P +* I halts_on Initialize s;

end;

:: deftheorem SCMFSA7B:def 6 :
canceled;

:: deftheorem Def7 defines is_closed_on SCMFSA7B:def 7 :
for I being Program of SCM+FSA
for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT 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 Def8 defines is_halting_on SCMFSA7B:def 8 :
for I being Program of SCM+FSA
for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds
( I is_halting_on s,P iff P +* I halts_on Initialize s );

theorem Th24: :: SCMFSA7B:24

for I being Program of SCM+FSA holds
( I is paraclosed iff for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds I is_closed_on s,P )

proof end;

theorem :: SCMFSA7B:25

for I being Program of SCM+FSA holds
( I is parahalting iff for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds I is_halting_on s,P )

proof end;

theorem Th26: :: SCMFSA7B:26

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 Th27: :: SCMFSA7B:27

for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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

cluster Stop SCM+FSA -> parahalting good ;
coherence
( Stop SCM+FSA is parahalting & Stop SCM+FSA is good )

proof end;

end;

registration

cluster non empty V11() Relation-like NAT -defined the carrier of SCM+FSA -defined the Instructions of SCM+FSA -valued Function-like the Object-Kind of SCM+FSA -compatible V26() initial parahalting good set ;
existence
ex b₁ being Program of SCM+FSA st
( b₁ is parahalting & b₁ is good )

proof end;

end;

registration

cluster non empty Relation-like NAT -defined the carrier of SCM+FSA -defined the Instructions of SCM+FSA -valued Function-like the Object-Kind of SCM+FSA -compatible V26() initial paraclosed good -> keeping_0 set ;
correctness
coherence
for b₁ being Program of SCM+FSA st b₁ is paraclosed & b₁ is good holds
b₁ is keeping_0 ;

proof end;

end;

theorem :: SCMFSA7B:28

canceled;

theorem Th29: :: SCMFSA7B:29

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 Th30: :: SCMFSA7B:30

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 -> keeping_0 ;
correctness
coherence
a := k is keeping_0 ;
;

end;

theorem :: SCMFSA7B:31

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

proof end;