begin
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
canceled;
theorem
canceled;
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 :
Def13:
( ( 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 Def13 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;
theorem Th9:
theorem Th10:
:: deftheorem Def15 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 :
Def16:
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 Def16 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) ) ) );
set Term = the bin-term;
consider f being Function of (TS SCM-AE),NAT such that
max_Data-Loc_in the bin-term = f . the bin-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
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 Def16;
theorem Th11:
Lm6:
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;
Lm8:
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 F being NAT -defined the Instructions of SCM -valued total Function
for aux, n, k being Element of NAT st Shift ((SCM-Compile ($1,aux)),n) c= F holds
for s being b3 -started State-consisting of k, <*> INT st aux > max_Data-Loc_in $1 holds
ex i being Element of NAT ex 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 Th14:
for
F being
NAT -defined the
Instructions of
SCM -valued total Function for
term being
bin-term for
aux,
n,
k being
Element of
NAT st
Shift (
(SCM-Compile (term,aux)),
n)
c= F holds
for
s being
b4 -started State-consisting of
k,
<*> INT st
aux > max_Data-Loc_in term holds
ex
i being
Element of
NAT ex
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) ) )
theorem