:: Constant assignment macro instructions of SCM+FSA, Part II
:: by Noriko Asamoto
::
:: Received August 27, 1996
:: Copyright (c) 1996-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, FINSEQ_1, AMI_1, SCMFSA_2, RELAT_1, SCMFSA_7,
ARYTM_3, ARYTM_1, TARSKI, FUNCT_1, XXREAL_0, PARTFUN1, CAT_1, NAT_1,
CARD_1, FUNCOP_1, SCMFSA6A, ORDINAL4, AMI_3, FUNCT_4, INT_1, GRAPHSP,
FSM_1, CIRCUIT2, EXTPRO_1, SCMFSA6B, SF_MASTR, MSUALG_1, XBOOLE_0,
PRE_POLY, AMISTD_2, SCMFSA7B, AFINSQ_1, SCMFSA6C, COMPOS_1, AMISTD_1,
TURING_1, RELOC, VALUED_1, SCMPDS_4;
notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0,
COMPLEX1, NAT_1, INT_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1,
FINSEQ_2, FUNCT_4, DOMAIN_1, VALUED_1, AFINSQ_1, STRUCT_0, MEMSTR_0,
COMPOS_0, COMPOS_1, EXTPRO_1, FUNCT_7, SCMFSA_2, AMISTD_1, AMISTD_2,
FUNCOP_1, XXREAL_0, ENUMSET1, NAT_D, PBOOLE, AFINSQ_2, AMISTD_4,
SCMFSA_7, COMPOS_2, SCMFSA6A, SF_MASTR, SCMFSA6B, INT_2, PRE_POLY,
SCMFSA_M;
constructors ENUMSET1, XXREAL_0, REAL_1, SCMFSA_7, SCMFSA6A, SF_MASTR,
SCMFSA6B, NAT_D, RELSET_1, PRE_POLY, DOMAIN_1, AFINSQ_2, PARTFUN3,
PBOOLE, AMISTD_1, AMISTD_2, AMI_3, MEMSTR_0, SCMFSA_M, FUNCT_7, COMPOS_2;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FUNCOP_1, XXREAL_0, XREAL_0, NAT_1,
INT_1, SCMFSA_2, SCMFSA6B, ORDINAL1, CARD_1, AFINSQ_1, COMPOS_1,
AFINSQ_2, EXTPRO_1, FUNCT_4, STRUCT_0, MEMSTR_0, SCMFSA10, COMPOS_0,
SCMFSA_M, COMPOS_2, SCMFSA6C, SCMFSA_4;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin
reserve m for Nat;
reserve P for Instruction-Sequence of SCM+FSA;
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);
theorem :: SCMFSA7B:2
for i being Instruction of SCM+FSA holds (Directed Macro i). 1 = goto 2;
registration
let a be Int-Location, k be Integer;
cluster a := k -> initial non empty
NAT-defined (the InstructionsF of SCM+FSA)-valued;
end;
registration
let a be Int-Location, k be Integer;
cluster a := k -> parahalting;
end;
theorem :: SCMFSA7B:3
for s being State of SCM+FSA for a being read-write Int-Location, 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;
registration
let f be FinSeq-Location, p be FinSequence of INT;
cluster f := p -> initial non empty
NAT-defined (the InstructionsF of SCM+FSA)-valued;
end;
registration
let f be FinSeq-Location, p be FinSequence of INT;
cluster f := p -> parahalting;
end;
theorem :: SCMFSA7B:4
for s being State of SCM+FSA, f being FinSeq-Location, 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;
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, 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;
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;
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;
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;
definition
let I be NAT-defined (the InstructionsF of SCM+FSA)-valued Function;
attr I is good means
:: SCMFSA7B:def 5
I does not destroy intloc 0;
end;
theorem :: SCMFSA7B:5
for a being Int-Location holds halt SCM+FSA does not destroy a;
theorem :: SCMFSA7B:6
for a,b,c being Int-Location holds a <> b implies
b := c does not destroy a;
theorem :: SCMFSA7B:7
for a,b,c being Int-Location holds a <> b implies
AddTo(b,c) does not destroy a;
theorem :: SCMFSA7B:8
for a,b,c being Int-Location holds a <> b implies
SubFrom(b,c) does not destroy a;
theorem :: SCMFSA7B:9
for a,b,c being Int-Location holds a <> b implies
MultBy(b,c) does not destroy a;
theorem :: SCMFSA7B:10
for a,b,c being Int-Location holds a <> b & a <> c implies
Divide(b,c) does not destroy a;
theorem :: SCMFSA7B:11
for a being Int-Location, l being Nat
holds goto l does not destroy a;
theorem :: SCMFSA7B:12
for a,b being Int-Location, l being Nat
holds b =0_goto l does not destroy a;
theorem :: SCMFSA7B:13
for a,b being Int-Location, l being Nat
holds b >0_goto l does not destroy a;
theorem :: SCMFSA7B:14
for a,b,c being Int-Location, f being FinSeq-Location holds a <> b
implies b := (f,c) does not destroy a;
theorem :: SCMFSA7B:15
for a,b,c being Int-Location, f being FinSeq-Location holds
(f,c):= b does not destroy a;
theorem :: SCMFSA7B:16
for a,b being Int-Location, f being FinSeq-Location holds a <> b
implies b :=len f does not destroy a;
theorem :: SCMFSA7B:17
for a,b being Int-Location, f being FinSeq-Location holds
f:=<0,...,0> b does not destroy a;
::$CD
definition
let I be Program of SCM+FSA;
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 7
P +* I halts_on Initialize s;
end;
::$CT
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;
theorem :: SCMFSA7B:20
for i being Instruction of SCM+FSA, a being Int-Location, s
being State of SCM+FSA st i does not destroy a holds Exec(i,s).a = s.a;
theorem :: SCMFSA7B:21
for s being State of SCM+FSA,
P being Instruction-Sequence of SCM+FSA,
I being really-closed Program of SCM+FSA, a being Int-Location
st I does not destroy a :::& I is_closed_on s,P
for k being Nat holds Comput(P +* I,Initialize s,k).a = s.a;
registration
cluster Stop SCM+FSA -> parahalting good;
end;
registration
cluster parahalting good halt-ending unique-halt for Program of SCM+FSA;
end;
registration
cluster really-closed good -> keeping_0 for Program of SCM+FSA;
end;
theorem :: SCMFSA7B:22
for a being Int-Location, k being Integer holds rng aSeq(a,k) c=
{a := intloc 0,AddTo(a,intloc 0),SubFrom(a,intloc 0)};
theorem :: SCMFSA7B:23
for a being Int-Location, k being Integer holds rng (a := k) c=
{halt SCM+FSA,a := intloc 0,AddTo(a,intloc 0),SubFrom(a,intloc 0)};
registration
let a be read-write Int-Location, k be Integer;
cluster a := k -> good;
end;
reserve n for Nat;
registration
let a be read-write Int-Location, k be Integer;
cluster a := k -> really-closed;
end;
registration
let a be read-write Int-Location, k be Integer;
cluster a := k -> keeping_0;
end;