:: A compiler of arithmetic expressions for { \bf SCM } :: by Grzegorz Bancerek and Piotr Rudnicki :: :: Received December 30, 1993 :: Copyright (c) 1993-2012 Association of Mizar Users begin Lm1: 1 = { n where n is Element of NAT : n < 1 } by AXIOMS:4; Lm2: 5 = { n where n is Element of NAT : n < 5 } by AXIOMS:4; 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:] ) ) ) proofend; 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 proofend; 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:] ) ) ) ); 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 funcnt -tree (tl,tr) -> bin-term; coherence nt -tree (tl,tr) is bin-term proofend; 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_1; end; definition let t be Terminal of SCM-AE; func @ t -> Data-Location equals :: SCM_COMP:def 2 t; coherence t is Data-Location proofend; end; :: deftheorem defines @ SCM_COMP:def_2_:_ for t being Terminal of SCM-AE holds @ t = t; theorem Th1: :: SCM_COMP:1 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] ) proofend; theorem :: SCM_COMP:2 ( [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 ) proofend; 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; funct1 + t2 -> bin-term equals :: SCM_COMP:def 3 [0,0] -tree (t1,t2); coherence [0,0] -tree (t1,t2) is bin-term proofend; funct1 - t2 -> bin-term equals :: SCM_COMP:def 4 [0,1] -tree (t1,t2); coherence [0,1] -tree (t1,t2) is bin-term proofend; funct1 * t2 -> bin-term equals :: SCM_COMP:def 5 [0,2] -tree (t1,t2); coherence [0,2] -tree (t1,t2) is bin-term proofend; funct1 div t2 -> bin-term equals :: SCM_COMP:def 6 [0,3] -tree (t1,t2); coherence [0,3] -tree (t1,t2) is bin-term proofend; funct1 mod t2 -> bin-term equals :: SCM_COMP:def 7 [0,4] -tree (t1,t2); coherence [0,4] -tree (t1,t2) is bin-term proofend; 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:3 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 ) ) proofend; definition let o be NonTerminal of SCM-AE; let i, j be Integer; funco -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 ) ) ) proofend; 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 ) ); registration let s be State of SCM; let t be Terminal of SCM-AE; clusters . t -> integer ; coherence s . t is integer proofend; end; definition let D be non empty set ; let f be Function of INT,D; let x be Integer; :: original:. redefine funcf . x -> Element of D; coherence f . x is Element of D proofend; end; 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; functerm @ 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) ) ) proofend; 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 proofend; 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 Th4: :: SCM_COMP:4 for s being State of SCM for t being Terminal of SCM-AE holds (root-tree t) @ s = s . t proofend; theorem Th5: :: SCM_COMP:5 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)) proofend; theorem :: SCM_COMP:6 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) ) proofend; definition let nt be NonTerminal of SCM-AE; let n be Element of NAT ; func Selfwork (nt,n) -> XFinSequence of the InstructionsF 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 XFinSequence of the InstructionsF of SCM ) & ( nt = [0,1] implies <%(SubFrom ((dl. n),(dl. (n + 1))))%> is XFinSequence of the InstructionsF of SCM ) & ( nt = [0,2] implies <%(MultBy ((dl. n),(dl. (n + 1))))%> is XFinSequence of the InstructionsF of SCM ) & ( nt = [0,3] implies <%(Divide ((dl. n),(dl. (n + 1))))%> is XFinSequence of the InstructionsF of SCM ) & ( nt = [0,4] implies <%(Divide ((dl. n),(dl. (n + 1)))),((dl. n) := (dl. (n + 1)))%> is XFinSequence of the InstructionsF of SCM ) ) ; consistency for b1 being XFinSequence of the InstructionsF 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)))%> ) ) ) proofend; 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 deffunc H2( NonTerminal of SCM-AE, Function of NAT,( the InstructionsF of SCM ^omega), Function of NAT,( the InstructionsF of SCM ^omega), Element of NAT ) -> Element of the InstructionsF of SCM ^omega = (($2 . $4) ^ ($3 . ($4 + 1))) ^ (Down (Selfwork ($1,$4))); deffunc H3( Terminal of SCM-AE, Element of NAT ) -> Element of the InstructionsF of SCM ^omega = Down <%((dl. $2) := (@ $1))%>; func SCM-Compile -> Function of (TS SCM-AE),(Funcs (NAT,( the InstructionsF of SCM ^omega))) means :Def11: :: SCM_COMP:def 11 ( ( for t being Terminal of SCM-AE ex g being Function of NAT,( the InstructionsF 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 InstructionsF 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 InstructionsF of SCM ^omega))) st ( ( for t being Terminal of SCM-AE ex g being Function of NAT,( the InstructionsF 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 InstructionsF 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)) ) ) ) ) proofend; uniqueness for b1, b2 being Function of (TS SCM-AE),(Funcs (NAT,( the InstructionsF of SCM ^omega))) st ( for t being Terminal of SCM-AE ex g being Function of NAT,( the InstructionsF 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 InstructionsF 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 InstructionsF 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 InstructionsF 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 proofend; end; :: deftheorem Def11 defines SCM-Compile SCM_COMP:def_11_:_ for b1 being Function of (TS SCM-AE),(Funcs (NAT,( the InstructionsF of SCM ^omega))) holds ( b1 = SCM-Compile iff ( ( for t being Terminal of SCM-AE ex g being Function of NAT,( the InstructionsF 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 InstructionsF 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)) ) ) ) ) ); definition let term be bin-term; let aux be Element of NAT ; func SCM-Compile (term,aux) -> XFinSequence of the InstructionsF of SCM equals :: SCM_COMP:def 12 (SCM-Compile . term) . aux; coherence (SCM-Compile . term) . aux is XFinSequence of the InstructionsF of SCM proofend; end; :: deftheorem defines SCM-Compile SCM_COMP:def_12_:_ for term being bin-term for aux being Element of NAT holds SCM-Compile (term,aux) = (SCM-Compile . term) . aux; theorem Th7: :: SCM_COMP:7 for t being Terminal of SCM-AE for n being Element of NAT holds SCM-Compile ((root-tree t),n) = <%((dl. n) := (@ t))%> proofend; theorem Th8: :: SCM_COMP:8 for nt being NonTerminal of SCM-AE for t1, t2 being bin-term for n being Element of 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)) proofend; definition let t be Terminal of SCM-AE; func d". t -> Element of NAT means :Def13: :: SCM_COMP:def 13 dl. it = t; existence ex b1 being Element of NAT st dl. b1 = t proofend; uniqueness for b1, b2 being Element of NAT st dl. b1 = t & dl. b2 = t holds b1 = b2 by AMI_3:10; end; :: deftheorem Def13 defines d". SCM_COMP:def_13_:_ 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 :Def14: :: SCM_COMP:def 14 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) ) ) proofend; 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 proofend; end; :: deftheorem Def14 defines max_Data-Loc_in SCM_COMP:def_14_:_ 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 Def14; theorem Th9: :: SCM_COMP:9 for t being Terminal of SCM-AE holds max_Data-Loc_in (root-tree t) = d". t proofend; Lm6: NonTerminals SCM-AE = [:1,5:] by Def1; theorem Th10: :: SCM_COMP:10 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)) proofend; 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; Lm7: now__::_thesis:_for_s_being_Terminal_of_SCM-AE_holds_S1[_root-tree_s] 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 Element of 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 Element of 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 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 (root-tree s) @ s1 = (root-tree s) @ s2 by A2, A3, Th4; ::_thesis: verum end; end; Lm8: now__::_thesis:_for_nt_being_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 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 that nt ==> <*(root-label tl),(root-label tr)*> and A1: S1[tl] and A2: 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 A3: 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 now__::_thesis:_for_dn_being_Element_of_NAT_st_dn_<=_max_Data-Loc_in_tl_holds_ s1_._(dl._dn)_=_s2_._(dl._dn) set ml = max_Data-Loc_in tl; set mr = max_Data-Loc_in tr; let dn be Element of NAT ; ::_thesis: ( dn <= max_Data-Loc_in tl implies s1 . (dl. dn) = s2 . (dl. dn) ) A4: max_Data-Loc_in tl <= max ((max_Data-Loc_in tl),(max_Data-Loc_in tr)) by XXREAL_0:25; assume dn <= max_Data-Loc_in tl ; ::_thesis: s1 . (dl. dn) = s2 . (dl. dn) then dn <= max ((max_Data-Loc_in tl),(max_Data-Loc_in tr)) 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; ::_thesis: verum end; then A5: tl @ s1 = tl @ s2 by A1; now__::_thesis:_for_dn_being_Element_of_NAT_st_dn_<=_max_Data-Loc_in_tr_holds_ s1_._(dl._dn)_=_s2_._(dl._dn) set ml = max_Data-Loc_in tl; set mr = max_Data-Loc_in tr; let dn be Element of NAT ; ::_thesis: ( dn <= max_Data-Loc_in tr implies s1 . (dl. dn) = s2 . (dl. dn) ) A6: max_Data-Loc_in tr <= max ((max_Data-Loc_in tl),(max_Data-Loc_in tr)) by XXREAL_0:25; assume dn <= max_Data-Loc_in tr ; ::_thesis: s1 . (dl. dn) = s2 . (dl. dn) then dn <= max ((max_Data-Loc_in tl),(max_Data-Loc_in tr)) 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; ::_thesis: verum end; then A7: tr @ s1 = tr @ s2 by A2; (nt -tree (tl,tr)) @ s1 = nt -Meaning_on ((tl @ s1),(tr @ s1)) by Th5; hence (nt -tree (tl,tr)) @ s1 = (nt -tree (tl,tr)) @ s2 by A5, A7, Th5; ::_thesis: verum end; end; theorem Th11: :: SCM_COMP:11 for term being bin-term for 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 proofend; defpred S2[ bin-term] means for F being Instruction-Sequence of SCM for aux, n being Element of NAT st Shift ((SCM-Compile ($1,aux)),n) c= F holds for s being b3 -started State of SCM 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 Th12: :: SCM_COMP:12 for F being Instruction-Sequence of SCM for term being bin-term for aux, n being Element of NAT st Shift ((SCM-Compile (term,aux)),n) c= F holds for s being b4 -started State of SCM 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) ) ) proofend; theorem :: SCM_COMP:13 for F being Instruction-Sequence of SCM for term being bin-term for aux, n being Element of NAT st Shift (((SCM-Compile (term,aux)) ^ <%(halt SCM)%>),n) c= F holds for s being b4 -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)) ) proofend;