Journal of Formalized Mathematics
Volume 5, 1993
University of Bialystok
Copyright (c) 1993
Association of Mizar Users
The abstract of the Mizar article:
-
- by
- Grzegorz Bancerek,
and
- Piotr Rudnicki
- Received December 30, 1993
- MML identifier: SCM_COMP
- [
Mizar article,
MML identifier index
]
environ
vocabulary AMI_3, FINSEQ_1, AMI_1, INT_1, SCM_1, FUNCT_1, RELAT_1, ARYTM_1,
BINTREE1, DTCONSTR, LANG1, AMI_2, TDGROUP, BOOLE, TREES_4, QC_LANG1,
CAT_1, NAT_1, TREES_2, MCART_1, FUNCT_2, SQUARE_1, SCM_COMP;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0,
NAT_1, INT_1, MCART_1, FUNCT_1, FUNCT_2, TREES_2, TREES_4, STRUCT_0,
AMI_1, AMI_2, AMI_3, FRAENKEL, SCM_1, FINSEQ_1, FINSEQ_2, LANG1,
BINTREE1, DTCONSTR, LIMFUNC1;
constructors NAT_1, AMI_2, SCM_1, BINTREE1, DTCONSTR, FINSOP_1, LIMFUNC1,
MEMBERED, XBOOLE_0;
clusters SUBSET_1, INT_1, TREES_3, DTCONSTR, BINTREE1, AMI_1, AMI_3, RELSET_1,
STRUCT_0, AMI_2, XBOOLE_0, NAT_1, FRAENKEL, MEMBERED, ZFMISC_1, ORDINAL2;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
begin
:: Auxiliary theorems about SCM
theorem :: SCM_COMP:1
for I1, I2 being FinSequence of the Instructions of SCM,
D being FinSequence of INT,
il, ps, ds being Nat,
s being State-consisting of il, ps, ds, I1^I2, D
holds s is State-consisting of il, ps, ds, I1, D &
s is State-consisting of il, (ps+len I1), ds, I2, D;
theorem :: SCM_COMP:2
for I1, I2 being FinSequence of the Instructions of SCM,
il, ps, ds, k, il1 being Nat,
s being State-consisting of il, ps, ds, I1^I2, <*>INT,
u being State of SCM st u = (Computation s).k & il.il1 = IC u
holds u is State-consisting of il1, (ps + len I1), ds, I2, <*>INT;
definition
func SCM-AE -> binary with_terminals with_nonterminals
with_useful_nonterminals strict (non empty DTConstrStr) means
:: SCM_COMP:def 1
Terminals it = SCM-Data-Loc &
NonTerminals it = [:1, 5:] &
for x, y, z being Symbol of it holds x ==> <*y, z*> iff x in [:1, 5:];
end;
definition
mode bin-term is Element of TS SCM-AE;
end;
definition
let nt be NonTerminal of SCM-AE;
let tl, tr be bin-term;
redefine func nt-tree (tl, tr) -> bin-term;
end;
definition
let t be Terminal of SCM-AE;
redefine func root-tree t -> bin-term;
end;
definition
let t be Terminal of SCM-AE;
func @t -> Data-Location equals
:: SCM_COMP:def 2
t;
end;
theorem :: SCM_COMP:3
for nt being NonTerminal of SCM-AE holds
nt = [0,0] or nt = [0,1] or nt = [0,2] or nt = [0,3] or nt = [0,4];
theorem :: SCM_COMP:4
[0,0] is NonTerminal of SCM-AE & [0,1] is NonTerminal of SCM-AE &
[0,2] is NonTerminal of SCM-AE & [0,3] is NonTerminal of SCM-AE &
[0,4] is NonTerminal of SCM-AE;
definition
let t1, t2 be bin-term;
func t1+t2 -> bin-term equals
:: SCM_COMP:def 3
[0,0]-tree(t1, t2);
func t1-t2 -> bin-term equals
:: SCM_COMP:def 4
[0,1]-tree(t1, t2);
func t1*t2 -> bin-term equals
:: SCM_COMP:def 5
[0,2]-tree(t1, t2);
func t1 div t2 -> bin-term equals
:: SCM_COMP:def 6
[0,3]-tree(t1, t2);
func t1 mod t2 -> bin-term equals
:: SCM_COMP:def 7
[0,4]-tree(t1, t2);
end;
theorem :: SCM_COMP:5 :: PRE_COMP_5:
for term being bin-term holds
(ex t being Terminal of SCM-AE st term = root-tree t) or
ex tl, tr being bin-term st term = tl+tr or term = tl-tr or
term = tl*tr or term = tl div tr or term = tl mod tr;
definition
let o be NonTerminal of SCM-AE, i, j be Integer;
func o-Meaning_on (i, j) -> Integer equals
:: SCM_COMP:def 8
i+j if o = [0,0],
i-j if o = [0,1],
i*j if o = [0,2],
i div j if o = [0,3],
i mod j if o = [0,4];
end;
definition
let s be State of SCM;
let t be Terminal of SCM-AE;
redefine func s.t -> Integer;
end;
definition let D be non empty set;
let f be Function of INT, D;
let x be Integer;
redefine func f.x -> Element of D;
end;
definition
let s be State of SCM;
let term be bin-term;
func term @ s -> Integer means
:: SCM_COMP:def 9
ex f being Function of TS SCM-AE, INT st
it = f.term &
(for t being Terminal of SCM-AE holds f.(root-tree t) = s.t) &
(for nt being NonTerminal of SCM-AE,
tl, tr being bin-term,
rtl, rtr being Symbol of SCM-AE
st rtl = root-label tl & rtr = root-label tr & nt ==> <* rtl, rtr *>
for xl, xr being Element of INT st xl = f.tl & xr = f.tr
holds f.(nt-tree (tl, tr)) = nt-Meaning_on (xl, xr));
end;
theorem :: SCM_COMP:6
for s being State of SCM, t being Terminal of SCM-AE holds
(root-tree t)@s = s.t;
theorem :: SCM_COMP:7
for s being State of SCM, nt being NonTerminal of SCM-AE,
tl, tr being bin-term holds
(nt-tree(tl, tr))@s = nt-Meaning_on(tl@s, tr@s);
theorem :: SCM_COMP:8 :: PRE_COMP_8:
for s being State of SCM, tl, tr being bin-term holds
(tl+tr)@s = (tl@s)+(tr@s) & (tl-tr)@s = (tl@s)-(tr@s) &
(tl*tr)@s = (tl@s)*(tr@s) &
(tl div tr)@s = (tl@s) div (tr@s) & (tl mod tr)@s = (tl@s) mod (tr@s);
definition
let nt be NonTerminal of SCM-AE, n be Nat;
func Selfwork(nt, n) -> Element of ((the Instructions of SCM) qua set)*
equals
:: SCM_COMP:def 10
<*AddTo(dl.n, dl.(n+1))*> if nt = [0,0],
<*SubFrom(dl.n, dl.(n+1))*> if nt = [0,1],
<*MultBy(dl.n, dl.(n+1))*> if nt = [0,2],
<*Divide(dl.n, dl.(n+1))*> if nt = [0,3],
<*Divide(dl.n, dl.(n+1)), dl.n:=dl.(n+1)*> if nt = [0,4];
end;
definition
let term be bin-term, aux be Nat;
func SCM-Compile(term, aux) -> FinSequence of the Instructions of SCM means
:: SCM_COMP:def 11
ex f being Function of TS SCM-AE,
Funcs(NAT, ((the Instructions of SCM) qua set)*)
st it = (f.term qua
Element of Funcs(NAT, ((the Instructions of SCM) qua set)*)).aux &
(for t being Terminal of SCM-AE
ex g being Function of NAT, ((the Instructions of SCM) qua set)*
st g = f.(root-tree t) &
for n being Nat holds g.n = <*dl.n:=@t*>) &
for nt being NonTerminal of SCM-AE, t1, t2 being bin-term,
rtl, rtr being Symbol of SCM-AE
st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl, rtr*>
ex g, f1, f2 being Function of NAT, ((the Instructions of SCM) qua set)
*
st g = f.(nt-tree (t1, t2)) & f1 = f.t1 & f2 = f.t2 &
for n being Nat holds g.n = (f1.n)^(f2.(n+1))^Selfwork(nt, n);
end;
theorem :: SCM_COMP:9
for t being Terminal of SCM-AE, n being Nat holds
SCM-Compile(root-tree t, n) = <* dl.n:=@t *>;
theorem :: SCM_COMP:10
for nt being NonTerminal of SCM-AE, t1, t2 being bin-term, n being Nat,
rtl, rtr being Symbol of SCM-AE
st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl, rtr*>
holds SCM-Compile(nt-tree(t1,t2), n) =
SCM-Compile(t1, n)^SCM-Compile(t2, n+1)^Selfwork(nt, n);
definition
let t be Terminal of SCM-AE;
func d".t -> Nat means
:: SCM_COMP:def 12
dl.it = t;
end;
definition
let term be bin-term;
func max_Data-Loc_in term -> Nat means
:: SCM_COMP:def 13
ex f being Function of TS SCM-AE, NAT st
it = f.term &
(for t being Terminal of SCM-AE holds f.(root-tree t) = d".t) &
(for nt being NonTerminal of SCM-AE, tl, tr being bin-term,
rtl, rtr being Symbol of SCM-AE
st rtl = root-label tl & rtr = root-label tr & nt ==> <* rtl, rtr *>
for xl, xr being Nat st xl = f.tl & xr = f.tr
holds f.(nt-tree (tl, tr)) = max(xl, xr));
end;
theorem :: SCM_COMP:11
for t being Terminal of SCM-AE holds max_Data-Loc_in root-tree t = d".t;
theorem :: SCM_COMP:12
for nt being NonTerminal of SCM-AE, tl, tr being bin-term holds
max_Data-Loc_in(nt-tree(tl, tr)) =
max(max_Data-Loc_in tl, max_Data-Loc_in tr);
theorem :: SCM_COMP:13
for term being bin-term,
s1, s2 being State of SCM
st for dn being Nat st dn <= max_Data-Loc_in term holds s1.dl.dn = s2.dl.dn
holds term @ s1 = term @ s2;
theorem :: SCM_COMP:14
for term being bin-term
for aux, n, k being Nat,
s being State-consisting of n, n, k, SCM-Compile(term, aux), <*>INT
st aux > max_Data-Loc_in term
ex i being Nat, u being State of SCM st
u = (Computation s).(i+1) & i+1 = len SCM-Compile(term, aux) &
IC (Computation s).i = il.(n+i) & IC u = il.(n+(i+1)) &
u.dl.aux = term@s &
for dn being Nat st dn < aux holds s.dl.dn = u.dl.dn;
theorem :: SCM_COMP:15
for term being bin-term,
aux, n, k being Nat,
s being State-consisting of n, n, k, SCM-Compile(term, aux)^<*halt SCM*>,
<*>INT
st aux > max_Data-Loc_in term
holds s is halting &
(Result s).dl.aux = term@s &
Complexity s = len SCM-Compile(term, aux);
Back to top