:: A compiler of arithmetic expressions for { \bf SCM }
:: by Grzegorz Bancerek and Piotr Rudnicki
::
:: Received December 30, 1993
:: Copyright (c) 1993 Association of Mizar Users
theorem Th1: :: SCM_COMP:1
for
I1,
I2 being
FinSequence of the
Instructions of
SCM for
D being
FinSequence of
INT for
il,
ps,
ds being
Element of
NAT for
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 Th2: :: SCM_COMP:2
for
I1,
I2 being
FinSequence of the
Instructions of
SCM for
il,
ps,
ds,
k,
il1 being
Element of
NAT for
s being
State-consisting of
il,
ps,
ds,
I1 ^ I2,
<*> INT for
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
Lm1:
1 = { n where n is Element of NAT : n < 1 }
by AXIOMS:30;
Lm2:
5 = { n where n is Element of NAT : n < 5 }
by AXIOMS:30;
definition
func SCM-AE -> non
empty strict with_terminals with_nonterminals with_useful_nonterminals binary DTConstrStr means :
Def1:
:: 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:] ) ) );
existence
ex b1 being non empty strict with_terminals with_nonterminals with_useful_nonterminals binary DTConstrStr st
( Terminals b1 = SCM-Data-Loc & NonTerminals b1 = [:1,5:] & ( for x, y, z being Symbol of b1 holds
( x ==> <*y,z*> iff x in [:1,5:] ) ) )
uniqueness
for b1, b2 being non empty strict with_terminals with_nonterminals with_useful_nonterminals binary DTConstrStr st Terminals b1 = SCM-Data-Loc & NonTerminals b1 = [:1,5:] & ( for x, y, z being Symbol of b1 holds
( x ==> <*y,z*> iff x in [:1,5:] ) ) & Terminals b2 = SCM-Data-Loc & NonTerminals b2 = [:1,5:] & ( for x, y, z being Symbol of b2 holds
( x ==> <*y,z*> iff x in [:1,5:] ) ) holds
b1 = b2
end;
:: deftheorem Def1 defines SCM-AE SCM_COMP:def 1 :
Lm3:
NonTerminals SCM-AE = [:1,5:]
by Def1;
:: deftheorem defines @ SCM_COMP:def 2 :
theorem Th3: :: SCM_COMP:3
theorem :: SCM_COMP:4
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 :: SCM_COMP:def 3
[0 ,0 ] -tree t1,
t2;
coherence
[0 ,0 ] -tree t1,t2 is bin-term
func t1 - t2 -> bin-term equals :: SCM_COMP:def 4
[0 ,1] -tree t1,
t2;
coherence
[0 ,1] -tree t1,t2 is bin-term
func t1 * t2 -> bin-term equals :: SCM_COMP:def 5
[0 ,2] -tree t1,
t2;
coherence
[0 ,2] -tree t1,t2 is bin-term
func t1 div t2 -> bin-term equals :: SCM_COMP:def 6
[0 ,3] -tree t1,
t2;
coherence
[0 ,3] -tree t1,t2 is bin-term
func t1 mod t2 -> bin-term equals :: SCM_COMP:def 7
[0 ,4] -tree t1,
t2;
coherence
[0 ,4] -tree t1,t2 is bin-term
end;
:: deftheorem defines + SCM_COMP:def 3 :
:: deftheorem defines - SCM_COMP:def 4 :
:: deftheorem defines * SCM_COMP:def 5 :
:: deftheorem defines div SCM_COMP:def 6 :
:: deftheorem defines mod SCM_COMP:def 7 :
theorem :: SCM_COMP:5
definition
let o be
NonTerminal of
SCM-AE ;
let i,
j be
Integer;
func o -Meaning_on i,
j -> Integer equals :
Def8:
:: 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];
coherence
( ( o = [0 ,0 ] implies i + j is Integer ) & ( o = [0 ,1] implies i - j is Integer ) & ( o = [0 ,2] implies i * j is Integer ) & ( o = [0 ,3] implies i div j is Integer ) & ( o = [0 ,4] implies i mod j is Integer ) )
;
consistency
for b1 being Integer holds
( ( o = [0 ,0 ] & o = [0 ,1] implies ( b1 = i + j iff b1 = i - j ) ) & ( o = [0 ,0 ] & o = [0 ,2] implies ( b1 = i + j iff b1 = i * j ) ) & ( o = [0 ,0 ] & o = [0 ,3] implies ( b1 = i + j iff b1 = i div j ) ) & ( o = [0 ,0 ] & o = [0 ,4] implies ( b1 = i + j iff b1 = i mod j ) ) & ( o = [0 ,1] & o = [0 ,2] implies ( b1 = i - j iff b1 = i * j ) ) & ( o = [0 ,1] & o = [0 ,3] implies ( b1 = i - j iff b1 = i div j ) ) & ( o = [0 ,1] & o = [0 ,4] implies ( b1 = i - j iff b1 = i mod j ) ) & ( o = [0 ,2] & o = [0 ,3] implies ( b1 = i * j iff b1 = i div j ) ) & ( o = [0 ,2] & o = [0 ,4] implies ( b1 = i * j iff b1 = i mod j ) ) & ( o = [0 ,3] & o = [0 ,4] implies ( b1 = i div j iff b1 = i mod j ) ) )
end;
:: deftheorem Def8 defines -Meaning_on SCM_COMP:def 8 :
for
o being
NonTerminal of
SCM-AE for
i,
j being
Integer holds
( (
o = [0 ,0 ] implies
o -Meaning_on i,
j = i + j ) & (
o = [0 ,1] implies
o -Meaning_on i,
j = i - j ) & (
o = [0 ,2] implies
o -Meaning_on i,
j = i * j ) & (
o = [0 ,3] implies
o -Meaning_on i,
j = i div j ) & (
o = [0 ,4] implies
o -Meaning_on i,
j = i mod j ) );
set i2i = id INT ;
definition
let s be
State of
SCM ;
let term be
bin-term;
deffunc H1(
NonTerminal of
SCM-AE ,
set ,
set ,
Integer,
Integer)
-> Element of
INT =
(id INT ) . ($1 -Meaning_on $4,$5);
deffunc H2(
Terminal of
SCM-AE )
-> Element of
INT =
(id INT ) . (s . $1);
func term @ s -> Integer means :
Def9:
:: 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 for
tl,
tr being
bin-term for
rtl,
rtr being
Symbol of
SCM-AE st
rtl = root-label tl &
rtr = root-label tr &
nt ==> <*rtl,rtr*> holds
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
ex b1 being Integer ex f being Function of TS SCM-AE , INT st
( b1 = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = s . t ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
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 ) )
uniqueness
for b1, b2 being Integer st ex f being Function of TS SCM-AE , INT st
( b1 = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = s . t ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
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 ) ) & ex f being Function of TS SCM-AE , INT st
( b2 = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = s . t ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
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 ) ) holds
b1 = b2
end;
:: deftheorem Def9 defines @ SCM_COMP:def 9 :
theorem Th6: :: SCM_COMP:6
theorem Th7: :: SCM_COMP:7
theorem :: SCM_COMP:8
definition
let nt be
NonTerminal of
SCM-AE ;
let n be
Element of
NAT ;
func Selfwork nt,
n -> Element of the
Instructions of
SCM * equals :
Def10:
:: 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];
coherence
( ( nt = [0 ,0 ] implies <*(AddTo (dl. n),(dl. (n + 1)))*> is Element of the Instructions of SCM * ) & ( nt = [0 ,1] implies <*(SubFrom (dl. n),(dl. (n + 1)))*> is Element of the Instructions of SCM * ) & ( nt = [0 ,2] implies <*(MultBy (dl. n),(dl. (n + 1)))*> is Element of the Instructions of SCM * ) & ( nt = [0 ,3] implies <*(Divide (dl. n),(dl. (n + 1)))*> is Element of the Instructions of SCM * ) & ( nt = [0 ,4] implies <*(Divide (dl. n),(dl. (n + 1))),((dl. n) := (dl. (n + 1)))*> is Element of the Instructions of SCM * ) )
;
consistency
for b1 being Element of the Instructions of SCM * holds
( ( nt = [0 ,0 ] & nt = [0 ,1] implies ( b1 = <*(AddTo (dl. n),(dl. (n + 1)))*> iff b1 = <*(SubFrom (dl. n),(dl. (n + 1)))*> ) ) & ( nt = [0 ,0 ] & nt = [0 ,2] implies ( b1 = <*(AddTo (dl. n),(dl. (n + 1)))*> iff b1 = <*(MultBy (dl. n),(dl. (n + 1)))*> ) ) & ( nt = [0 ,0 ] & nt = [0 ,3] implies ( b1 = <*(AddTo (dl. n),(dl. (n + 1)))*> iff b1 = <*(Divide (dl. n),(dl. (n + 1)))*> ) ) & ( nt = [0 ,0 ] & nt = [0 ,4] implies ( b1 = <*(AddTo (dl. n),(dl. (n + 1)))*> iff b1 = <*(Divide (dl. n),(dl. (n + 1))),((dl. n) := (dl. (n + 1)))*> ) ) & ( nt = [0 ,1] & nt = [0 ,2] implies ( b1 = <*(SubFrom (dl. n),(dl. (n + 1)))*> iff b1 = <*(MultBy (dl. n),(dl. (n + 1)))*> ) ) & ( nt = [0 ,1] & nt = [0 ,3] implies ( b1 = <*(SubFrom (dl. n),(dl. (n + 1)))*> iff b1 = <*(Divide (dl. n),(dl. (n + 1)))*> ) ) & ( nt = [0 ,1] & nt = [0 ,4] implies ( b1 = <*(SubFrom (dl. n),(dl. (n + 1)))*> iff b1 = <*(Divide (dl. n),(dl. (n + 1))),((dl. n) := (dl. (n + 1)))*> ) ) & ( nt = [0 ,2] & nt = [0 ,3] implies ( b1 = <*(MultBy (dl. n),(dl. (n + 1)))*> iff b1 = <*(Divide (dl. n),(dl. (n + 1)))*> ) ) & ( nt = [0 ,2] & nt = [0 ,4] implies ( b1 = <*(MultBy (dl. n),(dl. (n + 1)))*> iff b1 = <*(Divide (dl. n),(dl. (n + 1))),((dl. n) := (dl. (n + 1)))*> ) ) & ( nt = [0 ,3] & nt = [0 ,4] implies ( b1 = <*(Divide (dl. n),(dl. (n + 1)))*> iff b1 = <*(Divide (dl. n),(dl. (n + 1))),((dl. n) := (dl. (n + 1)))*> ) ) )
end;
:: deftheorem Def10 defines Selfwork SCM_COMP:def 10 :
for
nt being
NonTerminal of
SCM-AE for
n being
Element of
NAT holds
( (
nt = [0 ,0 ] implies
Selfwork nt,
n = <*(AddTo (dl. n),(dl. (n + 1)))*> ) & (
nt = [0 ,1] implies
Selfwork nt,
n = <*(SubFrom (dl. n),(dl. (n + 1)))*> ) & (
nt = [0 ,2] implies
Selfwork nt,
n = <*(MultBy (dl. n),(dl. (n + 1)))*> ) & (
nt = [0 ,3] implies
Selfwork nt,
n = <*(Divide (dl. n),(dl. (n + 1)))*> ) & (
nt = [0 ,4] implies
Selfwork nt,
n = <*(Divide (dl. n),(dl. (n + 1))),((dl. n) := (dl. (n + 1)))*> ) );
definition
let term be
bin-term;
let aux be
Element of
NAT ;
deffunc H1(
Terminal of
SCM-AE ,
Element of
NAT )
-> Element of the
Instructions of
SCM * =
<*((dl. $2) := (@ $1))*>;
deffunc H2(
NonTerminal of
SCM-AE ,
Function of
NAT ,the
Instructions of
SCM * ,
Function of
NAT ,the
Instructions of
SCM * ,
Element of
NAT )
-> Element of the
Instructions of
SCM * =
(($2 . $4) ^ ($3 . ($4 + 1))) ^ (Selfwork $1,$4);
func SCM-Compile term,
aux -> FinSequence of the
Instructions of
SCM means :
Def11:
:: SCM_COMP:def 11
ex
f being
Function of
TS SCM-AE ,
Funcs NAT ,
(the Instructions of SCM * ) st
(
it = (f . term) . aux & ( for
t being
Terminal of
SCM-AE ex
g being
Function of
NAT ,the
Instructions of
SCM * st
(
g = f . (root-tree t) & ( for
n being
Element of
NAT holds
g . n = <*((dl. n) := (@ t))*> ) ) ) & ( for
nt being
NonTerminal of
SCM-AE for
t1,
t2 being
bin-term for
rtl,
rtr being
Symbol of
SCM-AE st
rtl = root-label t1 &
rtr = root-label t2 &
nt ==> <*rtl,rtr*> holds
ex
g,
f1,
f2 being
Function of
NAT ,the
Instructions of
SCM * st
(
g = f . (nt -tree t1,t2) &
f1 = f . t1 &
f2 = f . t2 & ( for
n being
Element of
NAT holds
g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork nt,n) ) ) ) );
existence
ex b1 being FinSequence of the Instructions of SCM ex f being Function of TS SCM-AE , Funcs NAT ,(the Instructions of SCM * ) st
( b1 = (f . term) . aux & ( for t being Terminal of SCM-AE ex g being Function of NAT ,the Instructions of SCM * st
( g = f . (root-tree t) & ( for n being Element of NAT holds g . n = <*((dl. n) := (@ t))*> ) ) ) & ( for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being Function of NAT ,the Instructions of SCM * st
( g = f . (nt -tree t1,t2) & f1 = f . t1 & f2 = f . t2 & ( for n being Element of NAT holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork nt,n) ) ) ) )
uniqueness
for b1, b2 being FinSequence of the Instructions of SCM st ex f being Function of TS SCM-AE , Funcs NAT ,(the Instructions of SCM * ) st
( b1 = (f . term) . aux & ( for t being Terminal of SCM-AE ex g being Function of NAT ,the Instructions of SCM * st
( g = f . (root-tree t) & ( for n being Element of NAT holds g . n = <*((dl. n) := (@ t))*> ) ) ) & ( for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being Function of NAT ,the Instructions of SCM * st
( g = f . (nt -tree t1,t2) & f1 = f . t1 & f2 = f . t2 & ( for n being Element of NAT holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork nt,n) ) ) ) ) & ex f being Function of TS SCM-AE , Funcs NAT ,(the Instructions of SCM * ) st
( b2 = (f . term) . aux & ( for t being Terminal of SCM-AE ex g being Function of NAT ,the Instructions of SCM * st
( g = f . (root-tree t) & ( for n being Element of NAT holds g . n = <*((dl. n) := (@ t))*> ) ) ) & ( for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being Function of NAT ,the Instructions of SCM * st
( g = f . (nt -tree t1,t2) & f1 = f . t1 & f2 = f . t2 & ( for n being Element of NAT holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork nt,n) ) ) ) ) holds
b1 = b2
end;
:: deftheorem Def11 defines SCM-Compile SCM_COMP:def 11 :
for
term being
bin-term for
aux being
Element of
NAT for
b3 being
FinSequence of the
Instructions of
SCM holds
(
b3 = SCM-Compile term,
aux iff ex
f being
Function of
TS SCM-AE ,
Funcs NAT ,
(the Instructions of SCM * ) st
(
b3 = (f . term) . aux & ( for
t being
Terminal of
SCM-AE ex
g being
Function of
NAT ,the
Instructions of
SCM * st
(
g = f . (root-tree t) & ( for
n being
Element of
NAT holds
g . n = <*((dl. n) := (@ t))*> ) ) ) & ( for
nt being
NonTerminal of
SCM-AE for
t1,
t2 being
bin-term for
rtl,
rtr being
Symbol of
SCM-AE st
rtl = root-label t1 &
rtr = root-label t2 &
nt ==> <*rtl,rtr*> holds
ex
g,
f1,
f2 being
Function of
NAT ,the
Instructions of
SCM * st
(
g = f . (nt -tree t1,t2) &
f1 = f . t1 &
f2 = f . t2 & ( for
n being
Element of
NAT holds
g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork nt,n) ) ) ) ) );
consider term' being bin-term;
consider f being Function of TS SCM-AE , Funcs NAT ,(the Instructions of SCM * ) such that
SCM-Compile term',0 = (f . term') . 0
and
Lm4:
( ( for t being Terminal of SCM-AE ex g being Function of NAT ,the Instructions of SCM * st
( g = f . (root-tree t) & ( for n being Element of NAT holds g . n = <*((dl. n) := (@ t))*> ) ) ) & ( for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being Function of NAT ,the Instructions of SCM * st
( g = f . (nt -tree t1,t2) & f1 = f . t1 & f2 = f . t2 & ( for n being Element of NAT holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork nt,n) ) ) ) )
by Def11;
theorem Th9: :: SCM_COMP:9
theorem Th10: :: SCM_COMP:10
:: deftheorem Def12 defines d". SCM_COMP:def 12 :
definition
let term be
bin-term;
deffunc H1(
NonTerminal of
SCM-AE ,
set ,
set ,
Element of
NAT ,
Element of
NAT )
-> Element of
NAT =
max $4,$5;
deffunc H2(
Terminal of
SCM-AE )
-> Element of
NAT =
d". $1;
func max_Data-Loc_in term -> Element of
NAT means :
Def13:
:: 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 for
tl,
tr being
bin-term for
rtl,
rtr being
Symbol of
SCM-AE st
rtl = root-label tl &
rtr = root-label tr &
nt ==> <*rtl,rtr*> holds
for
xl,
xr being
Element of
NAT st
xl = f . tl &
xr = f . tr holds
f . (nt -tree tl,tr) = max xl,
xr ) );
existence
ex b1 being Element of NAT ex f being Function of TS SCM-AE , NAT st
( b1 = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = d". t ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of NAT st xl = f . tl & xr = f . tr holds
f . (nt -tree tl,tr) = max xl,xr ) )
uniqueness
for b1, b2 being Element of NAT st ex f being Function of TS SCM-AE , NAT st
( b1 = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = d". t ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of NAT st xl = f . tl & xr = f . tr holds
f . (nt -tree tl,tr) = max xl,xr ) ) & ex f being Function of TS SCM-AE , NAT st
( b2 = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = d". t ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of NAT st xl = f . tl & xr = f . tr holds
f . (nt -tree tl,tr) = max xl,xr ) ) holds
b1 = b2
end;
:: deftheorem Def13 defines max_Data-Loc_in SCM_COMP:def 13 :
consider Term being bin-term;
consider f being Function of TS SCM-AE , NAT such that
max_Data-Loc_in Term = f . Term
and
Lm5:
( ( for t being Terminal of SCM-AE holds f . (root-tree t) = d". t ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of NAT st xl = f . tl & xr = f . tr holds
f . (nt -tree tl,tr) = max xl,xr ) )
by Def13;
theorem Th11: :: SCM_COMP:11
Lm6:
NonTerminals SCM-AE = [:1,5:]
by Def1;
theorem Th12: :: SCM_COMP:12
defpred S1[ 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;
Lm8:
now
let nt be
NonTerminal of
SCM-AE ;
:: thesis: for tl, tr being Element of TS SCM-AE st nt ==> <*(root-label tl),(root-label tr)*> & S1[tl] & S1[tr] holds
S1[nt -tree tl,tr]let tl,
tr be
Element of
TS SCM-AE ;
:: thesis: ( nt ==> <*(root-label tl),(root-label tr)*> & S1[tl] & S1[tr] implies S1[nt -tree tl,tr] )assume A1:
(
nt ==> <*(root-label tl),(root-label tr)*> &
S1[
tl] &
S1[
tr] )
;
:: thesis: S1[nt -tree tl,tr]thus
S1[
nt -tree tl,
tr]
:: thesis: verum
proof
let s1,
s2 be
State of
SCM ;
:: thesis: ( ( for dn being Element of NAT st dn <= max_Data-Loc_in (nt -tree tl,tr) holds
s1 . (dl. dn) = s2 . (dl. dn) ) implies (nt -tree tl,tr) @ s1 = (nt -tree tl,tr) @ s2 )
assume A2:
for
dn being
Element of
NAT st
dn <= max_Data-Loc_in (nt -tree tl,tr) holds
s1 . (dl. dn) = s2 . (dl. dn)
;
:: thesis: (nt -tree tl,tr) @ s1 = (nt -tree tl,tr) @ s2
then A4:
tl @ s1 = tl @ s2
by A1;
then A6:
tr @ s1 = tr @ s2
by A1;
(nt -tree tl,tr) @ s1 = nt -Meaning_on (tl @ s1),
(tr @ s1)
by Th7;
hence
(nt -tree tl,tr) @ s1 = (nt -tree tl,tr) @ s2
by A4, A6, Th7;
:: thesis: verum
end;
end;
theorem Th13: :: SCM_COMP:13
set D = <*> INT ;
defpred S2[ bin-term] means for aux, n, k being Element of NAT
for s being State-consisting of n,n,k, SCM-Compile $1,aux, <*> INT st aux > max_Data-Loc_in $1 holds
ex i being Element of NAT ex u being State of SCM st
( u = Computation s,(i + 1) & i + 1 = len (SCM-Compile $1,aux) & IC (Computation s,i) = il. (n + i) & IC u = il. (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 Th14: :: SCM_COMP:14
for
term being
bin-term for
aux,
n,
k being
Element of
NAT for
s being
State-consisting of
n,
n,
k,
SCM-Compile term,
aux,
<*> INT st
aux > max_Data-Loc_in term holds
ex
i being
Element of
NAT ex
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
Element of
NAT st
dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
theorem :: SCM_COMP:15