:: SCM_COMP semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: SCM_COMP:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I1, I2 being FinSequence of the Instructions of SCM
for D being FinSequence of INT
for il, ps, ds being 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 )
proof end;

theorem Th2: :: SCM_COMP:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I1, I2 being FinSequence of the Instructions of SCM
for il, ps, ds, k, il1 being 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
proof end;

Lm1: 1 = { n where n is Nat : n < 1 }
by AXIOMS:30;

Lm2: 5 = { n where n is Nat : n < 5 }
by AXIOMS:30;

definition
func SCM-AE -> non empty strict binary with_terminals with_nonterminals with_useful_nonterminals 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 binary with_terminals with_nonterminals with_useful_nonterminals 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:] ) ) )
proof end;
uniqueness
for b1, b2 being non empty strict binary with_terminals with_nonterminals with_useful_nonterminals 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
proof end;
end;

:: deftheorem Def1 defines SCM-AE SCM_COMP:def 1 :
for b1 being non empty strict binary with_terminals with_nonterminals with_useful_nonterminals 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:] ) ) ) );

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;
:: original: -tree
redefine func nt -tree tl,tr -> bin-term;
coherence
nt -tree tl,tr is bin-term
proof end;
end;

definition
let t be Terminal of SCM-AE ;
:: original: root-tree
redefine func root-tree t -> bin-term;
coherence
root-tree t is bin-term by DTCONSTR:def 4;
end;

definition
let t be Terminal of SCM-AE ;
func @ t -> Data-Location equals :: SCM_COMP:def 2
t;
coherence
t is Data-Location
proof end;
end;

:: deftheorem defines @ SCM_COMP:def 2 :
for t being Terminal of SCM-AE holds @ t = t;

theorem Th3: :: SCM_COMP:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for nt being NonTerminal of SCM-AE holds
( nt = [0,0] or nt = [0,1] or nt = [0,2] or nt = [0,3] or nt = [0,4] )
proof end;

theorem :: SCM_COMP:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( [0,0] is NonTerminal of SCM-AE & [0,1] is NonTerminal of SCM-AE & [0,2] is NonTerminal of SCM-AE & [0,3] is NonTerminal of SCM-AE & [0,4] is NonTerminal of SCM-AE )
proof 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 :: SCM_COMP:def 3
[0,0] -tree t1,t2;
coherence
[0,0] -tree t1,t2 is bin-term
proof end;
func t1 - t2 -> bin-term equals :: SCM_COMP:def 4
[0,1] -tree t1,t2;
coherence
[0,1] -tree t1,t2 is bin-term
proof end;
func t1 * t2 -> bin-term equals :: SCM_COMP:def 5
[0,2] -tree t1,t2;
coherence
[0,2] -tree t1,t2 is bin-term
proof end;
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
proof end;
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
proof end;
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 :: SCM_COMP:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

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 ) ) )
proof end;
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 ) );

definition
let s be State of SCM ;
let t be Terminal of SCM-AE ;
:: original: .
redefine func s . t -> Integer;
coherence
s . t is Integer
proof end;
end;

definition
let D be non empty set ;
let f be Function of INT ,D;
let x be Integer;
:: original: .
redefine func f . x -> Element of D;
coherence
f . x is Element of D
proof end;
end;

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 ) )
proof end;
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
proof end;
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: :: SCM_COMP:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM
for t being Terminal of SCM-AE holds (root-tree t) @ s = s . t
proof end;

theorem Th7: :: SCM_COMP:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM
for nt being NonTerminal of SCM-AE
for tl, tr being bin-term holds (nt -tree tl,tr) @ s = nt -Meaning_on (tl @ s),(tr @ s)
proof end;

theorem :: SCM_COMP:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM
for 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 end;

definition
let nt be NonTerminal of SCM-AE ;
let n be 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)))*> ) ) )
proof end;
end;

:: deftheorem Def10 defines Selfwork SCM_COMP:def 10 :
for nt being NonTerminal of SCM-AE
for n being 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 Nat;
deffunc H1( Terminal of SCM-AE , 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 * , 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 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 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 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 Nat holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork nt,n) ) ) ) )
proof end;
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 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 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 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 Nat holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork nt,n) ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines SCM-Compile SCM_COMP:def 11 :
for term being bin-term
for aux being 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 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 Nat holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork nt,n) ) ) ) ) );

consider term' being bin-term, aux' being Nat;

consider f being Function of TS SCM-AE , Funcs NAT ,(the Instructions of SCM * ) such that
SCM-Compile term',aux' = (f . term') . aux' 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 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 Nat holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork nt,n) ) ) ) ) by Def11;

theorem Th9: :: SCM_COMP:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for t being Terminal of SCM-AE
for n being Nat holds SCM-Compile (root-tree t),n = <*((dl. n) := (@ t))*>
proof end;

theorem Th10: :: SCM_COMP:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for n being Nat
for 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 end;

definition
let t be Terminal of SCM-AE ;
func d". t -> Nat means :Def12: :: SCM_COMP:def 12
 dl. it = t;
existence
ex b1 being Nat st dl. b1 = t
proof end;
uniqueness
for b1, b2 being Nat st dl. b1 = t & dl. b2 = t holds
b1 = b2 by AMI_3:52;
end;

:: deftheorem Def12 defines d". SCM_COMP:def 12 :
for t being Terminal of SCM-AE
for b2 being Nat holds
( b2 = d". t iff dl. b2 = t );

definition
let term be bin-term;
deffunc H1( NonTerminal of SCM-AE , set , set , Nat, Nat) -> Element of NAT = max $4,$5;
deffunc H2( Terminal of SCM-AE ) -> Nat = d". $1;
func max_Data-Loc_in term -> 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 Nat st xl = f . tl & xr = f . tr holds
f . (nt -tree tl,tr) = max xl,xr ) );
existence
ex b1 being 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 Nat st xl = f . tl & xr = f . tr holds
f . (nt -tree tl,tr) = max xl,xr ) )
proof end;
uniqueness
for b1, b2 being 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 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 Nat st xl = f . tl & xr = f . tr holds
f . (nt -tree tl,tr) = max xl,xr ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines max_Data-Loc_in SCM_COMP:def 13 :
for term being bin-term
for b2 being 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 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
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 Nat st xl = f . tl & xr = f . tr holds
f . (nt -tree tl,tr) = max xl,xr ) ) by Def13;

theorem Th11: :: SCM_COMP:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for t being Terminal of SCM-AE holds max_Data-Loc_in (root-tree t) = d". t
proof end;

Lm6: NonTerminals SCM-AE = [:1,5:]
by Def1;

theorem Th12: :: SCM_COMP:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for nt being NonTerminal of SCM-AE
for 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 end;

defpred S1[ bin-term] means for s1, s2 being State of SCM st ( for dn being 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 ; :: thesis: S1[ root-tree s]
thus S1[ root-tree s] :: thesis: verum
proof
let s1, s2 be State of SCM ; :: thesis: ( ( for dn being Nat st dn <= max_Data-Loc_in (root-tree s) holds
s1 . (dl. dn) = s2 . (dl. dn) ) implies (root-tree s) @ s1 = (root-tree s) @ s2 )
assume A1: for dn being Nat st dn <= max_Data-Loc_in (root-tree s) holds
s1 . (dl. dn) = s2 . (dl. dn) ; :: thesis: (root-tree s) @ s1 = (root-tree s) @ s2
d". s <= max_Data-Loc_in (root-tree s) by Th11;
then A2: ( s1 . (dl. (d". s)) = s2 . (dl. (d". s)) & s1 . s = s1 . (dl. (d". s)) & s2 . s = s2 . (dl. (d". s)) ) by A1, Def12;
(root-tree s) @ s1 = s1 . s by Th6;
hence (root-tree s) @ s1 = (root-tree s) @ s2 by A2, Th6; :: thesis: verum
end;
end;

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 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 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
now
let dn be Nat; :: thesis: ( dn <= max_Data-Loc_in tl implies s1 . (dl. dn) = s2 . (dl. dn) )
assume A3: dn <= max_Data-Loc_in tl ; :: thesis: s1 . (dl. dn) = s2 . (dl. dn)
set ml = max_Data-Loc_in tl;
set mr = max_Data-Loc_in tr;
max_Data-Loc_in tl <= max (max_Data-Loc_in tl),(max_Data-Loc_in tr) by SQUARE_1:46;
then dn <= max (max_Data-Loc_in tl),(max_Data-Loc_in tr) by A3, XREAL_1:2;
then dn <= max_Data-Loc_in (nt -tree tl,tr) by Th12;
hence s1 . (dl. dn) = s2 . (dl. dn) by A2; :: thesis: verum
end;
then A4: tl @ s1 = tl @ s2 by A1;
now
let dn be Nat; :: thesis: ( dn <= max_Data-Loc_in tr implies s1 . (dl. dn) = s2 . (dl. dn) )
assume A5: dn <= max_Data-Loc_in tr ; :: thesis: s1 . (dl. dn) = s2 . (dl. dn)
set ml = max_Data-Loc_in tl;
set mr = max_Data-Loc_in tr;
max_Data-Loc_in tr <= max (max_Data-Loc_in tl),(max_Data-Loc_in tr) by SQUARE_1:46;
then dn <= max (max_Data-Loc_in tl),(max_Data-Loc_in tr) by A5, XREAL_1:2;
then dn <= max_Data-Loc_in (nt -tree tl,tr) by Th12;
hence s1 . (dl. dn) = s2 . (dl. dn) by A2; :: thesis: verum
end;
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for term being bin-term
for s1, s2 being State of SCM st ( for dn being Nat st dn <= max_Data-Loc_in term holds
s1 . (dl. dn) = s2 . (dl. dn) ) holds
term @ s1 = term @ s2
proof end;

set D = <*> INT ;

defpred S2[ bin-term] means for aux, n, k being 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 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 Nat st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) );

theorem Th14: :: SCM_COMP:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for term being bin-term
for aux, n, k being 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 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 Nat st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
proof end;

theorem :: SCM_COMP:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for term being bin-term
for aux, n, k being 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
( s is halting & (Result s) . (dl. aux) = term @ s & Complexity s = len (SCM-Compile term,aux) )
proof end;