:: A compiler of arithmetic expressions for { \bf SCM }
:: by Grzegorz Bancerek and Piotr Rudnicki
::
:: Received December 30, 1993
:: Copyright (c) 1993-2026 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, AFINSQ_1, AMI_1, AMI_3, FINSEQ_1, SUBSET_1, ORDINAL4,
ARYTM_3, FUNCT_1, ARYTM_1, XXREAL_0, RELAT_1, FSM_1, BINTREE1, DTCONSTR,
STRUCT_0, XBOOLE_0, LANG1, AMI_2, ZFMISC_1, TDGROUP, TARSKI, CARD_1,
TREES_4, TREES_3, QC_LANG1, CAT_1, INT_1, TREES_2, MCART_1, GRAPHSP,
CONNSP_3, FUNCT_2, MSUALG_1, SCM_COMP, EXTPRO_1, VALUED_1, COMPOS_1,
NAT_1, FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
XCMPLX_0, XXREAL_0, INT_1, NAT_1, XTUPLE_0, MCART_1, FUNCT_1, FUNCT_2,
VALUED_1, TREES_2, TREES_3, TREES_4, AFINSQ_1, STRUCT_0, MEMSTR_0,
COMPOS_1, EXTPRO_1, AMI_2, AMI_3, FINSEQ_1, LANG1, BINTREE1, DTCONSTR,
PARTFUN1, PRE_POLY;
constructors DTCONSTR, BINTREE1, DOMAIN_1, PRE_POLY, RELSET_1, AMI_3,
XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2,
NUMBERS, XREAL_0, INT_1, TREES_3, STRUCT_0, DTCONSTR, BINTREE1, AMI_3,
AFINSQ_1, FINSEQ_1, COMPOS_0, MEMSTR_0, XTUPLE_0, NAT_1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0, RELAT_1;
equalities AMI_3, AFINSQ_1, SCM_INST;
theorems AXIOMS, TARSKI, ZFMISC_1, NAT_1, INT_1, FINSEQ_1, FINSEQ_2, AMI_3,
TREES_4, SCM_1, LANG1, DTCONSTR, BINTREE1, XBOOLE_0, TREES_3, FUNCT_1,
XREAL_1, XXREAL_0, CARD_1, AFINSQ_1, FUNCT_2, EXTPRO_1, MEMSTR_0, AMI_2,
XTUPLE_0, VALUED_1, ORDINAL1;
schemes BINTREE1;
begin
:: Auxiliary theorems about SCM
:: Arithmetic Expressions over a set of variables X with binary operators
:: We have resigned from the general treatment, to much ado.
:: For the future we need a machinery for talking about interpretations of
:: expressions.
Lm1: 1 = {n where n is Nat: n < 1} by AXIOMS:4;
Lm2: 5 = {n where n is Nat: n < 5} by AXIOMS:4;
definition
func SCM-AE -> binary with_terminals with_nonterminals
with_useful_nonterminals strict non empty DTConstrStr means
:Def1:
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:];
existence
proof
defpred X[set,set,set] means $1 in [:1, 5:];
consider G being binary strict non empty DTConstrStr such that
A1: the carrier of G = SCM-Data-Loc \/ [:1, 5:] and
A2: for x, y, z being Symbol of G holds x ==> <*y, z*> iff X[x,y,z]
from BINTREE1:sch 1;
A3: NonTerminals G = { t where t is Symbol of G : ex tnt being
FinSequence st t ==> tnt } by LANG1:def 3;
A4: NonTerminals G = [:1, 5:]
proof
thus NonTerminals G c= [:1, 5:]
proof
let x be object;
assume x in NonTerminals G;
then consider t being Symbol of G such that
A5: x = t and
A6: ex tnt being FinSequence st t ==> tnt by A3;
consider tnt being FinSequence such that
A7: t ==> tnt by A6;
ex x1, x2 being Symbol of G st tnt = <*x1,x2*> by A7,BINTREE1:def 4;
hence thesis by A2,A5,A7;
end;
let x be object;
assume
A8: x in [:1, 5:];
then reconsider t = x as Symbol of G by A1,XBOOLE_0:def 3;
t ==> <*t, t*> by A2,A8;
hence thesis by A3;
end;
then
A9: G is with_nonterminals by DTCONSTR:def 4;
A10: Terminals G = { t where t is Symbol of G : not ex tnt being
FinSequence st t ==> tnt } by LANG1:def 2;
A11: Terminals G = SCM-Data-Loc
proof
thus Terminals G c= SCM-Data-Loc
proof
let x be object;
assume x in Terminals G;
then consider t be Symbol of G such that
A12: x = t and
A13: not ex tnt being FinSequence st t ==> tnt by A10;
assume not x in SCM-Data-Loc;
then t in [:1, 5:] by A1,A12,XBOOLE_0:def 3;
then t ==> <*t, t*> by A2;
hence contradiction by A13;
end;
let x be object;
assume
A14: x in SCM-Data-Loc;
then
A15: ex y,z being object st y in {1} & z in NAT & x = [y,z] by ZFMISC_1:84;
reconsider t = x as Symbol of G by A1,A14,XBOOLE_0:def 3;
assume not x in Terminals G;
then consider tnt being FinSequence such that
A16: t ==> tnt by A10;
ex x1, x2 being Symbol of G st tnt = <*x1, x2*> by A16,BINTREE1:def 4;
then x in [:1, 5:] by A2,A16;
then consider x1, x2 being object such that
A17: x1 in 1 and
x2 in 5 and
A18: x = [x1,x2] by ZFMISC_1:84;
x = [0,x2] by A17,A18,CARD_1:49,TARSKI:def 1;
hence contradiction by A15,XTUPLE_0:1;
end;
now
A19: dl.1 in SCM-Data-Loc by AMI_2:def 16;
A20: dl.0 in SCM-Data-Loc by AMI_2:def 16;
then reconsider d0 = dl.0, d1 = dl.1 as Symbol of G by A1,A19,
XBOOLE_0:def 3;
A21: root-tree d1 in TS G by A11,A19,DTCONSTR:def 1;
root-tree d0 in TS G by A11,A20,DTCONSTR:def 1;
then reconsider
p = <* root-tree d0, root-tree d1*> as FinSequence of TS G by A21,
FINSEQ_2:13;
let nt be Symbol of G;
assume
A22: nt in NonTerminals G;
take p;
roots p = <* (root-tree d0).{}, (root-tree d1).{} *> by DTCONSTR:6
.= <* (root-tree d0).{}, d1 *> by TREES_4:3
.= <* d0, d1 *> by TREES_4:3;
hence nt ==> roots p by A2,A4,A22;
end;
then
A23: G is with_useful_nonterminals by DTCONSTR:def 5;
G is with_terminals by A11,DTCONSTR:def 3;
hence thesis by A2,A11,A4,A9,A23;
end;
uniqueness
proof
let S1, S2 be binary with_terminals with_nonterminals
with_useful_nonterminals strict non empty DTConstrStr;
assume that
A24: Terminals S1 = SCM-Data-Loc & NonTerminals S1 = [:1, 5:] and
A25: for x, y, z being Symbol of S1 holds x ==> <*y, z*> iff x in [:1,
5 :];
assume that
A26: Terminals S2 = SCM-Data-Loc & NonTerminals S2 = [:1, 5:] and
A27: for x, y, z being Symbol of S2 holds x ==> <*y, z*> iff x in [:1,
5 :];
A28: the carrier of S1 = Terminals S1 \/ NonTerminals S1 by LANG1:1
.= the carrier of S2 by A24,A26,LANG1:1;
the Rules of S1 = the Rules of S2
proof
set p1 = the Rules of S1, p2 = the Rules of S2;
let a, b be object;
hereby
assume
A29: [a,b] in p1;
then reconsider l = a as Symbol of S1 by ZFMISC_1:87;
reconsider r = b as Element of (the carrier of S1)* by A29,ZFMISC_1:87;
A30: l ==> r by A29,LANG1:def 1;
then consider x1, x2 being Symbol of S1 such that
A31: r = <* x1, x2 *> by BINTREE1:def 4;
reconsider l, x1, x2 as Symbol of S2 by A28;
l in [:1, 5:] by A25,A30,A31;
then l ==> <* x1, x2 *> by A27;
hence [a,b] in p2 by A31,LANG1:def 1;
end;
assume
A32: [a,b] in p2;
then reconsider l = a as Symbol of S2 by ZFMISC_1:87;
reconsider r = b as Element of (the carrier of S2)* by A32,ZFMISC_1:87;
A33: l ==> r by A32,LANG1:def 1;
then consider x1, x2 being Symbol of S2 such that
A34: r = <* x1, x2 *> by BINTREE1:def 4;
reconsider l, x1, x2 as Symbol of S1 by A28;
l in [:1, 5:] by A27,A33,A34;
then l ==> <* x1, x2 *> by A25;
hence thesis by A34,LANG1:def 1;
end;
hence thesis by A28;
end;
end;
definition
mode bin-term is Element of TS SCM-AE;
end;
Lm3: NonTerminals SCM-AE = [:1, 5:] by Def1;
definition
let nt be NonTerminal of SCM-AE;
let tl, tr be bin-term;
redefine func nt-tree (tl, tr) -> bin-term; :: redefines -tree (TREES_4, definition)
coherence
proof
nt ==> <*root-label tl, root-label tr*> by Def1,Lm3;
then nt ==> roots <*tl, tr*> by BINTREE1:2;
then nt-tree <*tl, tr*> in TS SCM-AE by DTCONSTR:def 1;
hence thesis by TREES_4:def 6;
end;
end;
definition
let t be Terminal of SCM-AE;
redefine func root-tree t -> bin-term; :: redefines root-tree (TREES_4, definition)
coherence by DTCONSTR:def 1;
end;
definition
let t be Terminal of SCM-AE;
func @t -> Data-Location equals
t;
coherence
proof
reconsider t as Element of SCM-Data-Loc by Def1;
t in Data-Locations SCM by AMI_3:27;
then reconsider t as Object of SCM;
t is Data-Location by AMI_2:def 16;
hence thesis;
end;
end;
theorem Th1:
for nt being NonTerminal of SCM-AE
holds nt = [0,0] or ... or nt = [0,4]
proof
let nt be NonTerminal of SCM-AE;
consider x, y being object such that
A1: x in 1 and
A2: y in 5 and
A3: nt = [x,y] by Lm3,ZFMISC_1:84;
A4: x = 0 by A1,CARD_1:49,TARSKI:def 1;
consider n being Nat such that
A5: y = n and
A6: n < 5 by A2,Lm2;
5 = 4+1;
then n <= 4 by A6,NAT_1:13;
then n = 0 or ... or n = 4;
hence thesis by A3,A4,A5;
end;
theorem
[0,0] is NonTerminal of SCM-AE &
... & [0,4] is
NonTerminal of SCM-AE
proof
A1: 3 in 5 & 4 in 5 by Lm2;
A2: 1 in 5 & 2 in 5 by Lm2;
0 in 1 & 0 in 5 by Lm1,Lm2;
hence thesis by A2,A1,Lm3,ZFMISC_1:87;
end;
then reconsider
nt0 = [0,0], nt1 = [0,1], nt2 = [0,2], nt3 = [0,3], nt4 = [0,4] as
NonTerminal of SCM-AE;
definition
let t1, t2 be bin-term;
func t1+t2 -> bin-term equals
[0,0]-tree(t1, t2);
coherence
proof
nt0-tree(t1, t2) in TS SCM-AE;
hence thesis;
end;
func t1-t2 -> bin-term equals
[0,1]-tree(t1, t2);
coherence
proof
nt1-tree(t1, t2) in TS SCM-AE;
hence thesis;
end;
func t1*t2 -> bin-term equals
[0,2]-tree(t1, t2);
coherence
proof
nt2-tree(t1, t2) in TS SCM-AE;
hence thesis;
end;
func t1 div t2 -> bin-term equals
[0,3]-tree(t1, t2);
coherence
proof
nt3-tree(t1, t2) in TS SCM-AE;
hence thesis;
end;
func t1 mod t2 -> bin-term equals
[0,4]-tree(t1, t2);
coherence
proof
nt4-tree(t1, t2) in TS SCM-AE;
hence thesis;
end;
end;
theorem :: 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
proof
let term be bin-term;
root-label term in the carrier of SCM-AE;
then term.{} in the carrier of SCM-AE by BINTREE1:def 1;
then
A1: term.{} in (Terminals SCM-AE) \/ (NonTerminals SCM-AE) by LANG1:1;
per cases by A1,XBOOLE_0:def 3;
suppose
term.{} in (Terminals SCM-AE);
then reconsider t = term.{} as Terminal of SCM-AE;
term = root-tree t by DTCONSTR:9;
hence thesis;
end;
suppose
term.{} in (NonTerminals SCM-AE);
then reconsider nt = term.{} as NonTerminal of SCM-AE;
consider ts being FinSequence of TS SCM-AE such that
A2: term = nt-tree ts and
A3: nt ==> roots ts by DTCONSTR:10;
ex x1, x2 being Symbol of SCM-AE st roots ts = <* x1, x2*> by A3,
BINTREE1:def 4;
then len roots ts = 2 by FINSEQ_1:44;
then
A4: dom roots ts = dom ts & dom roots ts = Seg 2 by FINSEQ_1:def 3
,TREES_3:def 18;
A5: 2 in Seg 2 by FINSEQ_1:2,TARSKI:def 2;
then consider tr being DecoratedTree such that
A6: tr = ts.2 and
(roots ts).2 = tr.{} by A4,TREES_3:def 18;
A7: 1 in Seg 2 by FINSEQ_1:2,TARSKI:def 2;
then consider tl being DecoratedTree such that
A8: tl = ts.1 and
(roots ts).1 = tl.{} by A4,TREES_3:def 18;
reconsider tl, tr as bin-term by A4,A7,A5,A8,A6,FINSEQ_2:11;
A9: nt = [0,0] or ... or nt = [0,4] by Th1;
len ts = 2 by A4,FINSEQ_1:def 3;
then ts = <*tl, tr*> by A8,A6,FINSEQ_1:44;
then term = nt-tree (tl, tr) by A2,TREES_4:def 6;
then term = tl+tr or term = tl-tr or term = tl*tr or term = tl div tr or
term = tl mod tr by A9;
hence thesis;
end;
end;
definition
let o be NonTerminal of SCM-AE, i, j be Integer;
func o-Meaning_on (i, j) -> Integer equals
:Def8:
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];
coherence;
consistency
proof
[0,0]`2 = 0 & [0,1]`2 = 1 & [0,2]`2 = 2 & [0,3]`2 = 3 & [0,4]`2 = 4;
hence thesis;
end;
end;
registration
let s be State of SCM;
let t be Terminal of SCM-AE;
cluster s.t -> integer;
coherence
proof
s.@t = s.t;
hence thesis;
end;
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; :: redefines . (FUNCT_1, definition)
coherence
proof
reconsider x as Element of INT by INT_1:def 2;
f.x is Element of D;
hence thesis;
end;
end;
set i2i = id INT;
deffunc U(NonTerminal of SCM-AE,set,set,Integer,Integer) = i2i.($1
-Meaning_on ($4, $5));
definition
let s be State of SCM;
let term be bin-term;
func term @ s -> Integer means
:Def9:
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);
existence
proof
deffunc V(Terminal of SCM-AE) = i2i.(s.$1);
consider f being Function of TS SCM-AE, INT such that
A1: (for t being Terminal of SCM-AE holds f.(root-tree t) = V(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)) = U(nt,rtl,rtr,xl, xr) from BINTREE1:sch 3;
reconsider IT = f.term as Element of INT;
take IT, f;
thus IT = f.term;
hereby
let t be Terminal of SCM-AE;
s.t in INT by INT_1:def 2;
then i2i.(s.t) = s.t by FUNCT_1:18;
hence f.(root-tree t) = s.t by A1;
end;
let nt be NonTerminal of SCM-AE, tl, tr be bin-term, rtl, rtr be Symbol of
SCM-AE;
assume
A2: rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl, rtr*>;
let xl, xr be Element of INT;
nt-Meaning_on (xl, xr) in INT by INT_1:def 2;
then i2i.(nt-Meaning_on (xl, xr)) = nt-Meaning_on (xl, xr) by FUNCT_1:18;
hence thesis by A1,A2;
end;
uniqueness
proof
deffunc V(Terminal of SCM-AE) = i2i.(s.$1);
let it1, it2 be Integer;
given f1 being Function of TS SCM-AE, INT such that
A3: it1 = f1.term and
A4: for t being Terminal of SCM-AE holds f1.(root-tree t) = s.t and
A5: 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 = f1.tl & xr = f1.tr
holds f1.(nt-tree (tl, tr)) = nt-Meaning_on (xl, xr);
A6: now
hereby
let t be Terminal of SCM-AE;
s.t in INT by INT_1:def 2;
then i2i.(s.t) = s.t by FUNCT_1:18;
hence f1.(root-tree t) = V(t) by A4;
end;
let nt be NonTerminal of SCM-AE, tl, tr be bin-term, rtl, rtr be Symbol
of SCM-AE such that
A7: rtl = root-label tl & rtr = root-label tr & nt ==> <* rtl, rtr
*>;
let xl, xr be Element of INT such that
A8: xl = f1.tl & xr = f1.tr;
nt-Meaning_on (xl, xr) in INT by INT_1:def 2;
then i2i.(nt-Meaning_on (xl, xr)) = nt-Meaning_on (xl, xr) by FUNCT_1:18;
hence f1.(nt-tree (tl, tr)) = U(nt,rtl, rtr,xl, xr) by A5,A7,A8;
end;
given f2 being Function of TS SCM-AE, INT such that
A9: it2 = f2.term and
A10: for t being Terminal of SCM-AE holds f2.(root-tree t) = s.t and
A11: 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 = f2.tl & xr = f2.tr
holds f2.(nt-tree (tl, tr)) = nt-Meaning_on (xl, xr);
A12: now
hereby
let t be Terminal of SCM-AE;
s.t in INT by INT_1:def 2;
then i2i.(s.t) = s.t by FUNCT_1:18;
hence f2.(root-tree t) = V(t) by A10;
end;
let nt be NonTerminal of SCM-AE, tl, tr be bin-term, rtl, rtr be Symbol
of SCM-AE such that
A13: rtl = root-label tl & rtr = root-label tr & nt ==> <* rtl, rtr
*>;
let xl, xr be Element of INT such that
A14: xl = f2.tl & xr = f2.tr;
nt-Meaning_on (xl, xr) in INT by INT_1:def 2;
then i2i.(nt-Meaning_on (xl, xr)) = nt-Meaning_on (xl, xr) by FUNCT_1:18;
hence f2.(nt-tree (tl, tr)) = U(nt,rtl, rtr,xl, xr) by A11,A13,A14;
end;
f1 = f2 from BINTREE1:sch 4 (A6, A12);
hence thesis by A3,A9;
end;
end;
theorem Th4:
for s being State of SCM, t being Terminal of SCM-AE holds
(root-tree t)@s = s.t
proof
let s be State of SCM, t be Terminal of SCM-AE;
ex f being Function of TS SCM-AE, INT st (root-tree t)@s = f.(root-tree
t) & (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) by Def9;
hence thesis;
end;
theorem Th5:
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)
proof
let s be State of SCM, nt be NonTerminal of SCM-AE, tl, tr be bin-term;
consider f being Function of TS SCM-AE, INT such that
A1: (nt-tree(tl, tr))@s = f.(nt-tree(tl,tr)) and
A2: for t being Terminal of SCM-AE holds f.(root-tree t) = s.t and
A3: 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) by Def9;
A4: nt ==> <* root-label tl, root-label tr *> by Def1,Lm3;
tl@s = f.tl & tr@s = f.tr by A2,A3,Def9;
hence thesis by A1,A3,A4;
end;
theorem :: 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)
proof
let s be State of SCM, tl, tr be bin-term;
thus (tl+tr)@s = nt0-Meaning_on (tl@s, tr@s) by Th5
.= tl@s + tr@s by Def8;
thus (tl-tr)@s = nt1-Meaning_on (tl@s, tr@s) by Th5
.= tl@s - tr@s by Def8;
thus (tl * tr)@s = nt2-Meaning_on (tl@s, tr@s) by Th5
.= tl@s * tr@s by Def8;
thus (tl div tr)@s = nt3-Meaning_on (tl@s, tr@s) by Th5
.= tl@s div tr@s by Def8;
thus (tl mod tr)@s = nt4-Meaning_on (tl@s, tr@s) by Th5
.= tl@s mod tr@s by Def8;
end;
definition
let nt be NonTerminal of SCM-AE, n be Nat;
func Selfwork(nt, n) -> XFinSequence of the InstructionsF of SCM equals
:Def10:
<%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];
coherence;
consistency
proof
[0,0]`2 = 0 & [0,1]`2 = 1 & [0,2]`2 = 2 & [0,3]`2 = 3 & [0,4]`2 = 4;
hence thesis;
end;
end;
definition
deffunc V(NonTerminal of SCM-AE,
sequence of (the InstructionsF of SCM)^omega,
sequence of (the InstructionsF of SCM)^omega, Nat)
= ($2.In($4,NAT))^($3.In($4+1,NAT))^Down Selfwork($1, $4);
deffunc U(Terminal of SCM-AE,Nat) = Down <%dl.$2:=@$1%>;
func SCM-Compile ->
Function of TS SCM-AE, Funcs(NAT, (the InstructionsF of SCM)^omega)
means
:Def11:
(for t being Terminal of SCM-AE
ex g being sequence of (the InstructionsF of SCM)^omega
st g = it.(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 sequence of (the InstructionsF of SCM)^omega
st g = it.(nt-tree (t1, t2)) & f1 = it.t1 &
f2 = it.t2 & for n being Nat
holds g.n = (f1.In(n,NAT))^(f2.In(n+1,NAT))^Selfwork(nt, n);
existence
proof
consider f being
Function of TS SCM-AE, Funcs(NAT, (the InstructionsF of SCM)^omega)
such that
A1: (for t being Terminal of SCM-AE
ex g being sequence of (the InstructionsF of SCM)^omega
st g = f.(root-tree t) & for n being Element of NAT
holds g.n = U(t,n))
& 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 sequence of (the InstructionsF of SCM)^omega
st g = f.(nt-tree (t1, t2)) & f1 = f.t1 & f2 = f
.t2 & for n being Element of NAT holds g.n = V(nt,f1,f2,n)
from BINTREE1:sch 5;
take f;
(for t being Terminal of SCM-AE
ex g being sequence of (the InstructionsF of SCM)^omega
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 sequence of (the InstructionsF of SCM)^omega
st g = f.(nt-tree (t1, t2)) & f1 = f.t1 & f2 = f
.t2 & for n being Nat
holds g.n = (f1.In(n,NAT))^(f2.In(n+1,NAT))^Selfwork(nt, n)
proof
thus for t being Terminal of SCM-AE
ex g being sequence of (the InstructionsF of SCM)^omega
st g = f.(root-tree t) & for n being Nat holds g.n = <%dl.n:=@t%>
proof let t being Terminal of SCM-AE;
consider g being sequence of (the InstructionsF of SCM)^omega
such that
A2: g = f.(root-tree t) and
A3: for n being Element of NAT holds g.n = U(t,n) by A1;
take g;
thus g = f.(root-tree t) by A2;
let n be Nat;
n in NAT by ORDINAL1:def 12;
then g.n = U(t,n) by A3;
hence thesis;
end;
thus 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 sequence of (the InstructionsF of SCM)^omega
st g = f.(nt-tree (t1, t2)) & f1 = f.t1 & f2 = f
.t2 & for n being Nat
holds g.n = (f1.In(n,NAT))^(f2.In(n+1,NAT))^Selfwork(nt, n)
proof let nt being NonTerminal of SCM-AE, t1, t2 being
bin-term, rtl, rtr being Symbol of SCM-AE such that
A4: rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl, rtr*>;
consider g, f1, f2 being sequence of
(the InstructionsF of SCM)^omega
such that
A5: g = f.(nt-tree (t1, t2)) & f1 = f.t1 & f2 = f.t2 and
A6: for n being Element of NAT
holds g.n = V(nt,f1,f2,n) by A4,A1;
take g,f1,f2;
thus g = f.(nt-tree (t1, t2)) & f1 = f.t1 & f2 = f.t2 by A5;
let n be Nat;
g.n = V(nt,f1,f2,n) by A6;
hence thesis;
end;
end;
hence thesis;
end;
uniqueness
proof
let f1, f2 be
Function of TS SCM-AE, Funcs(NAT, (the InstructionsF of SCM)^omega)
such that
A7: (for t being Terminal of SCM-AE
ex g being sequence of (the InstructionsF of SCM)^omega
st g = f1.(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, g1, g2 being sequence of (the InstructionsF of SCM)^omega
st g = f1.(nt-tree (t1, t2)) & g1 = f1.t1 & g2 =
f1.t2 & for n being Nat
holds g.n = (g1.In(n,NAT))^(g2.In(n+1,NAT))^Selfwork(nt, n) and
A8: (for t being Terminal of SCM-AE
ex g being sequence of (the InstructionsF of SCM)^omega
st g = f2.(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, g1, g2 being sequence of (the InstructionsF of SCM)^omega
st g = f2.(nt-tree (t1, t2)) & g1 = f2.t1 & g2 =
f2.t2 & for n being Nat
holds g.n = (g1.In(n,NAT))^(g2.In(n+1,NAT))^Selfwork(nt, n);
A9: (for t being Terminal of SCM-AE
ex g being sequence of (the InstructionsF of SCM)^omega
st g = f1.(root-tree t) & for n being Element of
NAT holds g.n = U(t,n)) &
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, g1, g2 being sequence of (the InstructionsF of SCM)^omega
st g = f1.(nt-tree (t1, t2)) & g1 = f1.t1 & g2 =
f1.t2 & for n being Element of NAT
holds g.n = V(nt,g1,g2,n)
proof
thus for t being Terminal of SCM-AE
ex g being sequence of (the InstructionsF of SCM)^omega
st g = f1.(root-tree t) & for n being Element of
NAT holds g.n = U(t,n)
proof let t be Terminal of SCM-AE;
consider g being sequence of (the InstructionsF of SCM)^omega
such that
A10: g = f1.(root-tree t) & for n being Nat holds g.n = <%dl.n:=@t%>
by A7;
take g;
thus thesis by A10;
end;
thus 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, g1, g2 being sequence of (the InstructionsF of SCM)^omega
st g = f1.(nt-tree (t1, t2)) & g1 = f1.t1 & g2 =
f1.t2 & for n being Element of NAT
holds g.n = V(nt,g1,g2,n)
proof let nt be NonTerminal of SCM-AE, t1, t2 be
bin-term, rtl, rtr be Symbol of SCM-AE such that
A11: rtl = root-label t1 & rtr = root-label t2 & nt ==> <* rtl, rtr *>;
consider g, g1, g2 being sequence of (the InstructionsF of SCM)^omega
such that
A12: g = f1.(nt-tree (t1, t2)) & g1 = f1.t1 & g2 =
f1.t2 & for n being Nat
holds g.n = (g1.In(n,NAT))^(g2.In(n+1,NAT))^Selfwork(nt, n) by A7,A11;
take g,g1,g2;
thus thesis by A12;
end;
end;
A13: (for t being Terminal of SCM-AE
ex g being sequence of (the InstructionsF of SCM)^omega
st g = f2.(root-tree t) & for n being Element of
NAT holds g.n = U(t,n)) &
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, g1, g2 being sequence of (the InstructionsF of SCM)^omega
st g = f2.(nt-tree (t1, t2)) & g1 = f2.t1 & g2 =
f2.t2 & for n being Element of NAT
holds g.n = V(nt,g1,g2,n)
proof
thus for t being Terminal of SCM-AE
ex g being sequence of (the InstructionsF of SCM)^omega
st g = f2.(root-tree t) & for n being Element of
NAT holds g.n = U(t,n)
proof let t be Terminal of SCM-AE;
consider g being sequence of (the InstructionsF of SCM)^omega
such that
A14: g = f2.(root-tree t) & for n being Nat holds g.n = <%dl.n:=@t%>
by A8;
take g;
thus thesis by A14;
end;
thus 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, g1, g2 being sequence of (the InstructionsF of SCM)^omega
st g = f2.(nt-tree (t1, t2)) & g1 = f2.t1 & g2 =
f2.t2 & for n being Element of NAT
holds g.n = V(nt,g1,g2,n)
proof let nt be NonTerminal of SCM-AE, t1, t2 be
bin-term, rtl, rtr be Symbol of SCM-AE such that
A15: rtl = root-label t1 & rtr = root-label t2 & nt ==> <* rtl, rtr *>;
consider g, g1, g2 being sequence of (the InstructionsF of SCM)^omega
such that
A16: g = f2.(nt-tree (t1, t2)) & g1 = f2.t1 & g2 =
f2.t2 & for n being Nat
holds g.n = (g1.In(n,NAT))^(g2.In(n+1,NAT))^Selfwork(nt, n) by A8,A15;
take g,g1,g2;
thus thesis by A16;
end;
end;
thus f1 = f2 from BINTREE1:sch 6 (A9, A13);
end;
end;
definition
let term be bin-term, aux be Nat;
func SCM-Compile(term, aux) ->
XFinSequence of the InstructionsF of SCM equals
(SCM-Compile.term).aux;
coherence
proof
reconsider f = SCM-Compile.term
as sequence of (the InstructionsF of SCM)^omega by FUNCT_2:66;
f.In(aux,NAT) in (the InstructionsF of SCM)^omega;
hence thesis by AFINSQ_1:def 7;
end;
end;
theorem Th7:
for t being Terminal of SCM-AE, n being Element of NAT holds
SCM-Compile(root-tree t, n) = <% dl.n:=@t %>
proof
let t be Terminal of SCM-AE, n be Element of NAT;
consider g being sequence of (the InstructionsF of SCM)^omega such
that
A1: g = SCM-Compile.root-tree t and
A2: for n being Nat holds g.n = <%dl.n:=@t%> by Def11;
thus thesis by A1,A2;
end;
theorem Th8:
for nt being NonTerminal of SCM-AE, t1, t2 being bin-term, n
being Element of 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)
proof
let nt be NonTerminal of SCM-AE, t1, t2 be bin-term, n be Element of NAT,
rtl, rtr be Symbol of SCM-AE;
assume
A1: rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl, rtr*>;
consider g, f1, f2 being sequence of (the InstructionsF of SCM)^omega
such that
A2: g = SCM-Compile.(nt-tree (t1, t2)) and
A3: f1 = SCM-Compile.t1 and
A4: f2 = SCM-Compile.t2 and
A5: for n being Nat holds g.n
= (f1.In(n,NAT))^(f2.In(n+1,NAT))^Selfwork(nt, n)
by A1,Def11;
g.n = (f1.In(n,NAT))^(f2.In(n+1,NAT))^Selfwork(nt, n) by A5;
hence SCM-Compile(nt-tree(t1,t2), n)
= SCM-Compile(t1, n)^SCM-Compile(t2, n+1)^Selfwork(nt, n) by A3,A4,A2;
end;
definition
let t be Terminal of SCM-AE;
func d".t -> Element of NAT means
:Def13:
dl.it = t;
existence
proof
Terminals SCM-AE = [:{1},NAT:] by Def1;
then consider x,y being object such that
A1: x in {1} and
A2: y in NAT and
A3: t = [x,y] by ZFMISC_1:84;
reconsider k = y as Element of NAT by A2;
take k;
thus thesis by A1,A3,TARSKI:def 1;
end;
uniqueness by AMI_3:10;
end;
definition
deffunc V(Terminal of SCM-AE) = d".$1;
deffunc U(NonTerminal of SCM-AE,set,set,Element of NAT,Element of NAT) = max
($4, $5);
let term be bin-term;
func max_Data-Loc_in term -> Element of NAT means
:Def14:
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 Element of NAT st xl = f
.tl & xr = f.tr holds f.(nt-tree (tl, tr)) = max(xl, xr);
existence
proof
consider f being Function of TS SCM-AE, NAT such that
A1: (for t being Terminal of SCM-AE holds f.(root-tree t) = V(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 NAT st xl = f.tl & xr = f.tr holds f.(nt
-tree (tl, tr)) = U(nt,rtl,rtr,xl,xr) from BINTREE1:sch 3;
reconsider fterm = f.term as Element of NAT;
take fterm, f;
thus thesis by A1;
end;
uniqueness
proof
let it1, it2 be Element of NAT;
given f1 being Function of TS SCM-AE, NAT such that
A2: it1 = f1.term and
A3: (for t being Terminal of SCM-AE holds f1.(root-tree t) = V(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 NAT st xl = f1.tl & xr = f1.tr holds f1.(nt
-tree (tl, tr)) = U(nt,rtl,rtr,xl, xr);
given f2 being Function of TS SCM-AE, NAT such that
A4: it2 = f2.term and
A5: (for t being Terminal of SCM-AE holds f2.(root-tree t) = V(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 NAT st xl = f2.tl & xr = f2.tr holds f2.(nt
-tree (tl, tr)) = U(nt,rtl,rtr,xl, xr);
f1 = f2 from BINTREE1:sch 4 (A3, A5);
hence thesis by A2,A4;
end;
end;
set Term = the bin-term;
consider f being Function of TS SCM-AE, NAT such that
max_Data-Loc_in Term = f.Term and
Lm4: for t being Terminal of SCM-AE holds f.(root-tree t) = d".t and
Lm5: 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 NAT st xl = f.tl & xr = f.tr holds f.(
nt-tree (tl, tr)) = max(xl, xr) by Def14;
theorem Th9:
for t being Terminal of SCM-AE holds max_Data-Loc_in root-tree t = d".t
proof
let t be Terminal of SCM-AE;
max_Data-Loc_in (root-tree t) = f.(root-tree t) qua Element of NAT by Def14
,Lm4,Lm5;
hence thesis by Lm4;
end;
Lm6: NonTerminals SCM-AE = [:1, 5:] by Def1;
theorem Th10:
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)
proof
let nt be NonTerminal of SCM-AE, tl, tr be bin-term;
A1: max_Data-Loc_in tl = f.tl & max_Data-Loc_in tr = f.tr by Def14,Lm4,Lm5;
nt ==> <*root-label tl, root-label tr*> & max_Data-Loc_in(nt-tree(tl, tr
)) = f.(nt-tree(tl, tr)) by Def1,Def14,Lm4,Lm5,Lm6;
hence thesis by A1,Lm5;
end;
defpred X[bin-term] means for s1, s2 being State of SCM st for dn being
Element of NAT st dn <= max_Data-Loc_in $1 holds s1.dl.dn = s2.dl.dn holds $1 @
s1 = $1 @ s2;
Lm7: now
let s be Terminal of SCM-AE;
thus X[root-tree s]
proof
let s1, s2 be State of SCM;
assume
A1: for dn being Element of NAT st dn <= max_Data-Loc_in root-tree s
holds s1.dl.dn = s2.dl.dn;
d".s <= max_Data-Loc_in root-tree s by Th9;
then
A2: s1.dl.d".s=s2.dl.d".s by A1;
A3: (root-tree s) @ s1 = s1.s by Th4;
s1.s = s1.dl.d".s & s2.s = s2.dl.d".s by Def13;
hence thesis by A2,A3,Th4;
end;
end;
Lm8: now
let nt be NonTerminal of SCM-AE, tl, tr be Element of TS SCM-AE;
assume that
nt ==> <* root-label tl, root-label tr *> and
A1: X[tl] and
A2: X[tr];
thus X[nt-tree(tl, tr)]
proof
let s1, s2 be State of SCM;
assume
A3: for dn being Element of NAT st dn <= max_Data-Loc_in (nt-tree (tl,
tr)) holds s1.dl.dn = s2.dl.dn;
now
set ml = max_Data-Loc_in tl, mr = max_Data-Loc_in tr;
let dn be Element of NAT;
A4: ml <= max(ml, mr) by XXREAL_0:25;
assume dn <= max_Data-Loc_in tl;
then dn <= max(ml, mr) by A4,XXREAL_0:2;
then dn <= max_Data-Loc_in (nt-tree (tl, tr)) by Th10;
hence s1.dl.dn = s2.dl.dn by A3;
end;
then
A5: tl@s1 = tl@s2 by A1;
now
set ml = max_Data-Loc_in tl, mr = max_Data-Loc_in tr;
let dn be Element of NAT;
A6: mr <= max(ml, mr) by XXREAL_0:25;
assume dn <= max_Data-Loc_in tr;
then dn <= max(ml, mr) by A6,XXREAL_0:2;
then dn <= max_Data-Loc_in (nt-tree (tl, tr)) by Th10;
hence s1.dl.dn = s2.dl.dn by A3;
end;
then
A7: tr@s1 = tr@s2 by A2;
nt-tree (tl, tr) @ s1 = nt-Meaning_on (tl@s1, tr@s1) by Th5;
hence thesis by A5,A7,Th5;
end;
end;
theorem Th11:
for term being bin-term, s1, s2 being State of SCM st for dn
being Element of NAT st dn <= max_Data-Loc_in term holds s1.dl.dn = s2.dl.dn
holds term @ s1 = term @ s2
proof
thus for t being bin-term holds X[t] from BINTREE1:sch 2 (Lm7, Lm8);
end;
reserve F for Instruction-Sequence of SCM;
defpred P[bin-term] means
for F for aux, n being Element of NAT
st Shift(SCM-Compile($1, aux),n) c= F
for s being n-started State of SCM
st aux > max_Data-Loc_in $1
ex i being Element of NAT, u being State of SCM st u = Comput(F,s,i+1) &
i+1 = len SCM-Compile($1, aux) & IC Comput(F,s,i)=(n+i) &
IC u = (n+(i+1)) & u.dl.aux = $1@s &
for dn being Element of NAT st dn < aux holds s.dl.dn = u.dl.dn;
theorem Th12:
for F for term being bin-term for aux, n being Element of NAT
st Shift(SCM-Compile(term, aux),n) c= F
for s being n-started State of SCM
st aux > max_Data-Loc_in term
ex i being Element of NAT, u being State of SCM st u =
Comput(F,s,i+1) & i+1 = len SCM-Compile(term, aux) & IC Comput(
F,s,i) =
(n+i) & IC u = (n+(i+1)) & u.dl.aux = term@s & for dn being Element of
NAT st dn < aux holds s.dl.dn = u.dl.dn
proof
A1: for nt being NonTerminal of SCM-AE, tl, tr being bin-term st nt ==> <*
root-label tl, root-label tr*> & P[tl] & P[tr] holds P[nt-tree(tl, tr)]
proof
let nt be NonTerminal of SCM-AE, tl, tr be bin-term;
assume that
A2: nt ==> <*root-label tl, root-label tr*> and
A3: P[tl] and
A4: P[tr];
let F;
let aux, n be Element of NAT such that
A5: Shift(SCM-Compile(nt-tree(tl, tr),aux),n) c= F;
let s be n-started State of SCM;
assume
A6: aux > max_Data-Loc_in (nt-tree(tl, tr));
A7: max_Data-Loc_in (nt-tree(tl, tr)) = max(max_Data-Loc_in tl,
max_Data-Loc_in tr) by Th10;
then max_Data-Loc_in tl <= max_Data-Loc_in (nt-tree(tl, tr))
by XXREAL_0:25;
then
A8: max_Data-Loc_in tl < aux by A6,XXREAL_0:2;
max_Data-Loc_in tr <= max_Data-Loc_in (nt-tree(tl, tr)) by A7,XXREAL_0:25;
then
A9: max_Data-Loc_in tr < aux by A6,XXREAL_0:2;
then
A10: max_Data-Loc_in tr < aux+1 by NAT_1:13;
A11: SCM-Compile(nt-tree(tl, tr), aux) = SCM-Compile(tl, aux)^SCM-Compile(
tr, aux+1)^Selfwork(nt, aux) by A2,Th8;
then SCM-Compile(nt-tree(tl, tr), aux) = SCM-Compile(tl, aux)^
(SCM-Compile(tr, aux+1)^Selfwork(nt, aux)) by AFINSQ_1:27;
then Shift(SCM-Compile(tl, aux),n) c= F by A5,AFINSQ_1:82;
then consider i1 being Element of NAT, u1 being State of SCM such that
A12: u1 = Comput(F,s,i1+1) and
A13: i1+1 = len SCM-Compile(tl, aux) and
IC Comput(F,s,i1) = n+i1 and
A14: IC u1 = n+(i1+1) and
A15: u1.dl.aux = tl@s and
A16: for dn being Element of NAT st dn < aux holds s.dl.dn = u1.dl.dn
by A3,A8;
A17: u1 is n+(i1+1)-started State of SCM
by A14,MEMSTR_0:def 12;
SCM-Compile(nt-tree(tl, tr), aux) = SCM-Compile(tl, aux)^
(SCM-Compile(tr, aux+1)^Selfwork(nt, aux)) by A11,AFINSQ_1:27;
then
Shift(SCM-Compile(tr, aux+1)^Selfwork(nt, aux),n+(i1+1)) c= F
by A5,A13,AFINSQ_1:83;
then
Shift(SCM-Compile(tr, aux+1),n+(i1+1)) c= F by AFINSQ_1:82;
then consider i2 being Element of NAT, u2 being State of SCM such that
A18: u2 = Comput(F,u1,i2+1) and
A19: i2+1 = len SCM-Compile(tr, aux+1) and
IC Comput(F,u1,i2) = (n+(i1+1)+i2) and
A20: IC u2 = (n+(i1+1)+(i2+1)) and
A21: u2.dl.(aux+1) = tr@u1 and
A22: for dn being Element of NAT st dn < aux+1 holds u1.dl.dn = u2.dl.
dn by A4,A10,A17;
A23: u2 = Comput(F,s,((i1+1)+(i2+1))) by A12,A18,EXTPRO_1:4;
A24: now
let n be Element of NAT;
assume n <= max_Data-Loc_in tr;
then n < aux by A9,XXREAL_0:2;
hence s.dl.n = u1.dl.n by A16;
end;
A25: aux < aux+1 by NAT_1:13;
A26: (nt-tree(tl, tr))@s = nt-Meaning_on(tl@s, tr@s) by Th5;
A27: len (SCM-Compile(tl, aux)^SCM-Compile(tr, aux+1)) = i1+1+(i2+1) by A13,A19
,AFINSQ_1:17;
nt = [0,0] or ... or nt = [0,4] by Th1;
then per cases;
suppose
A28: nt = [0, 0];
then
A29: nt-Meaning_on(tl@s, tr@s) = tl@s + tr@s by Def8;
take i = (i1+1)+(i2+1), u = Comput(F,s,i+1);
thus u = Comput(F,s,i+1);
A30: Selfwork(nt, aux) = <%AddTo(dl.aux, dl.(aux+1))%> by A28,Def10;
then
A31: len Selfwork(nt, aux) = 1 by AFINSQ_1:34;
hence i+1 = len SCM-Compile(nt-tree(tl, tr), aux) by A11,A27,AFINSQ_1:17;
thus IC Comput(F,s,i) = (n+i) by A12,A18,A20,EXTPRO_1:4;
len SCM-Compile(nt-tree(tl, tr), aux) = (i1+1)+(i2+1)+1 by A11,A27,A31,
AFINSQ_1:17;
then i < len SCM-Compile(nt-tree(tl, tr), aux) by NAT_1:13;
then i in dom SCM-Compile(nt-tree(tl, tr), aux) by AFINSQ_1:86;
then
A32: F.(n+i) = SCM-Compile(nt-tree(tl, tr), aux).i by A5,VALUED_1:51
.= AddTo(dl.aux, dl.(aux+1)) by A27,A11,A30,AFINSQ_1:36;
hence IC u = ((n+i)+1) by A20,A23,SCM_1:5
.= (n+(i+1));
thus u.dl.aux = u2.dl.aux + u2.dl.(aux+1) by A20,A23,A32,SCM_1:5
.= u1.dl.aux + tr@u1 by A21,A22,A25
.= (nt-tree(tl, tr))@s by A15,A26,A24,A29,Th11;
let dn be Element of NAT;
assume
A33: dn < aux;
then dn < aux+1 by NAT_1:13;
then
A34: u1.dl.dn = u2.dl.dn by A22;
dl.dn <> dl.aux by A33,AMI_3:10;
then u.dl.dn = u2.dl.dn by A20,A23,A32,SCM_1:5;
hence thesis by A16,A33,A34;
end;
suppose
A35: nt = [0, 1];
then
A36: nt-Meaning_on(tl@s, tr@s) = tl@s - tr@s by Def8;
take i = (i1+1)+(i2+1), u = Comput(F,s,i+1);
thus u = Comput(F,s,i+1);
A37: Selfwork(nt, aux) = <%SubFrom(dl.aux, dl.(aux+1))%> by A35,Def10;
then
A38: len Selfwork(nt, aux) = 1 by AFINSQ_1:34;
hence i+1 = len SCM-Compile(nt-tree(tl, tr), aux)
by A11,A27,AFINSQ_1:17;
thus IC Comput(F,s,i) = (n+i) by A12,A18,A20,EXTPRO_1:4;
len SCM-Compile(nt-tree(tl, tr), aux) = (i1+1)+(i2+1)+1 by A11,A27,A38,
AFINSQ_1:17;
then i < len SCM-Compile(nt-tree(tl, tr), aux) by NAT_1:13;
then i in dom SCM-Compile(nt-tree(tl, tr), aux) by AFINSQ_1:86;
then
A39: F.(n+i) = SCM-Compile(nt-tree(tl, tr), aux).i by A5,VALUED_1:51
.= SubFrom(dl.aux, dl.(aux+1)) by A11,A27,A37,AFINSQ_1:36;
hence IC u = ((n+i)+1) by A20,A23,SCM_1:6
.= (n+(i+1));
thus u.dl.aux = u2.dl.aux - u2.dl.(aux+1) by A20,A23,A39,SCM_1:6
.= u1.dl.aux - tr@u1 by A21,A22,A25
.= (nt-tree(tl, tr))@s by A15,A26,A24,A36,Th11;
let dn be Element of NAT;
assume
A40: dn < aux;
then dn < aux+1 by NAT_1:13;
then
A41: u1.dl.dn = u2.dl.dn by A22;
dl.dn <> dl.aux by A40,AMI_3:10;
then u.dl.dn = u2.dl.dn by A20,A23,A39,SCM_1:6;
hence thesis by A16,A40,A41;
end;
suppose
A42: nt = [0, 2];
then
A43: nt-Meaning_on(tl@s, tr@s) = tl@s * tr@s by Def8;
take i = (i1+1)+(i2+1), u = Comput(F,s,i+1);
thus u = Comput(F,s,i+1);
A44: Selfwork(nt, aux) = <%MultBy(dl.aux, dl.(aux+1))%> by A42,Def10;
then
A45: len Selfwork(nt, aux) = 1 by AFINSQ_1:34;
hence i+1 = len SCM-Compile(nt-tree(tl, tr), aux) by A11,A27,AFINSQ_1:17;
thus IC Comput(F,s,i) = (n+i) by A12,A18,A20,EXTPRO_1:4;
len SCM-Compile(nt-tree(tl, tr), aux) = (i1+1)+(i2+1)+1 by A11,A27,A45,
AFINSQ_1:17;
then i < len SCM-Compile(nt-tree(tl, tr), aux) by NAT_1:13;
then i in dom SCM-Compile(nt-tree(tl, tr), aux) by AFINSQ_1:86;
then
A46: F.(n+i) = SCM-Compile(nt-tree(tl, tr), aux).i by A5,VALUED_1:51
.= MultBy(dl.aux, dl.(aux+1)) by A11,A27,A44,AFINSQ_1:36;
hence IC u = ((n+i)+1) by A20,A23,SCM_1:7
.= (n+(i+1));
thus u.dl.aux = u2.dl.aux * u2.dl.(aux+1) by A20,A23,A46,SCM_1:7
.= u1.dl.aux * tr@u1 by A21,A22,A25
.= (nt-tree(tl, tr))@s by A15,A26,A24,A43,Th11;
let dn be Element of NAT;
assume
A47: dn < aux;
then dn < aux+1 by NAT_1:13;
then
A48: u1.dl.dn = u2.dl.dn by A22;
dl.dn <> dl.aux by A47,AMI_3:10;
then u.dl.dn = u2.dl.dn by A20,A23,A46,SCM_1:7;
hence thesis by A16,A47,A48;
end;
suppose
A49: nt = [0, 3];
take i = (i1+1)+(i2+1), u = Comput(F,s,i+1);
thus u = Comput(F,s,i+1);
A50: Selfwork(nt, aux) = <%Divide(dl.aux, dl.(aux+1))%> by A49,Def10;
then
A51: len Selfwork(nt, aux) = 1 by AFINSQ_1:34;
hence i+1 = len SCM-Compile(nt-tree(tl, tr), aux) by A11,A27,AFINSQ_1:17;
len SCM-Compile(nt-tree(tl, tr), aux) = (i1+1)+(i2+1)+1 by A11,A27,A51,
AFINSQ_1:17;
then i < len SCM-Compile(nt-tree(tl, tr), aux) by NAT_1:13;
then i in dom SCM-Compile(nt-tree(tl, tr), aux) by AFINSQ_1:86;
then
A52: F.(n+i) = SCM-Compile(nt-tree(tl, tr), aux).i by A5,VALUED_1:51
.= Divide(dl.aux, dl.(aux+1)) by A11,A27,A50,AFINSQ_1:36;
thus IC Comput(F,s,i) = (n+i) by A12,A18,A20,EXTPRO_1:4;
A53: nt-Meaning_on(tl@s, tr@s) = tl@s div tr@s by A49,Def8;
aux <> aux+1;
then
A54: dl.aux <> dl.(aux+1) by AMI_3:10;
hence IC u = ((n+i)+1) by A20,A23,A52,SCM_1:8
.= (n+(i+1));
thus u.dl.aux = u2.dl.aux div u2.dl.(aux+1) by A20,A23,A52,A54,SCM_1:8
.= u1.dl.aux div tr@u1 by A21,A22,A25
.= (nt-tree(tl, tr))@s by A15,A26,A24,A53,Th11;
let dn be Element of NAT;
assume
A55: dn < aux;
then
A56: dn < aux+1 by NAT_1:13;
then
A57: dl.dn <> dl.(aux+1) by AMI_3:10;
A58: u1.dl.dn = u2.dl.dn by A22,A56;
dl.dn <> dl.aux by A55,AMI_3:10;
then u.dl.dn = u2.dl.dn by A20,A23,A52,A54,A57,SCM_1:8;
hence thesis by A16,A55,A58;
end;
suppose
A59: nt = [0, 4];
then
A60: nt-Meaning_on(tl@s, tr@s) = tl@s mod tr@s by Def8;
set i = (i1+1)+(i2+1), u = Comput(F,s,i+1);
take k = i+1, v = Comput(F,s,k+1);
thus v = Comput(F,s,k+1);
A61: Selfwork(nt, aux) = <%Divide(dl.aux, dl.(aux+1)), dl.aux:=dl.( aux+
1) %> by A59,Def10;
then
A62: len Selfwork(nt, aux) = 2 by AFINSQ_1:38;
then
A63: 0 in dom Selfwork(nt, aux) by CARD_1:50,TARSKI:def 2;
A64: len SCM-Compile(nt-tree(tl, tr), aux) = (i1+1)+(i2+1)+(1+1) by A11,A27
,A62,AFINSQ_1:17;
hence k+1 = len SCM-Compile(nt-tree(tl, tr), aux);
A65: 1 in dom Selfwork(nt, aux) by A62,CARD_1:50,TARSKI:def 2;
k < len SCM-Compile(nt-tree(tl, tr), aux) by A64,XREAL_1:6;
then k in dom SCM-Compile(nt-tree(tl, tr), aux) by AFINSQ_1:86;
then
A66: F.(n+k) = SCM-Compile(nt-tree(tl, tr), aux).k by A5,VALUED_1:51
.= Selfwork(nt, aux).1 by A11,A27,A65,AFINSQ_1:def 3
.= dl.aux:=dl.(aux+1) by A61;
i+0 = i;
then i < len SCM-Compile(nt-tree(tl, tr), aux) by A64,XREAL_1:6;
then i in dom SCM-Compile(nt-tree(tl, tr), aux) by AFINSQ_1:86;
then
A67: F.(n+i) = SCM-Compile(nt-tree(tl, tr), aux).(i+0) by A5,VALUED_1:51
.= Selfwork(nt, aux).0 by A11,A27,A63,AFINSQ_1:def 3
.= Divide(dl.aux, dl.(aux+1)) by A61;
aux <> aux+1;
then
A68: dl.aux <> dl.(aux+1) by AMI_3:10;
hence
A69: IC Comput(F,s,k) = (n+i+1) by A20,A23,A67,SCM_1:8
.= (n+k);
hence IC v = ((n+k)+1) by A66,SCM_1:4
.= (n+(k+1));
thus v.dl.aux = u.dl.(aux+1) by A66,A69,SCM_1:4
.= u2.dl.aux mod u2.dl.(aux+1) by A20,A23,A67,A68,SCM_1:8
.= u1.dl.aux mod tr@u1 by A21,A22,A25
.= (nt-tree(tl, tr))@s by A15,A26,A24,A60,Th11;
let dn be Element of NAT;
assume
A70: dn < aux;
then
A71: dl.dn <> dl.aux by AMI_3:10;
A72: dn < aux+1 by A70,NAT_1:13;
then
A73: u1.dl.dn = u2.dl.dn by A22;
dl.dn <> dl.(aux+1) by A72,AMI_3:10;
then u.dl.dn = u2.dl.dn by A20,A23,A67,A68,A71,SCM_1:8;
then s.dl.dn = u.dl.dn by A16,A70,A73;
hence thesis by A66,A69,A71,SCM_1:4;
end;
end;
A74: for t being Terminal of SCM-AE holds P[root-tree t]
proof
let t be Terminal of SCM-AE;
let F;
let aux, n be Element of NAT
such that
A75: Shift(SCM-Compile(root-tree t, aux),n) c= F;
let s be n-started State of SCM;
assume aux > max_Data-Loc_in root-tree t;
take i = 0, u = Comput(F,s,0+1);
thus u = Comput(F,s,i+1);
A76: <%dl.aux:=@t%>.0 = dl.aux:=@t;
A77: SCM-Compile(root-tree t, aux) = <%dl.aux:=@t%> by Th7;
hence i+1 = len SCM-Compile(root-tree t, aux) by AFINSQ_1:34;
A78: s = Comput(F,s,0) by EXTPRO_1:2;
hence IC Comput(F,s,i) = (n+i) by MEMSTR_0:def 12;
len <%dl.aux:=@t%> = 1 & n+0 = n by AFINSQ_1:34;
then i in dom SCM-Compile(root-tree t, aux) by A77,AFINSQ_1:86;
then
A79: IC s = n & F.(n+0) = dl.aux:=@t
by A77,A76,A75,MEMSTR_0:def 12,VALUED_1:51;
hence IC u = (n+(i+1)) by A78,SCM_1:4;
thus u.dl.aux = s.t by A78,A79,SCM_1:4
.= (root-tree t)@s by Th4;
let dn be Element of NAT;
assume dn < aux;
then dl.dn <> dl.aux by AMI_3:10;
hence thesis by A78,A79,SCM_1:4;
end;
for term being bin-term holds P[term] from BINTREE1:sch 2(A74, A1);
hence thesis;
end;
theorem
for F for term being bin-term, aux, n being Element of NAT
st Shift(SCM-Compile(term, aux)^<%halt SCM%>,n) c= F
for s being n-started State of SCM
st aux
> max_Data-Loc_in term holds F halts_on s &
(Result(F,s)).dl.aux = term@s &
LifeSpan(F,s) = len SCM-Compile(term, aux)
proof let F;
let term be bin-term, aux, n be Element of NAT such that
A1: Shift(SCM-Compile(term, aux)^<%halt SCM%>,n) c= F;
let s be n-started State of SCM;
assume
A2: aux > max_Data-Loc_in term;
Shift(SCM-Compile(term, aux),n) c= F by A1,AFINSQ_1:82;
then consider i being Element of NAT, u being State of SCM such that
A3: u = Comput(F,s,i+1) and
A4: i+1 = len SCM-Compile(term, aux) and
A5: IC Comput(F,s,i)=(n+i) and
A6: IC u = (n+(i+1)) and
A7: u.dl.aux = term@s and
for dn being Element of NAT st dn < aux holds s.dl.dn = u.dl.dn
by A2,Th12;
len <%halt SCM%> = 1 by AFINSQ_1:34;
then len (SCM-Compile(term, aux)^<%halt SCM%>) = i+1+1 by A4,AFINSQ_1:17;
then i+1 < len (SCM-Compile(term, aux)^<%halt SCM%>) by NAT_1:13;
then i+1 in dom (SCM-Compile(term, aux)^<%halt SCM%>) by AFINSQ_1:86;
then
A8: F.(n+(i+1))=(SCM-Compile(term, aux)^<%halt SCM%>).(i+1) by A1,VALUED_1:51
.= halt SCM by A4,AFINSQ_1:36;
hence F halts_on s by A3,A6,EXTPRO_1:30;
thus (Result(F,s)).dl.aux = term@s by A3,A6,A7,A8,EXTPRO_1:7;
(n+i) <> (n+(i+1));
hence thesis by A3,A4,A5,A6,A8,EXTPRO_1:33;
end;