begin
theorem Th1:
for
I1,
I2 being
XFinSequence 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:
for
I1,
I2 being
XFinSequence 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 = Comput (ProgramPart s),
s,
k &
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:
(
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 :
for b1 being non empty strict with_terminals with_nonterminals with_useful_nonterminals binary DTConstrStr holds
( b1 = SCM-AE iff ( 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:] ) ) ) );
Lm3:
NonTerminals SCM-AE = [:1,5:]
by Def1;
:: deftheorem defines @ SCM_COMP:def 2 :
for t being Terminal of SCM-AE holds @ t = t;
theorem Th3:
theorem
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
[0 ,0 ] -tree t1,t2 is bin-term
func t1 - t2 -> bin-term equals
[0 ,1] -tree t1,
t2;
coherence
[0 ,1] -tree t1,t2 is bin-term
func t1 * t2 -> bin-term equals
[0 ,2] -tree t1,
t2;
coherence
[0 ,2] -tree t1,t2 is bin-term
func t1 div t2 -> bin-term equals
[0 ,3] -tree t1,
t2;
coherence
[0 ,3] -tree t1,t2 is bin-term
func t1 mod t2 -> bin-term equals
[0 ,4] -tree t1,
t2;
coherence
[0 ,4] -tree t1,t2 is bin-term
end;
:: deftheorem defines + SCM_COMP:def 3 :
for t1, t2 being bin-term holds t1 + t2 = [0 ,0 ] -tree t1,t2;
:: deftheorem defines - SCM_COMP:def 4 :
for t1, t2 being bin-term holds t1 - t2 = [0 ,1] -tree t1,t2;
:: deftheorem defines * SCM_COMP:def 5 :
for t1, t2 being bin-term holds t1 * t2 = [0 ,2] -tree t1,t2;
:: deftheorem defines div SCM_COMP:def 6 :
for t1, t2 being bin-term holds t1 div t2 = [0 ,3] -tree t1,t2;
:: deftheorem defines mod SCM_COMP:def 7 :
for t1, t2 being bin-term holds t1 mod t2 = [0 ,4] -tree t1,t2;
theorem
definition
let o be
NonTerminal of
SCM-AE ;
let 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
( ( 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 ;
deffunc H1( NonTerminal of SCM-AE , set , set , Integer, Integer) -> Element of INT = (id INT ) . ($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 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 :
for s being State of SCM
for term being bin-term
for b3 being Integer holds
( b3 = term @ s iff ex f being Function of (TS SCM-AE ),INT st
( b3 = 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 ) ) );
theorem Th6:
theorem Th7:
theorem
definition
let nt be
NonTerminal of
SCM-AE ;
let n be
Element of
NAT ;
func Selfwork nt,
n -> XFinSequence of the
Instructions 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
( ( nt = [0 ,0 ] implies <%(AddTo (dl. n),(dl. (n + 1)))%> is XFinSequence of the Instructions of SCM ) & ( nt = [0 ,1] implies <%(SubFrom (dl. n),(dl. (n + 1)))%> is XFinSequence of the Instructions of SCM ) & ( nt = [0 ,2] implies <%(MultBy (dl. n),(dl. (n + 1)))%> is XFinSequence of the Instructions of SCM ) & ( nt = [0 ,3] implies <%(Divide (dl. n),(dl. (n + 1)))%> is XFinSequence of the Instructions of SCM ) & ( nt = [0 ,4] implies <%(Divide (dl. n),(dl. (n + 1))),((dl. n) := (dl. (n + 1)))%> is XFinSequence of the Instructions of SCM ) )
;
consistency
for b1 being XFinSequence 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
canceled;canceled;deffunc H2(
NonTerminal of
SCM-AE ,
Function of
NAT ,
(the Instructions of SCM ^omega ),
Function of
NAT ,
(the Instructions of SCM ^omega ),
Element of
NAT )
-> Element of the
Instructions of
SCM ^omega =
(($2 . $4) ^ ($3 . ($4 + 1))) ^ (Down (Selfwork $1,$4));
deffunc H3(
Terminal of
SCM-AE ,
Element of
NAT )
-> Element of the
Instructions of
SCM ^omega =
Down <%((dl. $2) := (@ $1))%>;
func SCM-Compile -> Function of
(TS SCM-AE ),
(Funcs NAT ,(the Instructions of SCM ^omega )) means :
Def11k:
( ( for
t being
Terminal of
SCM-AE ex
g being
Function of
NAT ,
(the Instructions of SCM ^omega ) st
(
g = it . (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 ^omega ) st
(
g = it . (nt -tree t1,t2) &
f1 = it . t1 &
f2 = it . t2 & ( for
n being
Element of
NAT holds
g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork nt,n) ) ) ) );
existence
ex b1 being Function of (TS SCM-AE ),(Funcs NAT ,(the Instructions of SCM ^omega )) st
( ( for t being Terminal of SCM-AE ex g being Function of NAT ,(the Instructions of SCM ^omega ) st
( g = b1 . (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 ^omega ) st
( g = b1 . (nt -tree t1,t2) & f1 = b1 . t1 & f2 = b1 . t2 & ( for n being Element of NAT holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork nt,n) ) ) ) )
uniqueness
for b1, b2 being Function of (TS SCM-AE ),(Funcs NAT ,(the Instructions of SCM ^omega )) st ( for t being Terminal of SCM-AE ex g being Function of NAT ,(the Instructions of SCM ^omega ) st
( g = b1 . (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 ^omega ) st
( g = b1 . (nt -tree t1,t2) & f1 = b1 . t1 & f2 = b1 . t2 & ( for n being Element of NAT holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork nt,n) ) ) ) & ( for t being Terminal of SCM-AE ex g being Function of NAT ,(the Instructions of SCM ^omega ) st
( g = b2 . (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 ^omega ) st
( g = b2 . (nt -tree t1,t2) & f1 = b2 . t1 & f2 = b2 . t2 & ( for n being Element of NAT holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork nt,n) ) ) ) holds
b1 = b2
end;
:: deftheorem SCM_COMP:def 11 :
canceled;
:: deftheorem SCM_COMP:def 12 :
canceled;
:: deftheorem Def11k defines SCM-Compile SCM_COMP:def 13 :
for b1 being Function of (TS SCM-AE ),(Funcs NAT ,(the Instructions of SCM ^omega )) holds
( b1 = SCM-Compile iff ( ( for t being Terminal of SCM-AE ex g being Function of NAT ,(the Instructions of SCM ^omega ) st
( g = b1 . (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 ^omega ) st
( g = b1 . (nt -tree t1,t2) & f1 = b1 . t1 & f2 = b1 . t2 & ( for n being Element of NAT holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork nt,n) ) ) ) ) );
:: deftheorem defines SCM-Compile SCM_COMP:def 14 :
for term being bin-term
for aux being Element of NAT holds SCM-Compile term,aux = (SCM-Compile . term) . aux;
consider term9 being bin-term;
theorem Th9:
theorem Th10:
:: deftheorem Def12 defines d". SCM_COMP:def 15 :
for t being Terminal of SCM-AE
for b2 being Element of NAT holds
( b2 = d". t iff dl. b2 = t );
definition
deffunc H2(
Terminal of
SCM-AE )
-> Element of
NAT =
d". $1;
deffunc H3(
NonTerminal of
SCM-AE ,
set ,
set ,
Element of
NAT ,
Element of
NAT )
-> Element of
NAT =
max $4,$5;
let term be
bin-term;
func max_Data-Loc_in term -> Element of
NAT means :
Def13:
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 16 :
for term being bin-term
for b2 being Element of NAT holds
( b2 = max_Data-Loc_in term iff 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 ) ) );
consider Term being bin-term;
consider f being Function of (TS SCM-AE ),NAT such that
max_Data-Loc_in Term = f . Term
and
Lm6:
for t being Terminal of SCM-AE holds f . (root-tree t) = d". t
and
Lm7:
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:
Lm8:
NonTerminals SCM-AE = [:1,5:]
by Def1;
theorem Th12:
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;
Lm10:
now
let nt be
NonTerminal of
SCM-AE ;
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 ;
( nt ==> <*(root-label tl),(root-label tr)*> & S1[tl] & S1[tr] implies S1[nt -tree tl,tr] )assume that
nt ==> <*(root-label tl),(root-label tr)*>
and A1:
S1[
tl]
and A2:
S1[
tr]
;
S1[nt -tree tl,tr]thus
S1[
nt -tree tl,
tr]
verum
proof
let s1,
s2 be
State of
SCM ;
( ( 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 A3:
for
dn being
Element of
NAT st
dn <= max_Data-Loc_in (nt -tree tl,tr) holds
s1 . (dl. dn) = s2 . (dl. dn)
;
(nt -tree tl,tr) @ s1 = (nt -tree tl,tr) @ s2
then A5:
tl @ s1 = tl @ s2
by A1;
then A7:
tr @ s1 = tr @ s2
by A2;
(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 A5, A7, Th7;
verum
end;
end;
theorem Th13:
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 = Comput (ProgramPart s),s,(i + 1) & i + 1 = len (SCM-Compile $1,aux) & IC (Comput (ProgramPart s),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 Th14:
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 = Comput (ProgramPart s),
s,
(i + 1) &
i + 1
= len (SCM-Compile term,aux) &
IC (Comput (ProgramPart s),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) ) )
theorem
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) ^ <%(halt SCM )%>,
<*> INT st
aux > max_Data-Loc_in term holds
(
ProgramPart s halts_on s &
(Result (ProgramPart s),s) . (dl. aux) = term @ s &
LifeSpan (ProgramPart s),
s = len (SCM-Compile term,aux) )