:: 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 b1 -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 b1 being Program of st
( b1 is parahalting & b1 is good & b1 is halt-ending & b1 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 b1 being Program of st b1 is really-closed & b1 is good holds
b1 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;