scm_comp.miz



    begin

    

     Lm1: 1 = { n where n be Nat : n < 1 } by AXIOMS: 4;

    

     Lm2: 5 = { n where n be Nat : n < 5 } by AXIOMS: 4;

    definition

      :: SCM_COMP:def1

      func SCM-AE -> binary with_terminals with_nonterminals with_useful_nonterminals strict non empty DTConstrStr means

      : Def1: ( Terminals it ) = SCM-Data-Loc & ( NonTerminals it ) = [:1, 5:] & for x,y,z be Symbol of it holds x ==> <*y, z*> iff x in [:1, 5:];

      existence

      proof

        defpred X[ set, set, set] means $1 in [:1, 5:];

        consider G be binary strict non empty DTConstrStr such that

         A1: the carrier of G = ( SCM-Data-Loc \/ [:1, 5:]) and

         A2: for x,y,z be Symbol of G holds x ==> <*y, z*> iff X[x, y, z] from BINTREE1:sch 1;

        

         A3: ( NonTerminals G) = { t where t be Symbol of G : ex tnt be FinSequence st t ==> tnt } by LANG1:def 3;

        

         A4: ( NonTerminals G) = [:1, 5:]

        proof

          thus ( NonTerminals G) c= [:1, 5:]

          proof

            let x be object;

            assume x in ( NonTerminals G);

            then

            consider t be Symbol of G such that

             A5: x = t and

             A6: ex tnt be FinSequence st t ==> tnt by A3;

            consider tnt be FinSequence such that

             A7: t ==> tnt by A6;

            ex x1,x2 be Symbol of G st tnt = <*x1, x2*> by A7, BINTREE1:def 4;

            hence thesis by A2, A5, A7;

          end;

          let x be object;

          assume

           A8: x in [:1, 5:];

          then

          reconsider t = x as Symbol of G by A1, XBOOLE_0:def 3;

          t ==> <*t, t*> by A2, A8;

          hence thesis by A3;

        end;

        then

         A9: G is with_nonterminals by DTCONSTR:def 4;

        

         A10: ( Terminals G) = { t where t be Symbol of G : not ex tnt be FinSequence st t ==> tnt } by LANG1:def 2;

        

         A11: ( Terminals G) = SCM-Data-Loc

        proof

          thus ( Terminals G) c= SCM-Data-Loc

          proof

            let x be object;

            assume x in ( Terminals G);

            then

            consider t be Symbol of G such that

             A12: x = t and

             A13: not ex tnt be FinSequence st t ==> tnt by A10;

            assume not x in SCM-Data-Loc ;

            then t in [:1, 5:] by A1, A12, XBOOLE_0:def 3;

            then t ==> <*t, t*> by A2;

            hence contradiction by A13;

          end;

          let x be object;

          assume

           A14: x in SCM-Data-Loc ;

          then

           A15: ex y,z be object st y in {1} & z in NAT & x = [y, z] by ZFMISC_1: 84;

          reconsider t = x as Symbol of G by A1, A14, XBOOLE_0:def 3;

          assume not x in ( Terminals G);

          then

          consider tnt be FinSequence such that

           A16: t ==> tnt by A10;

          ex x1,x2 be Symbol of G st tnt = <*x1, x2*> by A16, BINTREE1:def 4;

          then x in [:1, 5:] by A2, A16;

          then

          consider x1,x2 be object such that

           A17: x1 in 1 and x2 in 5 and

           A18: x = [x1, x2] by ZFMISC_1: 84;

          x = [ 0 , x2] by A17, A18, CARD_1: 49, TARSKI:def 1;

          hence contradiction by A15, XTUPLE_0: 1;

        end;

        now

          

           A19: ( dl. 1) in SCM-Data-Loc by AMI_2:def 16;

          

           A20: ( dl. 0 ) in SCM-Data-Loc by AMI_2:def 16;

          then

          reconsider d0 = ( dl. 0 ), d1 = ( dl. 1) as Symbol of G by A1, A19, XBOOLE_0:def 3;

          

           A21: ( root-tree d1) in ( TS G) by A11, A19, DTCONSTR:def 1;

          ( root-tree d0) in ( TS G) by A11, A20, DTCONSTR:def 1;

          then

          reconsider p = <*( root-tree d0), ( root-tree d1)*> as FinSequence of ( TS G) by A21, FINSEQ_2: 13;

          let nt be Symbol of G;

          assume

           A22: nt in ( NonTerminals G);

          take p;

          ( roots p) = <*(( root-tree d0) . {} ), (( root-tree d1) . {} )*> by DTCONSTR: 6

          .= <*(( root-tree d0) . {} ), d1*> by TREES_4: 3

          .= <*d0, d1*> by TREES_4: 3;

          hence nt ==> ( roots p) by A2, A4, A22;

        end;

        then

         A23: G is with_useful_nonterminals by DTCONSTR:def 5;

        G is with_terminals by A11, DTCONSTR:def 3;

        hence thesis by A2, A11, A4, A9, A23;

      end;

      uniqueness

      proof

        let S1,S2 be binary with_terminals with_nonterminals with_useful_nonterminals strict non empty DTConstrStr;

        assume that

         A24: ( Terminals S1) = SCM-Data-Loc & ( NonTerminals S1) = [:1, 5:] and

         A25: for x,y,z be Symbol of S1 holds x ==> <*y, z*> iff x in [:1, 5:];

        assume that

         A26: ( Terminals S2) = SCM-Data-Loc & ( NonTerminals S2) = [:1, 5:] and

         A27: for x,y,z be Symbol of S2 holds x ==> <*y, z*> iff x in [:1, 5:];

        

         A28: the carrier of S1 = (( Terminals S1) \/ ( NonTerminals S1)) by LANG1: 1

        .= the carrier of S2 by A24, A26, LANG1: 1;

        the Rules of S1 = the Rules of S2

        proof

          set p1 = the Rules of S1, p2 = the Rules of S2;

          let a,b be object;

          hereby

            assume

             A29: [a, b] in p1;

            then

            reconsider l = a as Symbol of S1 by ZFMISC_1: 87;

            reconsider r = b as Element of (the carrier of S1 * ) by A29, ZFMISC_1: 87;

            

             A30: l ==> r by A29, LANG1:def 1;

            then

            consider x1,x2 be Symbol of S1 such that

             A31: r = <*x1, x2*> by BINTREE1:def 4;

            reconsider l, x1, x2 as Symbol of S2 by A28;

            l in [:1, 5:] by A25, A30, A31;

            then l ==> <*x1, x2*> by A27;

            hence [a, b] in p2 by A31, LANG1:def 1;

          end;

          assume

           A32: [a, b] in p2;

          then

          reconsider l = a as Symbol of S2 by ZFMISC_1: 87;

          reconsider r = b as Element of (the carrier of S2 * ) by A32, ZFMISC_1: 87;

          

           A33: l ==> r by A32, LANG1:def 1;

          then

          consider x1,x2 be Symbol of S2 such that

           A34: r = <*x1, x2*> by BINTREE1:def 4;

          reconsider l, x1, x2 as Symbol of S1 by A28;

          l in [:1, 5:] by A27, A33, A34;

          then l ==> <*x1, x2*> by A25;

          hence thesis by A34, LANG1:def 1;

        end;

        hence thesis by A28;

      end;

    end

    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

      proof

        nt ==> <*( root-label tl), ( root-label tr)*> by Def1, Lm3;

        then nt ==> ( roots <*tl, tr*>) by BINTREE1: 2;

        then (nt -tree <*tl, tr*>) in ( TS SCM-AE ) by DTCONSTR:def 1;

        hence thesis by TREES_4:def 6;

      end;

    end

    definition

      let t be Terminal of SCM-AE ;

      :: original: root-tree

      redefine

      func root-tree t -> bin-term ;

      coherence by DTCONSTR:def 1;

    end

    definition

      let t be Terminal of SCM-AE ;

      :: SCM_COMP:def2

      func @ t -> Data-Location equals t;

      coherence

      proof

        reconsider t as Element of SCM-Data-Loc by Def1;

        t in ( Data-Locations SCM ) by AMI_3: 27;

        then

        reconsider t as Object of SCM ;

        t is Data-Location by AMI_2:def 16;

        hence thesis;

      end;

    end

    theorem :: SCM_COMP:1

    

     Th1: for nt be NonTerminal of SCM-AE holds nt = [ 0 , 0 ] or ... or nt = [ 0 , 4]

    proof

      let nt be NonTerminal of SCM-AE ;

      consider x,y be object such that

       A1: x in 1 and

       A2: y in 5 and

       A3: nt = [x, y] by Lm3, ZFMISC_1: 84;

      

       A4: x = 0 by A1, CARD_1: 49, TARSKI:def 1;

      consider n be Nat such that

       A5: y = n and

       A6: n < 5 by A2, Lm2;

      5 = (4 + 1);

      then n <= 4 by A6, NAT_1: 13;

      then n = 0 or ... or n = 4;

      hence thesis by A3, A4, A5;

    end;

    theorem :: SCM_COMP:2

     [ 0 , 0 ] is NonTerminal of SCM-AE & ... & [ 0 , 4] is NonTerminal of SCM-AE

    proof

      

       A1: 3 in 5 & 4 in 5 by Lm2;

      

       A2: 1 in 5 & 2 in 5 by Lm2;

       0 in 1 & 0 in 5 by Lm1, Lm2;

      hence thesis by A2, A1, Lm3, ZFMISC_1: 87;

    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;

      :: SCM_COMP:def3

      func t1 + t2 -> bin-term equals ( [ 0 , 0 ] -tree (t1,t2));

      coherence

      proof

        (nt0 -tree (t1,t2)) in ( TS SCM-AE );

        hence thesis;

      end;

      :: SCM_COMP:def4

      func t1 - t2 -> bin-term equals ( [ 0 , 1] -tree (t1,t2));

      coherence

      proof

        (nt1 -tree (t1,t2)) in ( TS SCM-AE );

        hence thesis;

      end;

      :: SCM_COMP:def5

      func t1 * t2 -> bin-term equals ( [ 0 , 2] -tree (t1,t2));

      coherence

      proof

        (nt2 -tree (t1,t2)) in ( TS SCM-AE );

        hence thesis;

      end;

      :: SCM_COMP:def6

      func t1 div t2 -> bin-term equals ( [ 0 , 3] -tree (t1,t2));

      coherence

      proof

        (nt3 -tree (t1,t2)) in ( TS SCM-AE );

        hence thesis;

      end;

      :: SCM_COMP:def7

      func t1 mod t2 -> bin-term equals ( [ 0 , 4] -tree (t1,t2));

      coherence

      proof

        (nt4 -tree (t1,t2)) in ( TS SCM-AE );

        hence thesis;

      end;

    end

    theorem :: SCM_COMP:3

    for term be bin-term holds (ex t be Terminal of SCM-AE st term = ( root-tree t)) or ex tl,tr be 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

      let term be bin-term;

      ( root-label term) in the carrier of SCM-AE ;

      then (term . {} ) in the carrier of SCM-AE by BINTREE1:def 1;

      then

       A1: (term . {} ) in (( Terminals SCM-AE ) \/ ( NonTerminals SCM-AE )) by LANG1: 1;

      per cases by A1, XBOOLE_0:def 3;

        suppose (term . {} ) in ( Terminals SCM-AE );

        then

        reconsider t = (term . {} ) as Terminal of SCM-AE ;

        term = ( root-tree t) by DTCONSTR: 9;

        hence thesis;

      end;

        suppose (term . {} ) in ( NonTerminals SCM-AE );

        then

        reconsider nt = (term . {} ) as NonTerminal of SCM-AE ;

        consider ts be FinSequence of ( TS SCM-AE ) such that

         A2: term = (nt -tree ts) and

         A3: nt ==> ( roots ts) by DTCONSTR: 10;

        ex x1,x2 be Symbol of SCM-AE st ( roots ts) = <*x1, x2*> by A3, BINTREE1:def 4;

        then ( len ( roots ts)) = 2 by FINSEQ_1: 44;

        then

         A4: ( dom ( roots ts)) = ( dom ts) & ( dom ( roots ts)) = ( Seg 2) by FINSEQ_1:def 3, TREES_3:def 18;

        

         A5: 2 in ( Seg 2) by FINSEQ_1: 2, TARSKI:def 2;

        then

        consider tr be DecoratedTree such that

         A6: tr = (ts . 2) and (( roots ts) . 2) = (tr . {} ) by A4, TREES_3:def 18;

        

         A7: 1 in ( Seg 2) by FINSEQ_1: 2, TARSKI:def 2;

        then

        consider tl be DecoratedTree such that

         A8: tl = (ts . 1) and (( roots ts) . 1) = (tl . {} ) by A4, TREES_3:def 18;

        reconsider tl, tr as bin-term by A4, A7, A5, A8, A6, FINSEQ_2: 11;

        

         A9: nt = [ 0 , 0 ] or ... or nt = [ 0 , 4] by Th1;

        ( len ts) = 2 by A4, FINSEQ_1:def 3;

        then ts = <*tl, tr*> by A8, A6, FINSEQ_1: 44;

        then term = (nt -tree (tl,tr)) by A2, TREES_4:def 6;

        then term = (tl + tr) or term = (tl - tr) or term = (tl * tr) or term = (tl div tr) or term = (tl mod tr) by A9;

        hence thesis;

      end;

    end;

    definition

      let o be NonTerminal of SCM-AE , i,j be Integer;

      :: SCM_COMP:def8

      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 ;

      consistency

      proof

        ( [ 0 , 0 ] `2 ) = 0 & ( [ 0 , 1] `2 ) = 1 & ( [ 0 , 2] `2 ) = 2 & ( [ 0 , 3] `2 ) = 3 & ( [ 0 , 4] `2 ) = 4;

        hence thesis;

      end;

    end

    registration

      let s be State of SCM ;

      let t be Terminal of SCM-AE ;

      cluster (s . t) -> integer;

      coherence

      proof

        (s . ( @ t)) = (s . t);

        hence thesis;

      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

      proof

        reconsider x as Element of INT by INT_1:def 2;

        (f . x) is Element of D;

        hence thesis;

      end;

    end

    set i2i = ( id INT );

    deffunc U( NonTerminal of SCM-AE , set, set, Integer, Integer) = (i2i . ($1 -Meaning_on ($4,$5)));

    definition

      let s be State of SCM ;

      let term be bin-term;

      :: SCM_COMP:def9

      func term @ s -> Integer means

      : Def9: ex f be Function of ( TS SCM-AE ), INT st it = (f . term) & (for t be Terminal of SCM-AE holds (f . ( root-tree t)) = (s . t)) & for nt be NonTerminal of SCM-AE , tl,tr be bin-term, rtl,rtr be Symbol of SCM-AE st rtl = ( root-label tl) & rtr = ( root-label tr) & nt ==> <*rtl, rtr*> holds for xl,xr be Element of INT st xl = (f . tl) & xr = (f . tr) holds (f . (nt -tree (tl,tr))) = (nt -Meaning_on (xl,xr));

      existence

      proof

        deffunc V( Terminal of SCM-AE ) = (i2i . (s . $1));

        consider f be Function of ( TS SCM-AE ), INT such that

         A1: (for t be Terminal of SCM-AE holds (f . ( root-tree t)) = V(t)) & for nt be NonTerminal of SCM-AE , tl,tr be bin-term, rtl,rtr be Symbol of SCM-AE st rtl = ( root-label tl) & rtr = ( root-label tr) & nt ==> <*rtl, rtr*> holds for xl,xr be Element of INT st xl = (f . tl) & xr = (f . tr) holds (f . (nt -tree (tl,tr))) = U(nt,rtl,rtr,xl,xr) from BINTREE1:sch 3;

        reconsider IT = (f . term) as Element of INT ;

        take IT, f;

        thus IT = (f . term);

        hereby

          let t be Terminal of SCM-AE ;

          (s . t) in INT by INT_1:def 2;

          then (i2i . (s . t)) = (s . t) by FUNCT_1: 18;

          hence (f . ( root-tree t)) = (s . t) by A1;

        end;

        let nt be NonTerminal of SCM-AE , tl,tr be bin-term, rtl,rtr be Symbol of SCM-AE ;

        assume

         A2: rtl = ( root-label tl) & rtr = ( root-label tr) & nt ==> <*rtl, rtr*>;

        let xl,xr be Element of INT ;

        (nt -Meaning_on (xl,xr)) in INT by INT_1:def 2;

        then (i2i . (nt -Meaning_on (xl,xr))) = (nt -Meaning_on (xl,xr)) by FUNCT_1: 18;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        deffunc V( Terminal of SCM-AE ) = (i2i . (s . $1));

        let it1,it2 be Integer;

        given f1 be Function of ( TS SCM-AE ), INT such that

         A3: it1 = (f1 . term) and

         A4: for t be Terminal of SCM-AE holds (f1 . ( root-tree t)) = (s . t) and

         A5: for nt be NonTerminal of SCM-AE , tl,tr be bin-term, rtl,rtr be Symbol of SCM-AE st rtl = ( root-label tl) & rtr = ( root-label tr) & nt ==> <*rtl, rtr*> holds for xl,xr be Element of INT st xl = (f1 . tl) & xr = (f1 . tr) holds (f1 . (nt -tree (tl,tr))) = (nt -Meaning_on (xl,xr));

         A6:

        now

          hereby

            let t be Terminal of SCM-AE ;

            (s . t) in INT by INT_1:def 2;

            then (i2i . (s . t)) = (s . t) by FUNCT_1: 18;

            hence (f1 . ( root-tree t)) = V(t) by A4;

          end;

          let nt be NonTerminal of SCM-AE , tl,tr be bin-term, rtl,rtr be Symbol of SCM-AE such that

           A7: rtl = ( root-label tl) & rtr = ( root-label tr) & nt ==> <*rtl, rtr*>;

          let xl,xr be Element of INT such that

           A8: xl = (f1 . tl) & xr = (f1 . tr);

          (nt -Meaning_on (xl,xr)) in INT by INT_1:def 2;

          then (i2i . (nt -Meaning_on (xl,xr))) = (nt -Meaning_on (xl,xr)) by FUNCT_1: 18;

          hence (f1 . (nt -tree (tl,tr))) = U(nt,rtl,rtr,xl,xr) by A5, A7, A8;

        end;

        given f2 be Function of ( TS SCM-AE ), INT such that

         A9: it2 = (f2 . term) and

         A10: for t be Terminal of SCM-AE holds (f2 . ( root-tree t)) = (s . t) and

         A11: for nt be NonTerminal of SCM-AE , tl,tr be bin-term, rtl,rtr be Symbol of SCM-AE st rtl = ( root-label tl) & rtr = ( root-label tr) & nt ==> <*rtl, rtr*> holds for xl,xr be Element of INT st xl = (f2 . tl) & xr = (f2 . tr) holds (f2 . (nt -tree (tl,tr))) = (nt -Meaning_on (xl,xr));

         A12:

        now

          hereby

            let t be Terminal of SCM-AE ;

            (s . t) in INT by INT_1:def 2;

            then (i2i . (s . t)) = (s . t) by FUNCT_1: 18;

            hence (f2 . ( root-tree t)) = V(t) by A10;

          end;

          let nt be NonTerminal of SCM-AE , tl,tr be bin-term, rtl,rtr be Symbol of SCM-AE such that

           A13: rtl = ( root-label tl) & rtr = ( root-label tr) & nt ==> <*rtl, rtr*>;

          let xl,xr be Element of INT such that

           A14: xl = (f2 . tl) & xr = (f2 . tr);

          (nt -Meaning_on (xl,xr)) in INT by INT_1:def 2;

          then (i2i . (nt -Meaning_on (xl,xr))) = (nt -Meaning_on (xl,xr)) by FUNCT_1: 18;

          hence (f2 . (nt -tree (tl,tr))) = U(nt,rtl,rtr,xl,xr) by A11, A13, A14;

        end;

        f1 = f2 from BINTREE1:sch 4( A6, A12);

        hence thesis by A3, A9;

      end;

    end

    theorem :: SCM_COMP:4

    

     Th4: for s be State of SCM , t be Terminal of SCM-AE holds (( root-tree t) @ s) = (s . t)

    proof

      let s be State of SCM , t be Terminal of SCM-AE ;

      ex f be Function of ( TS SCM-AE ), INT st (( root-tree t) @ s) = (f . ( root-tree t)) & (for t be Terminal of SCM-AE holds (f . ( root-tree t)) = (s . t)) & for nt be NonTerminal of SCM-AE , tl,tr be bin-term, rtl,rtr be Symbol of SCM-AE st rtl = ( root-label tl) & rtr = ( root-label tr) & nt ==> <*rtl, rtr*> holds for xl,xr be Element of INT st xl = (f . tl) & xr = (f . tr) holds (f . (nt -tree (tl,tr))) = (nt -Meaning_on (xl,xr)) by Def9;

      hence thesis;

    end;

    theorem :: SCM_COMP:5

    

     Th5: for s be State of SCM , nt be NonTerminal of SCM-AE , tl,tr be bin-term holds ((nt -tree (tl,tr)) @ s) = (nt -Meaning_on ((tl @ s),(tr @ s)))

    proof

      let s be State of SCM , nt be NonTerminal of SCM-AE , tl,tr be bin-term;

      consider f be Function of ( TS SCM-AE ), INT such that

       A1: ((nt -tree (tl,tr)) @ s) = (f . (nt -tree (tl,tr))) and

       A2: for t be Terminal of SCM-AE holds (f . ( root-tree t)) = (s . t) and

       A3: for nt be NonTerminal of SCM-AE , tl,tr be bin-term, rtl,rtr be Symbol of SCM-AE st rtl = ( root-label tl) & rtr = ( root-label tr) & nt ==> <*rtl, rtr*> holds for xl,xr be Element of INT st xl = (f . tl) & xr = (f . tr) holds (f . (nt -tree (tl,tr))) = (nt -Meaning_on (xl,xr)) by Def9;

      

       A4: nt ==> <*( root-label tl), ( root-label tr)*> by Def1, Lm3;

      (tl @ s) = (f . tl) & (tr @ s) = (f . tr) by A2, A3, Def9;

      hence thesis by A1, A3, A4;

    end;

    theorem :: SCM_COMP:6

    for s be State of SCM , tl,tr be 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

      let s be State of SCM , tl,tr be bin-term;

      

      thus ((tl + tr) @ s) = (nt0 -Meaning_on ((tl @ s),(tr @ s))) by Th5

      .= ((tl @ s) + (tr @ s)) by Def8;

      

      thus ((tl - tr) @ s) = (nt1 -Meaning_on ((tl @ s),(tr @ s))) by Th5

      .= ((tl @ s) - (tr @ s)) by Def8;

      

      thus ((tl * tr) @ s) = (nt2 -Meaning_on ((tl @ s),(tr @ s))) by Th5

      .= ((tl @ s) * (tr @ s)) by Def8;

      

      thus ((tl div tr) @ s) = (nt3 -Meaning_on ((tl @ s),(tr @ s))) by Th5

      .= ((tl @ s) div (tr @ s)) by Def8;

      

      thus ((tl mod tr) @ s) = (nt4 -Meaning_on ((tl @ s),(tr @ s))) by Th5

      .= ((tl @ s) mod (tr @ s)) by Def8;

    end;

    definition

      let nt be NonTerminal of SCM-AE , n be Nat;

      :: SCM_COMP:def10

      func Selfwork (nt,n) -> XFinSequence of the InstructionsF 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 ;

      consistency

      proof

        ( [ 0 , 0 ] `2 ) = 0 & ( [ 0 , 1] `2 ) = 1 & ( [ 0 , 2] `2 ) = 2 & ( [ 0 , 3] `2 ) = 3 & ( [ 0 , 4] `2 ) = 4;

        hence thesis;

      end;

    end

    definition

      deffunc V( NonTerminal of SCM-AE , sequence of (the InstructionsF of SCM ^omega ), sequence of (the InstructionsF of SCM ^omega ), Nat) = ((($2 . ( In ($4, NAT ))) ^ ($3 . ( In (($4 + 1), NAT )))) ^ ( Down ( Selfwork ($1,$4))));

      deffunc U( Terminal of SCM-AE , Nat) = ( Down <%(( dl. $2) := ( @ $1))%>);

      :: SCM_COMP:def11

      func SCM-Compile -> Function of ( TS SCM-AE ), ( Funcs ( NAT ,(the InstructionsF of SCM ^omega ))) means

      : Def11: (for t be Terminal of SCM-AE holds ex g be sequence of (the InstructionsF of SCM ^omega ) st g = (it . ( root-tree t)) & for n be Nat holds (g . n) = <%(( dl. n) := ( @ t))%>) & for nt be NonTerminal of SCM-AE , t1,t2 be bin-term, rtl,rtr be Symbol of SCM-AE st rtl = ( root-label t1) & rtr = ( root-label t2) & nt ==> <*rtl, rtr*> holds ex g,f1,f2 be sequence of (the InstructionsF of SCM ^omega ) st g = (it . (nt -tree (t1,t2))) & f1 = (it . t1) & f2 = (it . t2) & for n be Nat holds (g . n) = (((f1 . ( In (n, NAT ))) ^ (f2 . ( In ((n + 1), NAT )))) ^ ( Selfwork (nt,n)));

      existence

      proof

        consider f be Function of ( TS SCM-AE ), ( Funcs ( NAT ,(the InstructionsF of SCM ^omega ))) such that

         A1: (for t be Terminal of SCM-AE holds ex g be sequence of (the InstructionsF of SCM ^omega ) st g = (f . ( root-tree t)) & for n be Element of NAT holds (g . n) = U(t,n)) & for nt be NonTerminal of SCM-AE , t1,t2 be bin-term, rtl,rtr be Symbol of SCM-AE st rtl = ( root-label t1) & rtr = ( root-label t2) & nt ==> <*rtl, rtr*> holds ex g,f1,f2 be sequence of (the InstructionsF of SCM ^omega ) st g = (f . (nt -tree (t1,t2))) & f1 = (f . t1) & f2 = (f . t2) & for n be Element of NAT holds (g . n) = V(nt,f1,f2,n) from BINTREE1:sch 5;

        take f;

        (for t be Terminal of SCM-AE holds ex g be sequence of (the InstructionsF of SCM ^omega ) st g = (f . ( root-tree t)) & for n be Nat holds (g . n) = <%(( dl. n) := ( @ t))%>) & for nt be NonTerminal of SCM-AE , t1,t2 be bin-term, rtl,rtr be Symbol of SCM-AE st rtl = ( root-label t1) & rtr = ( root-label t2) & nt ==> <*rtl, rtr*> holds ex g,f1,f2 be sequence of (the InstructionsF of SCM ^omega ) st g = (f . (nt -tree (t1,t2))) & f1 = (f . t1) & f2 = (f . t2) & for n be Nat holds (g . n) = (((f1 . ( In (n, NAT ))) ^ (f2 . ( In ((n + 1), NAT )))) ^ ( Selfwork (nt,n)))

        proof

          thus for t be Terminal of SCM-AE holds ex g be sequence of (the InstructionsF of SCM ^omega ) st g = (f . ( root-tree t)) & for n be Nat holds (g . n) = <%(( dl. n) := ( @ t))%>

          proof

            let t be Terminal of SCM-AE ;

            consider g be sequence of (the InstructionsF of SCM ^omega ) such that

             A2: g = (f . ( root-tree t)) and

             A3: for n be Element of NAT holds (g . n) = U(t,n) by A1;

            take g;

            thus g = (f . ( root-tree t)) by A2;

            let n be Nat;

            n in NAT by ORDINAL1:def 12;

            then (g . n) = U(t,n) by A3;

            hence thesis;

          end;

          thus for nt be NonTerminal of SCM-AE , t1,t2 be bin-term, rtl,rtr be Symbol of SCM-AE st rtl = ( root-label t1) & rtr = ( root-label t2) & nt ==> <*rtl, rtr*> holds ex g,f1,f2 be sequence of (the InstructionsF of SCM ^omega ) st g = (f . (nt -tree (t1,t2))) & f1 = (f . t1) & f2 = (f . t2) & for n be Nat holds (g . n) = (((f1 . ( In (n, NAT ))) ^ (f2 . ( In ((n + 1), NAT )))) ^ ( Selfwork (nt,n)))

          proof

            let nt be NonTerminal of SCM-AE , t1,t2 be bin-term, rtl,rtr be Symbol of SCM-AE such that

             A4: rtl = ( root-label t1) & rtr = ( root-label t2) & nt ==> <*rtl, rtr*>;

            consider g,f1,f2 be sequence of (the InstructionsF of SCM ^omega ) such that

             A5: g = (f . (nt -tree (t1,t2))) & f1 = (f . t1) & f2 = (f . t2) and

             A6: for n be Element of NAT holds (g . n) = V(nt,f1,f2,n) by A4, A1;

            take g, f1, f2;

            thus g = (f . (nt -tree (t1,t2))) & f1 = (f . t1) & f2 = (f . t2) by A5;

            let n be Nat;

            (g . n) = V(nt,f1,f2,n) by A6;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be Function of ( TS SCM-AE ), ( Funcs ( NAT ,(the InstructionsF of SCM ^omega ))) such that

         A7: (for t be Terminal of SCM-AE holds ex g be sequence of (the InstructionsF of SCM ^omega ) st g = (f1 . ( root-tree t)) & for n be Nat holds (g . n) = <%(( dl. n) := ( @ t))%>) & for nt be NonTerminal of SCM-AE , t1,t2 be bin-term, rtl,rtr be Symbol of SCM-AE st rtl = ( root-label t1) & rtr = ( root-label t2) & nt ==> <*rtl, rtr*> holds ex g,g1,g2 be sequence of (the InstructionsF of SCM ^omega ) st g = (f1 . (nt -tree (t1,t2))) & g1 = (f1 . t1) & g2 = (f1 . t2) & for n be Nat holds (g . n) = (((g1 . ( In (n, NAT ))) ^ (g2 . ( In ((n + 1), NAT )))) ^ ( Selfwork (nt,n))) and

         A8: (for t be Terminal of SCM-AE holds ex g be sequence of (the InstructionsF of SCM ^omega ) st g = (f2 . ( root-tree t)) & for n be Nat holds (g . n) = <%(( dl. n) := ( @ t))%>) & for nt be NonTerminal of SCM-AE , t1,t2 be bin-term, rtl,rtr be Symbol of SCM-AE st rtl = ( root-label t1) & rtr = ( root-label t2) & nt ==> <*rtl, rtr*> holds ex g,g1,g2 be sequence of (the InstructionsF of SCM ^omega ) st g = (f2 . (nt -tree (t1,t2))) & g1 = (f2 . t1) & g2 = (f2 . t2) & for n be Nat holds (g . n) = (((g1 . ( In (n, NAT ))) ^ (g2 . ( In ((n + 1), NAT )))) ^ ( Selfwork (nt,n)));

        

         A9: (for t be Terminal of SCM-AE holds ex g be sequence of (the InstructionsF of SCM ^omega ) st g = (f1 . ( root-tree t)) & for n be Element of NAT holds (g . n) = U(t,n)) & for nt be NonTerminal of SCM-AE , t1,t2 be bin-term, rtl,rtr be Symbol of SCM-AE st rtl = ( root-label t1) & rtr = ( root-label t2) & nt ==> <*rtl, rtr*> holds ex g,g1,g2 be sequence of (the InstructionsF of SCM ^omega ) st g = (f1 . (nt -tree (t1,t2))) & g1 = (f1 . t1) & g2 = (f1 . t2) & for n be Element of NAT holds (g . n) = V(nt,g1,g2,n)

        proof

          thus for t be Terminal of SCM-AE holds ex g be sequence of (the InstructionsF of SCM ^omega ) st g = (f1 . ( root-tree t)) & for n be Element of NAT holds (g . n) = U(t,n)

          proof

            let t be Terminal of SCM-AE ;

            consider g be sequence of (the InstructionsF of SCM ^omega ) such that

             A10: g = (f1 . ( root-tree t)) & for n be Nat holds (g . n) = <%(( dl. n) := ( @ t))%> by A7;

            take g;

            thus thesis by A10;

          end;

          thus for nt be NonTerminal of SCM-AE , t1,t2 be bin-term, rtl,rtr be Symbol of SCM-AE st rtl = ( root-label t1) & rtr = ( root-label t2) & nt ==> <*rtl, rtr*> holds ex g,g1,g2 be sequence of (the InstructionsF of SCM ^omega ) st g = (f1 . (nt -tree (t1,t2))) & g1 = (f1 . t1) & g2 = (f1 . t2) & for n be Element of NAT holds (g . n) = V(nt,g1,g2,n)

          proof

            let nt be NonTerminal of SCM-AE , t1,t2 be bin-term, rtl,rtr be Symbol of SCM-AE such that

             A11: rtl = ( root-label t1) & rtr = ( root-label t2) & nt ==> <*rtl, rtr*>;

            consider g,g1,g2 be sequence of (the InstructionsF of SCM ^omega ) such that

             A12: g = (f1 . (nt -tree (t1,t2))) & g1 = (f1 . t1) & g2 = (f1 . t2) & for n be Nat holds (g . n) = (((g1 . ( In (n, NAT ))) ^ (g2 . ( In ((n + 1), NAT )))) ^ ( Selfwork (nt,n))) by A7, A11;

            take g, g1, g2;

            thus thesis by A12;

          end;

        end;

        

         A13: (for t be Terminal of SCM-AE holds ex g be sequence of (the InstructionsF of SCM ^omega ) st g = (f2 . ( root-tree t)) & for n be Element of NAT holds (g . n) = U(t,n)) & for nt be NonTerminal of SCM-AE , t1,t2 be bin-term, rtl,rtr be Symbol of SCM-AE st rtl = ( root-label t1) & rtr = ( root-label t2) & nt ==> <*rtl, rtr*> holds ex g,g1,g2 be sequence of (the InstructionsF of SCM ^omega ) st g = (f2 . (nt -tree (t1,t2))) & g1 = (f2 . t1) & g2 = (f2 . t2) & for n be Element of NAT holds (g . n) = V(nt,g1,g2,n)

        proof

          thus for t be Terminal of SCM-AE holds ex g be sequence of (the InstructionsF of SCM ^omega ) st g = (f2 . ( root-tree t)) & for n be Element of NAT holds (g . n) = U(t,n)

          proof

            let t be Terminal of SCM-AE ;

            consider g be sequence of (the InstructionsF of SCM ^omega ) such that

             A14: g = (f2 . ( root-tree t)) & for n be Nat holds (g . n) = <%(( dl. n) := ( @ t))%> by A8;

            take g;

            thus thesis by A14;

          end;

          thus for nt be NonTerminal of SCM-AE , t1,t2 be bin-term, rtl,rtr be Symbol of SCM-AE st rtl = ( root-label t1) & rtr = ( root-label t2) & nt ==> <*rtl, rtr*> holds ex g,g1,g2 be sequence of (the InstructionsF of SCM ^omega ) st g = (f2 . (nt -tree (t1,t2))) & g1 = (f2 . t1) & g2 = (f2 . t2) & for n be Element of NAT holds (g . n) = V(nt,g1,g2,n)

          proof

            let nt be NonTerminal of SCM-AE , t1,t2 be bin-term, rtl,rtr be Symbol of SCM-AE such that

             A15: rtl = ( root-label t1) & rtr = ( root-label t2) & nt ==> <*rtl, rtr*>;

            consider g,g1,g2 be sequence of (the InstructionsF of SCM ^omega ) such that

             A16: g = (f2 . (nt -tree (t1,t2))) & g1 = (f2 . t1) & g2 = (f2 . t2) & for n be Nat holds (g . n) = (((g1 . ( In (n, NAT ))) ^ (g2 . ( In ((n + 1), NAT )))) ^ ( Selfwork (nt,n))) by A8, A15;

            take g, g1, g2;

            thus thesis by A16;

          end;

        end;

        thus f1 = f2 from BINTREE1:sch 6( A9, A13);

      end;

    end

    definition

      let term be bin-term, aux be Nat;

      :: SCM_COMP:def12

      func SCM-Compile (term,aux) -> XFinSequence of the InstructionsF of SCM equals (( SCM-Compile . term) . aux);

      coherence

      proof

        reconsider f = ( SCM-Compile . term) as sequence of (the InstructionsF of SCM ^omega ) by FUNCT_2: 66;

        (f . ( In (aux, NAT ))) in (the InstructionsF of SCM ^omega );

        hence thesis by AFINSQ_1:def 7;

      end;

    end

    theorem :: SCM_COMP:7

    

     Th7: for t be Terminal of SCM-AE , n be Element of NAT holds ( SCM-Compile (( root-tree t),n)) = <%(( dl. n) := ( @ t))%>

    proof

      let t be Terminal of SCM-AE , n be Element of NAT ;

      consider g be sequence of (the InstructionsF of SCM ^omega ) such that

       A1: g = ( SCM-Compile . ( root-tree t)) and

       A2: for n be Nat holds (g . n) = <%(( dl. n) := ( @ t))%> by Def11;

      thus thesis by A1, A2;

    end;

    theorem :: SCM_COMP:8

    

     Th8: for nt be NonTerminal of SCM-AE , t1,t2 be bin-term, n be Element of NAT , rtl,rtr be 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

      let nt be NonTerminal of SCM-AE , t1,t2 be bin-term, n be Element of NAT , rtl,rtr be Symbol of SCM-AE ;

      assume

       A1: rtl = ( root-label t1) & rtr = ( root-label t2) & nt ==> <*rtl, rtr*>;

      consider g,f1,f2 be sequence of (the InstructionsF of SCM ^omega ) such that

       A2: g = ( SCM-Compile . (nt -tree (t1,t2))) and

       A3: f1 = ( SCM-Compile . t1) and

       A4: f2 = ( SCM-Compile . t2) and

       A5: for n be Nat holds (g . n) = (((f1 . ( In (n, NAT ))) ^ (f2 . ( In ((n + 1), NAT )))) ^ ( Selfwork (nt,n))) by A1, Def11;

      (g . n) = (((f1 . ( In (n, NAT ))) ^ (f2 . ( In ((n + 1), NAT )))) ^ ( Selfwork (nt,n))) by A5;

      hence ( SCM-Compile ((nt -tree (t1,t2)),n)) = ((( SCM-Compile (t1,n)) ^ ( SCM-Compile (t2,(n + 1)))) ^ ( Selfwork (nt,n))) by A3, A4, A2;

    end;

    definition

      let t be Terminal of SCM-AE ;

      :: SCM_COMP:def13

      func d". t -> Element of NAT means

      : Def13: ( dl. it ) = t;

      existence

      proof

        ( Terminals SCM-AE ) = [: {1}, NAT :] by Def1;

        then

        consider x,y be object such that

         A1: x in {1} and

         A2: y in NAT and

         A3: t = [x, y] by ZFMISC_1: 84;

        reconsider k = y as Element of NAT by A2;

        take k;

        thus thesis by A1, A3, TARSKI:def 1;

      end;

      uniqueness by AMI_3: 10;

    end

    definition

      deffunc V( Terminal of SCM-AE ) = ( d". $1);

      deffunc U( NonTerminal of SCM-AE , set, set, Element of NAT , Element of NAT ) = ( max ($4,$5));

      let term be bin-term;

      :: SCM_COMP:def14

      func max_Data-Loc_in term -> Element of NAT means

      : Def14: ex f be Function of ( TS SCM-AE ), NAT st it = (f . term) & (for t be Terminal of SCM-AE holds (f . ( root-tree t)) = ( d". t)) & for nt be NonTerminal of SCM-AE , tl,tr be bin-term, rtl,rtr be Symbol of SCM-AE st rtl = ( root-label tl) & rtr = ( root-label tr) & nt ==> <*rtl, rtr*> holds for xl,xr be Element of NAT st xl = (f . tl) & xr = (f . tr) holds (f . (nt -tree (tl,tr))) = ( max (xl,xr));

      existence

      proof

        consider f be Function of ( TS SCM-AE ), NAT such that

         A1: (for t be Terminal of SCM-AE holds (f . ( root-tree t)) = V(t)) & for nt be NonTerminal of SCM-AE , tl,tr be bin-term, rtl,rtr be Symbol of SCM-AE st rtl = ( root-label tl) & rtr = ( root-label tr) & nt ==> <*rtl, rtr*> holds for xl,xr be Element of NAT st xl = (f . tl) & xr = (f . tr) holds (f . (nt -tree (tl,tr))) = U(nt,rtl,rtr,xl,xr) from BINTREE1:sch 3;

        reconsider fterm = (f . term) as Element of NAT ;

        take fterm, f;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let it1,it2 be Element of NAT ;

        given f1 be Function of ( TS SCM-AE ), NAT such that

         A2: it1 = (f1 . term) and

         A3: (for t be Terminal of SCM-AE holds (f1 . ( root-tree t)) = V(t)) & for nt be NonTerminal of SCM-AE , tl,tr be bin-term, rtl,rtr be Symbol of SCM-AE st rtl = ( root-label tl) & rtr = ( root-label tr) & nt ==> <*rtl, rtr*> holds for xl,xr be Element of NAT st xl = (f1 . tl) & xr = (f1 . tr) holds (f1 . (nt -tree (tl,tr))) = U(nt,rtl,rtr,xl,xr);

        given f2 be Function of ( TS SCM-AE ), NAT such that

         A4: it2 = (f2 . term) and

         A5: (for t be Terminal of SCM-AE holds (f2 . ( root-tree t)) = V(t)) & for nt be NonTerminal of SCM-AE , tl,tr be bin-term, rtl,rtr be Symbol of SCM-AE st rtl = ( root-label tl) & rtr = ( root-label tr) & nt ==> <*rtl, rtr*> holds for xl,xr be Element of NAT st xl = (f2 . tl) & xr = (f2 . tr) holds (f2 . (nt -tree (tl,tr))) = U(nt,rtl,rtr,xl,xr);

        f1 = f2 from BINTREE1:sch 4( A3, A5);

        hence thesis by A2, A4;

      end;

    end

    set Term = the bin-term;

    consider f be Function of ( TS SCM-AE ), NAT such that ( max_Data-Loc_in Term) = (f . Term) and

     Lm4: for t be Terminal of SCM-AE holds (f . ( root-tree t)) = ( d". t) and

     Lm5: for nt be NonTerminal of SCM-AE , tl,tr be bin-term, rtl,rtr be Symbol of SCM-AE st rtl = ( root-label tl) & rtr = ( root-label tr) & nt ==> <*rtl, rtr*> holds for xl,xr be Element of NAT st xl = (f . tl) & xr = (f . tr) holds (f . (nt -tree (tl,tr))) = ( max (xl,xr)) by Def14;

    theorem :: SCM_COMP:9

    

     Th9: for t be Terminal of SCM-AE holds ( max_Data-Loc_in ( root-tree t)) = ( d". t)

    proof

      let t be Terminal of SCM-AE ;

      ( max_Data-Loc_in ( root-tree t)) = (f . ( root-tree t)) qua Element of NAT by Def14, Lm4, Lm5;

      hence thesis by Lm4;

    end;

    

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

    theorem :: SCM_COMP:10

    

     Th10: for nt be NonTerminal of SCM-AE , tl,tr be bin-term holds ( max_Data-Loc_in (nt -tree (tl,tr))) = ( max (( max_Data-Loc_in tl),( max_Data-Loc_in tr)))

    proof

      let nt be NonTerminal of SCM-AE , tl,tr be bin-term;

      

       A1: ( max_Data-Loc_in tl) = (f . tl) & ( max_Data-Loc_in tr) = (f . tr) by Def14, Lm4, Lm5;

      nt ==> <*( root-label tl), ( root-label tr)*> & ( max_Data-Loc_in (nt -tree (tl,tr))) = (f . (nt -tree (tl,tr))) by Def1, Def14, Lm4, Lm5, Lm6;

      hence thesis by A1, Lm5;

    end;

    defpred X[ bin-term] means for s1,s2 be State of SCM st for dn be Element of 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 ;

      thus X[( root-tree s)]

      proof

        let s1,s2 be State of SCM ;

        assume

         A1: for dn be Element of NAT st dn <= ( max_Data-Loc_in ( root-tree s)) holds (s1 . ( dl. dn)) = (s2 . ( dl. dn));

        ( 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 thesis by A2, A3, Th4;

      end;

    end;

     Lm8:

    now

      let nt be NonTerminal of SCM-AE , tl,tr be Element of ( TS SCM-AE );

      assume that nt ==> <*( root-label tl), ( root-label tr)*> and

       A1: X[tl] and

       A2: X[tr];

      thus X[(nt -tree (tl,tr))]

      proof

        let s1,s2 be State of SCM ;

        assume

         A3: for dn be Element of NAT st dn <= ( max_Data-Loc_in (nt -tree (tl,tr))) holds (s1 . ( dl. dn)) = (s2 . ( dl. dn));

        now

          set ml = ( max_Data-Loc_in tl), mr = ( max_Data-Loc_in tr);

          let dn be Element of NAT ;

          

           A4: ml <= ( max (ml,mr)) by XXREAL_0: 25;

          assume dn <= ( max_Data-Loc_in tl);

          then dn <= ( max (ml,mr)) 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;

        end;

        then

         A5: (tl @ s1) = (tl @ s2) by A1;

        now

          set ml = ( max_Data-Loc_in tl), mr = ( max_Data-Loc_in tr);

          let dn be Element of NAT ;

          

           A6: mr <= ( max (ml,mr)) by XXREAL_0: 25;

          assume dn <= ( max_Data-Loc_in tr);

          then dn <= ( max (ml,mr)) 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;

        end;

        then

         A7: (tr @ s1) = (tr @ s2) by A2;

        ((nt -tree (tl,tr)) @ s1) = (nt -Meaning_on ((tl @ s1),(tr @ s1))) by Th5;

        hence thesis by A5, A7, Th5;

      end;

    end;

    theorem :: SCM_COMP:11

    

     Th11: for term be bin-term, s1,s2 be State of SCM st for dn be Element of NAT st dn <= ( max_Data-Loc_in term) holds (s1 . ( dl. dn)) = (s2 . ( dl. dn)) holds (term @ s1) = (term @ s2)

    proof

      thus for t be bin-term holds X[t] from BINTREE1:sch 2( Lm7, Lm8);

    end;

    reserve F for Instruction-Sequence of SCM ;

    defpred P[ bin-term] means for F holds for aux,n be Element of NAT st ( Shift (( SCM-Compile ($1,aux)),n)) c= F holds for s be n -started State of SCM st aux > ( max_Data-Loc_in $1) holds ex i be Element of NAT , u be 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 be Element of NAT st dn < aux holds (s . ( dl. dn)) = (u . ( dl. dn));

    theorem :: SCM_COMP:12

    

     Th12: for F holds for term be bin-term holds for aux,n be Element of NAT st ( Shift (( SCM-Compile (term,aux)),n)) c= F holds for s be n -started State of SCM st aux > ( max_Data-Loc_in term) holds ex i be Element of NAT , u be 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 be Element of NAT st dn < aux holds (s . ( dl. dn)) = (u . ( dl. dn))

    proof

      

       A1: for nt be NonTerminal of SCM-AE , tl,tr be bin-term st nt ==> <*( root-label tl), ( root-label tr)*> & P[tl] & P[tr] holds P[(nt -tree (tl,tr))]

      proof

        let nt be NonTerminal of SCM-AE , tl,tr be bin-term;

        assume that

         A2: nt ==> <*( root-label tl), ( root-label tr)*> and

         A3: P[tl] and

         A4: P[tr];

        let F;

        let aux,n be Element of NAT such that

         A5: ( Shift (( SCM-Compile ((nt -tree (tl,tr)),aux)),n)) c= F;

        let s be n -started State of SCM ;

        assume

         A6: aux > ( max_Data-Loc_in (nt -tree (tl,tr)));

        

         A7: ( max_Data-Loc_in (nt -tree (tl,tr))) = ( max (( max_Data-Loc_in tl),( max_Data-Loc_in tr))) by Th10;

        then ( max_Data-Loc_in tl) <= ( max_Data-Loc_in (nt -tree (tl,tr))) by XXREAL_0: 25;

        then

         A8: ( max_Data-Loc_in tl) < aux by A6, XXREAL_0: 2;

        ( max_Data-Loc_in tr) <= ( max_Data-Loc_in (nt -tree (tl,tr))) by A7, XXREAL_0: 25;

        then

         A9: ( max_Data-Loc_in tr) < aux by A6, XXREAL_0: 2;

        then

         A10: ( max_Data-Loc_in tr) < (aux + 1) by NAT_1: 13;

        

         A11: ( SCM-Compile ((nt -tree (tl,tr)),aux)) = ((( SCM-Compile (tl,aux)) ^ ( SCM-Compile (tr,(aux + 1)))) ^ ( Selfwork (nt,aux))) by A2, Th8;

        then ( SCM-Compile ((nt -tree (tl,tr)),aux)) = (( SCM-Compile (tl,aux)) ^ (( SCM-Compile (tr,(aux + 1))) ^ ( Selfwork (nt,aux)))) by AFINSQ_1: 27;

        then ( Shift (( SCM-Compile (tl,aux)),n)) c= F by A5, AFINSQ_1: 82;

        then

        consider i1 be Element of NAT , u1 be State of SCM such that

         A12: u1 = ( Comput (F,s,(i1 + 1))) and

         A13: (i1 + 1) = ( len ( SCM-Compile (tl,aux))) and ( IC ( Comput (F,s,i1))) = (n + i1) and

         A14: ( IC u1) = (n + (i1 + 1)) and

         A15: (u1 . ( dl. aux)) = (tl @ s) and

         A16: for dn be Element of NAT st dn < aux holds (s . ( dl. dn)) = (u1 . ( dl. dn)) by A3, A8;

        

         A17: u1 is (n + (i1 + 1)) -started State of SCM by A14, MEMSTR_0:def 12;

        ( SCM-Compile ((nt -tree (tl,tr)),aux)) = (( SCM-Compile (tl,aux)) ^ (( SCM-Compile (tr,(aux + 1))) ^ ( Selfwork (nt,aux)))) by A11, AFINSQ_1: 27;

        then ( Shift ((( SCM-Compile (tr,(aux + 1))) ^ ( Selfwork (nt,aux))),(n + (i1 + 1)))) c= F by A5, A13, AFINSQ_1: 83;

        then ( Shift (( SCM-Compile (tr,(aux + 1))),(n + (i1 + 1)))) c= F by AFINSQ_1: 82;

        then

        consider i2 be Element of NAT , u2 be State of SCM such that

         A18: u2 = ( Comput (F,u1,(i2 + 1))) and

         A19: (i2 + 1) = ( len ( SCM-Compile (tr,(aux + 1)))) and ( IC ( Comput (F,u1,i2))) = ((n + (i1 + 1)) + i2) and

         A20: ( IC u2) = ((n + (i1 + 1)) + (i2 + 1)) and

         A21: (u2 . ( dl. (aux + 1))) = (tr @ u1) and

         A22: for dn be Element of NAT st dn < (aux + 1) holds (u1 . ( dl. dn)) = (u2 . ( dl. dn)) by A4, A10, A17;

        

         A23: u2 = ( Comput (F,s,((i1 + 1) + (i2 + 1)))) by A12, A18, EXTPRO_1: 4;

         A24:

        now

          let n be Element of NAT ;

          assume n <= ( max_Data-Loc_in tr);

          then n < aux by A9, XXREAL_0: 2;

          hence (s . ( dl. n)) = (u1 . ( dl. n)) by A16;

        end;

        

         A25: aux < (aux + 1) by NAT_1: 13;

        

         A26: ((nt -tree (tl,tr)) @ s) = (nt -Meaning_on ((tl @ s),(tr @ s))) by Th5;

        

         A27: ( len (( SCM-Compile (tl,aux)) ^ ( SCM-Compile (tr,(aux + 1))))) = ((i1 + 1) + (i2 + 1)) by A13, A19, AFINSQ_1: 17;

        nt = [ 0 , 0 ] or ... or nt = [ 0 , 4] by Th1;

        per cases ;

          suppose

           A28: nt = [ 0 , 0 ];

          then

           A29: (nt -Meaning_on ((tl @ s),(tr @ s))) = ((tl @ s) + (tr @ s)) by Def8;

          take i = ((i1 + 1) + (i2 + 1)), u = ( Comput (F,s,(i + 1)));

          thus u = ( Comput (F,s,(i + 1)));

          

           A30: ( Selfwork (nt,aux)) = <%( AddTo (( dl. aux),( dl. (aux + 1))))%> by A28, Def10;

          then

           A31: ( len ( Selfwork (nt,aux))) = 1 by AFINSQ_1: 34;

          hence (i + 1) = ( len ( SCM-Compile ((nt -tree (tl,tr)),aux))) by A11, A27, AFINSQ_1: 17;

          thus ( IC ( Comput (F,s,i))) = (n + i) by A12, A18, A20, EXTPRO_1: 4;

          ( len ( SCM-Compile ((nt -tree (tl,tr)),aux))) = (((i1 + 1) + (i2 + 1)) + 1) by A11, A27, A31, AFINSQ_1: 17;

          then i < ( len ( SCM-Compile ((nt -tree (tl,tr)),aux))) by NAT_1: 13;

          then i in ( dom ( SCM-Compile ((nt -tree (tl,tr)),aux))) by AFINSQ_1: 86;

          

          then

           A32: (F . (n + i)) = (( SCM-Compile ((nt -tree (tl,tr)),aux)) . i) by A5, VALUED_1: 51

          .= ( AddTo (( dl. aux),( dl. (aux + 1)))) by A27, A11, A30, AFINSQ_1: 36;

          

          hence ( IC u) = ((n + i) + 1) by A20, A23, SCM_1: 5

          .= (n + (i + 1));

          

          thus (u . ( dl. aux)) = ((u2 . ( dl. aux)) + (u2 . ( dl. (aux + 1)))) by A20, A23, A32, SCM_1: 5

          .= ((u1 . ( dl. aux)) + (tr @ u1)) by A21, A22, A25

          .= ((nt -tree (tl,tr)) @ s) by A15, A26, A24, A29, Th11;

          let dn be Element of NAT ;

          assume

           A33: dn < aux;

          then dn < (aux + 1) by NAT_1: 13;

          then

           A34: (u1 . ( dl. dn)) = (u2 . ( dl. dn)) by A22;

          ( dl. dn) <> ( dl. aux) by A33, AMI_3: 10;

          then (u . ( dl. dn)) = (u2 . ( dl. dn)) by A20, A23, A32, SCM_1: 5;

          hence thesis by A16, A33, A34;

        end;

          suppose

           A35: nt = [ 0 , 1];

          then

           A36: (nt -Meaning_on ((tl @ s),(tr @ s))) = ((tl @ s) - (tr @ s)) by Def8;

          take i = ((i1 + 1) + (i2 + 1)), u = ( Comput (F,s,(i + 1)));

          thus u = ( Comput (F,s,(i + 1)));

          

           A37: ( Selfwork (nt,aux)) = <%( SubFrom (( dl. aux),( dl. (aux + 1))))%> by A35, Def10;

          then

           A38: ( len ( Selfwork (nt,aux))) = 1 by AFINSQ_1: 34;

          hence (i + 1) = ( len ( SCM-Compile ((nt -tree (tl,tr)),aux))) by A11, A27, AFINSQ_1: 17;

          thus ( IC ( Comput (F,s,i))) = (n + i) by A12, A18, A20, EXTPRO_1: 4;

          ( len ( SCM-Compile ((nt -tree (tl,tr)),aux))) = (((i1 + 1) + (i2 + 1)) + 1) by A11, A27, A38, AFINSQ_1: 17;

          then i < ( len ( SCM-Compile ((nt -tree (tl,tr)),aux))) by NAT_1: 13;

          then i in ( dom ( SCM-Compile ((nt -tree (tl,tr)),aux))) by AFINSQ_1: 86;

          

          then

           A39: (F . (n + i)) = (( SCM-Compile ((nt -tree (tl,tr)),aux)) . i) by A5, VALUED_1: 51

          .= ( SubFrom (( dl. aux),( dl. (aux + 1)))) by A11, A27, A37, AFINSQ_1: 36;

          

          hence ( IC u) = ((n + i) + 1) by A20, A23, SCM_1: 6

          .= (n + (i + 1));

          

          thus (u . ( dl. aux)) = ((u2 . ( dl. aux)) - (u2 . ( dl. (aux + 1)))) by A20, A23, A39, SCM_1: 6

          .= ((u1 . ( dl. aux)) - (tr @ u1)) by A21, A22, A25

          .= ((nt -tree (tl,tr)) @ s) by A15, A26, A24, A36, Th11;

          let dn be Element of NAT ;

          assume

           A40: dn < aux;

          then dn < (aux + 1) by NAT_1: 13;

          then

           A41: (u1 . ( dl. dn)) = (u2 . ( dl. dn)) by A22;

          ( dl. dn) <> ( dl. aux) by A40, AMI_3: 10;

          then (u . ( dl. dn)) = (u2 . ( dl. dn)) by A20, A23, A39, SCM_1: 6;

          hence thesis by A16, A40, A41;

        end;

          suppose

           A42: nt = [ 0 , 2];

          then

           A43: (nt -Meaning_on ((tl @ s),(tr @ s))) = ((tl @ s) * (tr @ s)) by Def8;

          take i = ((i1 + 1) + (i2 + 1)), u = ( Comput (F,s,(i + 1)));

          thus u = ( Comput (F,s,(i + 1)));

          

           A44: ( Selfwork (nt,aux)) = <%( MultBy (( dl. aux),( dl. (aux + 1))))%> by A42, Def10;

          then

           A45: ( len ( Selfwork (nt,aux))) = 1 by AFINSQ_1: 34;

          hence (i + 1) = ( len ( SCM-Compile ((nt -tree (tl,tr)),aux))) by A11, A27, AFINSQ_1: 17;

          thus ( IC ( Comput (F,s,i))) = (n + i) by A12, A18, A20, EXTPRO_1: 4;

          ( len ( SCM-Compile ((nt -tree (tl,tr)),aux))) = (((i1 + 1) + (i2 + 1)) + 1) by A11, A27, A45, AFINSQ_1: 17;

          then i < ( len ( SCM-Compile ((nt -tree (tl,tr)),aux))) by NAT_1: 13;

          then i in ( dom ( SCM-Compile ((nt -tree (tl,tr)),aux))) by AFINSQ_1: 86;

          

          then

           A46: (F . (n + i)) = (( SCM-Compile ((nt -tree (tl,tr)),aux)) . i) by A5, VALUED_1: 51

          .= ( MultBy (( dl. aux),( dl. (aux + 1)))) by A11, A27, A44, AFINSQ_1: 36;

          

          hence ( IC u) = ((n + i) + 1) by A20, A23, SCM_1: 7

          .= (n + (i + 1));

          

          thus (u . ( dl. aux)) = ((u2 . ( dl. aux)) * (u2 . ( dl. (aux + 1)))) by A20, A23, A46, SCM_1: 7

          .= ((u1 . ( dl. aux)) * (tr @ u1)) by A21, A22, A25

          .= ((nt -tree (tl,tr)) @ s) by A15, A26, A24, A43, Th11;

          let dn be Element of NAT ;

          assume

           A47: dn < aux;

          then dn < (aux + 1) by NAT_1: 13;

          then

           A48: (u1 . ( dl. dn)) = (u2 . ( dl. dn)) by A22;

          ( dl. dn) <> ( dl. aux) by A47, AMI_3: 10;

          then (u . ( dl. dn)) = (u2 . ( dl. dn)) by A20, A23, A46, SCM_1: 7;

          hence thesis by A16, A47, A48;

        end;

          suppose

           A49: nt = [ 0 , 3];

          take i = ((i1 + 1) + (i2 + 1)), u = ( Comput (F,s,(i + 1)));

          thus u = ( Comput (F,s,(i + 1)));

          

           A50: ( Selfwork (nt,aux)) = <%( Divide (( dl. aux),( dl. (aux + 1))))%> by A49, Def10;

          then

           A51: ( len ( Selfwork (nt,aux))) = 1 by AFINSQ_1: 34;

          hence (i + 1) = ( len ( SCM-Compile ((nt -tree (tl,tr)),aux))) by A11, A27, AFINSQ_1: 17;

          ( len ( SCM-Compile ((nt -tree (tl,tr)),aux))) = (((i1 + 1) + (i2 + 1)) + 1) by A11, A27, A51, AFINSQ_1: 17;

          then i < ( len ( SCM-Compile ((nt -tree (tl,tr)),aux))) by NAT_1: 13;

          then i in ( dom ( SCM-Compile ((nt -tree (tl,tr)),aux))) by AFINSQ_1: 86;

          

          then

           A52: (F . (n + i)) = (( SCM-Compile ((nt -tree (tl,tr)),aux)) . i) by A5, VALUED_1: 51

          .= ( Divide (( dl. aux),( dl. (aux + 1)))) by A11, A27, A50, AFINSQ_1: 36;

          thus ( IC ( Comput (F,s,i))) = (n + i) by A12, A18, A20, EXTPRO_1: 4;

          

           A53: (nt -Meaning_on ((tl @ s),(tr @ s))) = ((tl @ s) div (tr @ s)) by A49, Def8;

          aux <> (aux + 1);

          then

           A54: ( dl. aux) <> ( dl. (aux + 1)) by AMI_3: 10;

          

          hence ( IC u) = ((n + i) + 1) by A20, A23, A52, SCM_1: 8

          .= (n + (i + 1));

          

          thus (u . ( dl. aux)) = ((u2 . ( dl. aux)) div (u2 . ( dl. (aux + 1)))) by A20, A23, A52, A54, SCM_1: 8

          .= ((u1 . ( dl. aux)) div (tr @ u1)) by A21, A22, A25

          .= ((nt -tree (tl,tr)) @ s) by A15, A26, A24, A53, Th11;

          let dn be Element of NAT ;

          assume

           A55: dn < aux;

          then

           A56: dn < (aux + 1) by NAT_1: 13;

          then

           A57: ( dl. dn) <> ( dl. (aux + 1)) by AMI_3: 10;

          

           A58: (u1 . ( dl. dn)) = (u2 . ( dl. dn)) by A22, A56;

          ( dl. dn) <> ( dl. aux) by A55, AMI_3: 10;

          then (u . ( dl. dn)) = (u2 . ( dl. dn)) by A20, A23, A52, A54, A57, SCM_1: 8;

          hence thesis by A16, A55, A58;

        end;

          suppose

           A59: nt = [ 0 , 4];

          then

           A60: (nt -Meaning_on ((tl @ s),(tr @ s))) = ((tl @ s) mod (tr @ s)) by Def8;

          set i = ((i1 + 1) + (i2 + 1)), u = ( Comput (F,s,(i + 1)));

          take k = (i + 1), v = ( Comput (F,s,(k + 1)));

          thus v = ( Comput (F,s,(k + 1)));

          

           A61: ( Selfwork (nt,aux)) = <%( Divide (( dl. aux),( dl. (aux + 1)))), (( dl. aux) := ( dl. (aux + 1)))%> by A59, Def10;

          then

           A62: ( len ( Selfwork (nt,aux))) = 2 by AFINSQ_1: 38;

          then

           A63: 0 in ( dom ( Selfwork (nt,aux))) by CARD_1: 50, TARSKI:def 2;

          

           A64: ( len ( SCM-Compile ((nt -tree (tl,tr)),aux))) = (((i1 + 1) + (i2 + 1)) + (1 + 1)) by A11, A27, A62, AFINSQ_1: 17;

          hence (k + 1) = ( len ( SCM-Compile ((nt -tree (tl,tr)),aux)));

          

           A65: 1 in ( dom ( Selfwork (nt,aux))) by A62, CARD_1: 50, TARSKI:def 2;

          k < ( len ( SCM-Compile ((nt -tree (tl,tr)),aux))) by A64, XREAL_1: 6;

          then k in ( dom ( SCM-Compile ((nt -tree (tl,tr)),aux))) by AFINSQ_1: 86;

          

          then

           A66: (F . (n + k)) = (( SCM-Compile ((nt -tree (tl,tr)),aux)) . k) by A5, VALUED_1: 51

          .= (( Selfwork (nt,aux)) . 1) by A11, A27, A65, AFINSQ_1:def 3

          .= (( dl. aux) := ( dl. (aux + 1))) by A61;

          (i + 0 ) = i;

          then i < ( len ( SCM-Compile ((nt -tree (tl,tr)),aux))) by A64, XREAL_1: 6;

          then i in ( dom ( SCM-Compile ((nt -tree (tl,tr)),aux))) by AFINSQ_1: 86;

          

          then

           A67: (F . (n + i)) = (( SCM-Compile ((nt -tree (tl,tr)),aux)) . (i + 0 )) by A5, VALUED_1: 51

          .= (( Selfwork (nt,aux)) . 0 ) by A11, A27, A63, AFINSQ_1:def 3

          .= ( Divide (( dl. aux),( dl. (aux + 1)))) by A61;

          aux <> (aux + 1);

          then

           A68: ( dl. aux) <> ( dl. (aux + 1)) by AMI_3: 10;

          

          hence

           A69: ( IC ( Comput (F,s,k))) = ((n + i) + 1) by A20, A23, A67, SCM_1: 8

          .= (n + k);

          

          hence ( IC v) = ((n + k) + 1) by A66, SCM_1: 4

          .= (n + (k + 1));

          

          thus (v . ( dl. aux)) = (u . ( dl. (aux + 1))) by A66, A69, SCM_1: 4

          .= ((u2 . ( dl. aux)) mod (u2 . ( dl. (aux + 1)))) by A20, A23, A67, A68, SCM_1: 8

          .= ((u1 . ( dl. aux)) mod (tr @ u1)) by A21, A22, A25

          .= ((nt -tree (tl,tr)) @ s) by A15, A26, A24, A60, Th11;

          let dn be Element of NAT ;

          assume

           A70: dn < aux;

          then

           A71: ( dl. dn) <> ( dl. aux) by AMI_3: 10;

          

           A72: dn < (aux + 1) by A70, NAT_1: 13;

          then

           A73: (u1 . ( dl. dn)) = (u2 . ( dl. dn)) by A22;

          ( dl. dn) <> ( dl. (aux + 1)) by A72, AMI_3: 10;

          then (u . ( dl. dn)) = (u2 . ( dl. dn)) by A20, A23, A67, A68, A71, SCM_1: 8;

          then (s . ( dl. dn)) = (u . ( dl. dn)) by A16, A70, A73;

          hence thesis by A66, A69, A71, SCM_1: 4;

        end;

      end;

      

       A74: for t be Terminal of SCM-AE holds P[( root-tree t)]

      proof

        let t be Terminal of SCM-AE ;

        let F;

        let aux,n be Element of NAT such that

         A75: ( Shift (( SCM-Compile (( root-tree t),aux)),n)) c= F;

        let s be n -started State of SCM ;

        assume aux > ( max_Data-Loc_in ( root-tree t));

        take i = 0 , u = ( Comput (F,s,( 0 + 1)));

        thus u = ( Comput (F,s,(i + 1)));

        

         A76: ( <%(( dl. aux) := ( @ t))%> . 0 ) = (( dl. aux) := ( @ t));

        

         A77: ( SCM-Compile (( root-tree t),aux)) = <%(( dl. aux) := ( @ t))%> by Th7;

        hence (i + 1) = ( len ( SCM-Compile (( root-tree t),aux))) by AFINSQ_1: 34;

        

         A78: s = ( Comput (F,s, 0 )) by EXTPRO_1: 2;

        hence ( IC ( Comput (F,s,i))) = (n + i) by MEMSTR_0:def 12;

        ( len <%(( dl. aux) := ( @ t))%>) = 1 & (n + 0 ) = n by AFINSQ_1: 34;

        then i in ( dom ( SCM-Compile (( root-tree t),aux))) by A77, AFINSQ_1: 86;

        then

         A79: ( IC s) = n & (F . (n + 0 )) = (( dl. aux) := ( @ t)) by A77, A76, A75, MEMSTR_0:def 12, VALUED_1: 51;

        hence ( IC u) = (n + (i + 1)) by A78, SCM_1: 4;

        

        thus (u . ( dl. aux)) = (s . t) by A78, A79, SCM_1: 4

        .= (( root-tree t) @ s) by Th4;

        let dn be Element of NAT ;

        assume dn < aux;

        then ( dl. dn) <> ( dl. aux) by AMI_3: 10;

        hence thesis by A78, A79, SCM_1: 4;

      end;

      for term be bin-term holds P[term] from BINTREE1:sch 2( A74, A1);

      hence thesis;

    end;

    theorem :: SCM_COMP:13

    for F holds for term be bin-term, aux,n be Element of NAT st ( Shift ((( SCM-Compile (term,aux)) ^ <%( halt SCM )%>),n)) c= F holds for s be n -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)))

    proof

      let F;

      let term be bin-term, aux,n be Element of NAT such that

       A1: ( Shift ((( SCM-Compile (term,aux)) ^ <%( halt SCM )%>),n)) c= F;

      let s be n -started State of SCM ;

      assume

       A2: aux > ( max_Data-Loc_in term);

      ( Shift (( SCM-Compile (term,aux)),n)) c= F by A1, AFINSQ_1: 82;

      then

      consider i be Element of NAT , u be State of SCM such that

       A3: u = ( Comput (F,s,(i + 1))) and

       A4: (i + 1) = ( len ( SCM-Compile (term,aux))) and

       A5: ( IC ( Comput (F,s,i))) = (n + i) and

       A6: ( IC u) = (n + (i + 1)) and

       A7: (u . ( dl. aux)) = (term @ s) and for dn be Element of NAT st dn < aux holds (s . ( dl. dn)) = (u . ( dl. dn)) by A2, Th12;

      ( len <%( halt SCM )%>) = 1 by AFINSQ_1: 34;

      then ( len (( SCM-Compile (term,aux)) ^ <%( halt SCM )%>)) = ((i + 1) + 1) by A4, AFINSQ_1: 17;

      then (i + 1) < ( len (( SCM-Compile (term,aux)) ^ <%( halt SCM )%>)) by NAT_1: 13;

      then (i + 1) in ( dom (( SCM-Compile (term,aux)) ^ <%( halt SCM )%>)) by AFINSQ_1: 86;

      

      then

       A8: (F . (n + (i + 1))) = ((( SCM-Compile (term,aux)) ^ <%( halt SCM )%>) . (i + 1)) by A1, VALUED_1: 51

      .= ( halt SCM ) by A4, AFINSQ_1: 36;

      hence F halts_on s by A3, A6, EXTPRO_1: 30;

      thus (( Result (F,s)) . ( dl. aux)) = (term @ s) by A3, A6, A7, A8, EXTPRO_1: 7;

      (n + i) <> (n + (i + 1));

      hence thesis by A3, A4, A5, A6, A8, EXTPRO_1: 33;

    end;