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

set A = NAT ;

theorem Th1: :: SCMFSA7B:1

for p being FinSequence of the Instructions of SCM+FSA holds dom (Load p) = { m where m is Element of NAT : m < len p }

proof end;

theorem Th2: :: SCMFSA7B:2

for p being FinSequence of the Instructions of SCM+FSA holds rng (Load p) = rng p

proof end;

registration

let p be FinSequence of the Instructions of SCM+FSA ;
cluster Load p -> programmed initial ;
coherence
( Load p is initial & Load p is programmed )

proof end;

end;

theorem :: SCMFSA7B:3

for i being Instruction of SCM+FSA holds Load <*i*> = (insloc 0 ) .--> i

proof end;

theorem Th4: :: SCMFSA7B:4

for i being Instruction of SCM+FSA holds dom (Macro i) = {(insloc 0 ),(insloc 1)}

proof end;

theorem Th5: :: SCMFSA7B:5

for i being Instruction of SCM+FSA holds Macro i = Load <*i,(halt SCM+FSA )*>

proof end;

theorem Th6: :: SCMFSA7B:6

for i being Instruction of SCM+FSA holds card (Macro i) = 2

proof end;

theorem :: SCMFSA7B:7

for i being Instruction of SCM+FSA holds
( ( i = halt SCM+FSA implies (Directed (Macro i)) . (insloc 0 ) = goto (insloc 2) ) & ( i <> halt SCM+FSA implies (Directed (Macro i)) . (insloc 0 ) = i ) )

proof end;

theorem :: SCMFSA7B:8

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

proof end;

registration

let a be Int-Location ;
let k be Integer;
cluster a := k -> programmed initial ;
coherence
( a := k is initial & a := k is programmed )

proof end;

end;

Lm1: for s being State of SCM+FSA st IC s = insloc 0 holds
for a being Int-Location
for k being Integer st a := k c= s holds
s is halting

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 s being State of SCM+FSA
for a being read-write Int-Location
for k being Integer holds
( (IExec (a := k),s) . a = k & ( for b being read-write Int-Location st b <> a holds
(IExec (a := k),s) . b = s . b ) & ( for f being FinSeq-Location holds (IExec (a := k),s) . f = s . f ) )

proof end;

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

proof end;

Lm3: for p1, p2, p3 being FinSequence holds
( ((len p1) + (len p2)) + (len p3) = len ((p1 ^ p2) ^ p3) & ((len p1) + (len p2)) + (len p3) = len (p1 ^ (p2 ^ p3)) & (len p1) + ((len p2) + (len p3)) = len (p1 ^ (p2 ^ p3)) & (len p1) + ((len p2) + (len p3)) = len ((p1 ^ p2) ^ p3) )

proof end;

Lm4: for s being State of SCM+FSA st IC s = insloc 0 & s . (intloc 0 ) = 1 holds
for f being FinSeq-Location
for p being FinSequence of INT st f := p c= s holds
( s is halting & (Result s) . f = p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds
(Result s) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds
(Result s) . g = s . g ) )

proof end;

Lm5: for s being State of SCM+FSA
for c0 being Element of NAT st IC s = insloc c0 holds
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 + 1) = s . (insloc (c0 + c)) ) holds
for i being Element of NAT st i <= len (aSeq a,k) holds
IC (Computation s,i) = insloc (c0 + i)

proof end;

Lm6: for s being State of SCM+FSA st IC s = insloc 0 holds
for a being Int-Location
for k being Integer st Load (aSeq a,k) c= s holds
for i being Element of NAT st i <= len (aSeq a,k) holds
IC (Computation s,i) = insloc i

proof end;

Lm7: for s being State of SCM+FSA st IC s = insloc 0 holds
for f being FinSeq-Location
for p being FinSequence of INT st f := p c= s holds
s is halting

proof end;

registration

let f be FinSeq-Location ;
let p be FinSequence of INT ;
cluster f := p -> programmed initial ;
coherence
( f := p is initial & f := p is programmed )

proof end;

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 s being State of SCM+FSA
for f being FinSeq-Location
for p being FinSequence of INT holds
( (IExec (f := p),s) . f = p & ( for a being read-write Int-Location st a <> intloc 1 & a <> intloc 2 holds
(IExec (f := p),s) . a = s . a ) & ( for g being FinSeq-Location st g <> f holds
(IExec (f := p),s) . g = s . g ) )

proof end;

definition

let i be Instruction of SCM+FSA ;
let a be Int-Location ;
pred i does_not_refer a means :: SCMFSA7B:def 1
for b being Int-Location
for l being Instruction-Location of SCM+FSA
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 does_not_refer SCMFSA7B:def 1 :

for i being Instruction of SCM+FSA
for a being Int-Location holds
( i does_not_refer a iff for b being Int-Location
for l being Instruction-Location of SCM+FSA
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 does_not_refer a means :: SCMFSA7B:def 2
for i being Instruction of SCM+FSA st i in rng I holds
i does_not_refer a;

end;

:: deftheorem defines does_not_refer SCMFSA7B:def 2 :

for I being preProgram of SCM+FSA
for a being Int-Location holds
( I does_not_refer a iff for i being Instruction of SCM+FSA st i in rng I holds
i does_not_refer a );

definition

let i be Instruction of SCM+FSA ;
let a be Int-Location ;
pred i does_not_destroy a means :Def3: :: SCMFSA7B:def 3
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 Def3 defines does_not_destroy SCMFSA7B:def 3 :

for i being Instruction of SCM+FSA
for a being Int-Location holds
( i does_not_destroy a iff 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 FinPartState of SCM+FSA ;
let a be Int-Location ;
pred I does_not_destroy a means :Def4: :: SCMFSA7B:def 4
for i being Instruction of SCM+FSA st i in rng I holds
i does_not_destroy a;

end;

:: deftheorem Def4 defines does_not_destroy SCMFSA7B:def 4 :

for I being FinPartState of SCM+FSA
for a being Int-Location holds
( I does_not_destroy a iff for i being Instruction of SCM+FSA st i in rng I holds
i does_not_destroy a );

definition

let I be FinPartState of SCM+FSA ;
attr I is good means :Def5: :: SCMFSA7B:def 5
I does_not_destroy intloc 0 ;

end;

:: deftheorem Def5 defines good SCMFSA7B:def 5 :

for I being FinPartState of SCM+FSA holds
( I is good iff I does_not_destroy intloc 0 );

registration

cluster halt-free good Element of K392(the Object-Kind of SCM+FSA );
existence
ex b₁ being Program of SCM+FSA st
( b₁ is halt-free & b₁ is good )

proof end;

end;

theorem Th11: :: SCMFSA7B:11

for a being Int-Location holds halt SCM+FSA does_not_destroy a

proof end;

theorem Th12: :: SCMFSA7B:12

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

proof end;

theorem Th13: :: SCMFSA7B:13

for a, b, c being Int-Location st a <> b holds
AddTo b,c does_not_destroy a

proof end;

theorem Th14: :: SCMFSA7B:14

for a, b, c being Int-Location st a <> b holds
SubFrom b,c does_not_destroy a

proof end;

theorem :: SCMFSA7B:15

for a, b, c being Int-Location st a <> b holds
MultBy b,c does_not_destroy a

proof end;

theorem :: SCMFSA7B:16

for a, b, c being Int-Location st a <> b & a <> c holds
Divide b,c does_not_destroy a

proof end;

theorem :: SCMFSA7B:17

for a being Int-Location
for l being Instruction-Location of SCM+FSA holds goto l does_not_destroy a

proof end;

theorem :: SCMFSA7B:18

for a, b being Int-Location
for l being Instruction-Location of SCM+FSA holds b =0_goto l does_not_destroy a

proof end;

theorem :: SCMFSA7B:19

for a, b being Int-Location
for l being Instruction-Location of SCM+FSA holds b >0_goto l does_not_destroy a

proof end;

theorem :: SCMFSA7B:20

for a, b, c being Int-Location
for f being FinSeq-Location st a <> b holds
b := f,c does_not_destroy a

proof end;

theorem :: SCMFSA7B:21

for a, b, c being Int-Location
for f being FinSeq-Location holds f,c := b does_not_destroy a

proof end;

theorem :: SCMFSA7B:22

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

proof end;

theorem :: SCMFSA7B:23

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

proof end;

definition

canceled;
let I be FinPartState of SCM+FSA ;
let s be State of SCM+FSA ;
pred I is_closed_on s means :Def7: :: SCMFSA7B:def 7
for k being Element of NAT holds IC (Computation (s +* (I +* (Start-At (insloc 0 )))),k) in dom I;
pred I is_halting_on s means :Def8: :: SCMFSA7B:def 8
s +* (I +* (Start-At (insloc 0 ))) is halting;

end;

:: deftheorem SCMFSA7B:def 6 :

canceled;

:: deftheorem Def7 defines is_closed_on SCMFSA7B:def 7 :

for I being FinPartState of SCM+FSA
for s being State of SCM+FSA holds
( I is_closed_on s iff for k being Element of NAT holds IC (Computation (s +* (I +* (Start-At (insloc 0 )))),k) in dom I );

:: deftheorem Def8 defines is_halting_on SCMFSA7B:def 8 :

for I being FinPartState of SCM+FSA
for s being State of SCM+FSA holds
( I is_halting_on s iff s +* (I +* (Start-At (insloc 0 ))) is halting );

theorem Th24: :: SCMFSA7B:24

for I being Program of SCM+FSA holds
( I is paraclosed iff for s being State of SCM+FSA holds I is_closed_on s )

proof end;

theorem :: SCMFSA7B:25

for I being Program of SCM+FSA holds
( I is parahalting iff for s being State of SCM+FSA holds I is_halting_on s )

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 i does_not_destroy a holds
(Exec i,s) . a = s . a

proof end;

theorem Th27: :: SCMFSA7B:27

for s being State of SCM+FSA
for I being Program of SCM+FSA
for a being Int-Location st I does_not_destroy a & I is_closed_on s holds
for k being Element of NAT holds (Computation (s +* (I +* (Start-At (insloc 0 )))),k) . a = s . a

proof end;

theorem Th28: :: SCMFSA7B:28

Stop SCM+FSA does_not_destroy intloc 0

proof end;

Lm8: Stop SCM+FSA is parahalting

proof end;

registration

cluster parahalting good Element of K392(the Object-Kind of SCM+FSA );
existence
ex b₁ being Program of SCM+FSA st
( b₁ is parahalting & b₁ is good )

proof end;

end;

registration

cluster Stop SCM+FSA -> parahalting good ;
coherence
( Stop SCM+FSA is parahalting & Stop SCM+FSA is good ) by Def5, Lm8, Th28;

end;

registration

cluster paraclosed good -> keeping_0 Element of K392(the Object-Kind of SCM+FSA );
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 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;