prelamb.miz

    begin

    definition

      struct ( 1-sorted) typealg (# the carrier -> set,

the left_quotient, right_quotient, inner_product -> BinOp of the carrier #)

       attr strict strict;

    end

    registration

      cluster non empty strict for typealg;

      existence

      proof

        set l = the BinOp of { {} };

        take typealg (# { {} }, l, l, l #);

        thus the carrier of typealg (# { {} }, l, l, l #) is non empty;

        thus thesis;

      end;

    end

    definition

      let s be non empty typealg;

      mode type of s is Element of s;

    end

    reserve s for non empty typealg,

T,X,Y,T9,X9,Y9 for FinSequence of s,

x,y,z,y9,z9 for type of s;

    definition

      let s, x, y;

      :: PRELAMB:def1

      func x \ y -> type of s equals (the left_quotient of s . (x,y));

      coherence ;

      :: PRELAMB:def2

      func x /" y -> type of s equals (the right_quotient of s . (x,y));

      coherence ;

      :: PRELAMB:def3

      func x * y -> type of s equals (the inner_product of s . (x,y));

      coherence ;

    end

    definition

      let s;

      mode PreProof of s is finite DecoratedTree of [: [:(the carrier of s * ), the carrier of s:], NAT :];

    end

    reserve Tr for PreProof of s;

    definition

      let s, Tr;

      let v be Element of ( dom Tr);

      :: PRELAMB:def4

      attr v is correct means

      : Def4: ( branchdeg v) = 0 & ex x st ((Tr . v) `1 ) = [ <*x*>, x] if ((Tr . v) `2 ) = 0 ,

( branchdeg v) = 1 & ex T, x, y st ((Tr . v) `1 ) = [T, (x /" y)] & ((Tr . (v ^ <* 0 *>)) `1 ) = [(T ^ <*y*>), x] if ((Tr . v) `2 ) = 1,

( branchdeg v) = 1 & ex T, x, y st ((Tr . v) `1 ) = [T, (y \ x)] & ((Tr . (v ^ <* 0 *>)) `1 ) = [( <*y*> ^ T), x] if ((Tr . v) `2 ) = 2,

( branchdeg v) = 2 & ex T, X, Y, x, y, z st ((Tr . v) `1 ) = [(((X ^ <*(x /" y)*>) ^ T) ^ Y), z] & ((Tr . (v ^ <* 0 *>)) `1 ) = [T, y] & ((Tr . (v ^ <*1*>)) `1 ) = [((X ^ <*x*>) ^ Y), z] if ((Tr . v) `2 ) = 3,

( branchdeg v) = 2 & ex T, X, Y, x, y, z st ((Tr . v) `1 ) = [(((X ^ T) ^ <*(y \ x)*>) ^ Y), z] & ((Tr . (v ^ <* 0 *>)) `1 ) = [T, y] & ((Tr . (v ^ <*1*>)) `1 ) = [((X ^ <*x*>) ^ Y), z] if ((Tr . v) `2 ) = 4,

( branchdeg v) = 1 & ex X, x, y, Y st ((Tr . v) `1 ) = [((X ^ <*(x * y)*>) ^ Y), z] & ((Tr . (v ^ <* 0 *>)) `1 ) = [(((X ^ <*x*>) ^ <*y*>) ^ Y), z] if ((Tr . v) `2 ) = 5,

( branchdeg v) = 2 & ex X, Y, x, y st ((Tr . v) `1 ) = [(X ^ Y), (x * y)] & ((Tr . (v ^ <* 0 *>)) `1 ) = [X, x] & ((Tr . (v ^ <*1*>)) `1 ) = [Y, y] if ((Tr . v) `2 ) = 6,

( branchdeg v) = 2 & ex T, X, Y, y, z st ((Tr . v) `1 ) = [((X ^ T) ^ Y), z] & ((Tr . (v ^ <* 0 *>)) `1 ) = [T, y] & ((Tr . (v ^ <*1*>)) `1 ) = [((X ^ <*y*>) ^ Y), z] if ((Tr . v) `2 ) = 7

      otherwise contradiction;

      correctness ;

    end

    definition

      let s;

      let IT be type of s;

      :: PRELAMB:def5

      attr IT is left means ex x, y st IT = (x \ y);

      :: PRELAMB:def6

      attr IT is right means ex x, y st IT = (x /" y);

      :: PRELAMB:def7

      attr IT is middle means ex x, y st IT = (x * y);

    end

    definition

      let s;

      let IT be type of s;

      :: PRELAMB:def8

      attr IT is primitive means not (IT is left or IT is right or IT is middle);

    end

    definition

      let s;

      let Tr be finite DecoratedTree of the carrier of s;

      let v be Element of ( dom Tr);

      :: original: .

      redefine

      func Tr . v -> type of s ;

      coherence

      proof

        reconsider Tr as DecoratedTree of the carrier of s;

        reconsider v as Element of ( dom Tr);

        (Tr . v) is type of s;

        hence thesis;

      end;

    end

    definition

      let s;

      let Tr be finite DecoratedTree of the carrier of s, x;

      :: PRELAMB:def9

      pred Tr represents x means ( dom Tr) is finite & for v be Element of ( dom Tr) holds (( branchdeg v) = 0 or ( branchdeg v) = 2) & (( branchdeg v) = 0 implies (Tr . v) is primitive) & (( branchdeg v) = 2 implies ex y, z st ((Tr . v) = (y /" z) or (Tr . v) = (y \ z) or (Tr . v) = (y * z)) & (Tr . (v ^ <* 0 *>)) = y & (Tr . (v ^ <*1*>)) = z);

    end

    notation

      let s;

      let Tr be finite DecoratedTree of the carrier of s, x;

      antonym Tr does_not_represent x for Tr represents x;

    end

    definition

      let IT be non empty typealg;

      :: PRELAMB:def10

      attr IT is free means not (ex x be type of IT st x is left right or x is left middle or x is right middle) & for x be type of IT holds ex Tr be finite DecoratedTree of the carrier of IT st for Tr1 be finite DecoratedTree of the carrier of IT holds Tr1 represents x iff Tr = Tr1;

    end

    definition

      let s, x;

      :: PRELAMB:def11

      func repr_of x -> finite DecoratedTree of the carrier of s means for Tr be finite DecoratedTree of the carrier of s holds Tr represents x iff it = Tr;

      existence by A1;

      uniqueness ;

    end

    deffunc PAIRSOF( typealg) = [:(the carrier of $1 * ), the carrier of $1:];

    definition

      let s;

      let f be FinSequence of s;

      let t be type of s;

      :: original: [

      redefine

      func [f,t] -> Element of [:(the carrier of s * ), the carrier of s:] ;

      coherence

      proof

        f in (the carrier of s * ) by FINSEQ_1:def 11;

        hence thesis by ZFMISC_1: 87;

      end;

    end

    definition

      let s;

      :: PRELAMB:def12

      mode Proof of s -> PreProof of s means

      : Def12: ( dom it ) is finite & for v be Element of ( dom it ) holds v is correct;

      existence

      proof

        set x = the type of s;

        set Tr = ( { {} } --> [ [ <*x*>, x], 0 ]);



         A1: ( dom Tr) = { {} } by FUNCOP_1: 13;

        reconsider Tr as finite DecoratedTree by TREES_1: 23;



         A2: [ [ <*x*>, x], 0 ] in [: PAIRSOF(s), NAT :] by ZFMISC_1: 87;

         { [ [ <*x*>, x], 0 ]} = ( rng Tr) by FUNCOP_1: 8;

        then ( rng Tr) c= [: PAIRSOF(s), NAT :] by A2, ZFMISC_1: 31;

        then

        reconsider Tr as PreProof of s by RELAT_1:def 19;

        take Tr;

        thus ( dom Tr) is finite;

        let v be Element of ( dom Tr);



         A3: v = {} by A1, TARSKI:def 1;

         A4:

        now

          set x = the Element of (( dom Tr) -level 1);

          assume (( dom Tr) -level 1) <> {} ;

          then x in (( dom Tr) -level 1);

          then x in { w where w be Element of ( dom Tr) : ( len w) = 1 } by TREES_2:def 6;

          then ex w be Element of ( dom Tr) st (x = w) & (( len w) = 1);

          hence contradiction by A1, CARD_1: 27, TARSKI:def 1;

        end;



         A5: ( branchdeg v) = ( card ( succ v)) by TREES_2:def 12

        .= 0 by A3, A4, CARD_1: 27, TREES_2: 13;



         A6: (Tr . v) = [ [ <*x*>, x], 0 ] by A1, FUNCOP_1: 7;

        then

         A7: ((Tr . v) `1 ) = [ <*x*>, x];

        ((Tr . v) `2 ) = 0 by A6;

        hence thesis by A5, A7, Def4;

      end;

    end

    reserve p for Proof of s,

v for Element of ( dom p);

    theorem :: PRELAMB:1



     Th1: ( branchdeg v) = 1 implies (v ^ <* 0 *>) in ( dom p)

    proof

      assume ( branchdeg v) = 1;

      then

       A1: ( succ v) <> {} by CARD_1: 27, TREES_2:def 12;

      set x = the Element of ( succ v);

      x in ( succ v) by A1;

      then x in { (v ^ <*n*>) where n be Nat : (v ^ <*n*>) in ( dom p) } by TREES_2:def 5;

      then

      consider n be Nat such that x = (v ^ <*n*>) and

       A2: (v ^ <*n*>) in ( dom p);

      thus thesis by A2, TREES_1:def 3;

    end;

    theorem :: PRELAMB:2



     Th2: ( branchdeg v) = 2 implies (v ^ <* 0 *>) in ( dom p) & (v ^ <*1*>) in ( dom p)

    proof



       A1: ( succ v) = { (v ^ <*n*>) where n be Nat : (v ^ <*n*>) in ( dom p) } by TREES_2:def 5;

      assume ( branchdeg v) = 2;

      then ( card ( succ v)) = 2 by TREES_2:def 12;

      then

      consider x,y be object such that

       A2: x <> y and

       A3: ( succ v) = {x, y} by CARD_2: 60;

      x in ( succ v) by A3, TARSKI:def 2;

      then

      consider n be Nat such that

       A4: x = (v ^ <*n*>) and

       A5: (v ^ <*n*>) in ( dom p) by A1;

      y in ( succ v) by A3, TARSKI:def 2;

      then

      consider k be Nat such that

       A6: y = (v ^ <*k*>) and

       A7: (v ^ <*k*>) in ( dom p) by A1;

      n <> 0 or k <> 0 by A2, A4, A6;

      then

       A8: n > 0 or k > 0 ;

      thus (v ^ <* 0 *>) in ( dom p) by A5, TREES_1:def 3;

      n >= ( 0 + 1) or k >= ( 0 + 1) by A8, NAT_1: 13;

      hence thesis by A5, A7, TREES_1:def 3;

    end;

    theorem :: PRELAMB:3

    ((p . v) `2 ) = 0 implies ex x st ((p . v) `1 ) = [ <*x*>, x]

    proof

      v is correct by Def12;

      hence thesis by Def4;

    end;

    theorem :: PRELAMB:4

    ((p . v) `2 ) = 1 implies ex w be Element of ( dom p), T, x, y st w = (v ^ <* 0 *>) & ((p . v) `1 ) = [T, (x /" y)] & ((p . w) `1 ) = [(T ^ <*y*>), x]

    proof



       A1: v is correct by Def12;

      assume

       A2: ((p . v) `2 ) = 1;

      then

       A3: ex T, x, y st ((p . v) `1 ) = [T, (x /" y)] & ((p . (v ^ <* 0 *>)) `1 ) = [(T ^ <*y*>), x] by A1, Def4;

      ( branchdeg v) = 1 by A1, A2, Def4;

      then (v ^ <* 0 *>) in ( dom p) by Th1;

      hence thesis by A3;

    end;

    theorem :: PRELAMB:5

    ((p . v) `2 ) = 2 implies ex w be Element of ( dom p), T, x, y st w = (v ^ <* 0 *>) & ((p . v) `1 ) = [T, (y \ x)] & ((p . w) `1 ) = [( <*y*> ^ T), x]

    proof



       A1: v is correct by Def12;

      assume

       A2: ((p . v) `2 ) = 2;

      then

       A3: ex T, x, y st ((p . v) `1 ) = [T, (y \ x)] & ((p . (v ^ <* 0 *>)) `1 ) = [( <*y*> ^ T), x] by A1, Def4;

      ( branchdeg v) = 1 by A1, A2, Def4;

      then (v ^ <* 0 *>) in ( dom p) by Th1;

      hence thesis by A3;

    end;

    theorem :: PRELAMB:6

    ((p . v) `2 ) = 3 implies ex w,u be Element of ( dom p), T, X, Y, x, y, z st w = (v ^ <* 0 *>) & u = (v ^ <*1*>) & ((p . v) `1 ) = [(((X ^ <*(x /" y)*>) ^ T) ^ Y), z] & ((p . w) `1 ) = [T, y] & ((p . u) `1 ) = [((X ^ <*x*>) ^ Y), z]

    proof



       A1: v is correct by Def12;

      assume

       A2: ((p . v) `2 ) = 3;

      then

       A3: ex T, X, Y, x, y, z st ((p . v) `1 ) = [(((X ^ <*(x /" y)*>) ^ T) ^ Y), z] & ((p . (v ^ <* 0 *>)) `1 ) = [T, y] & ((p . (v ^ <*1*>)) `1 ) = [((X ^ <*x*>) ^ Y), z] by A1, Def4;



       A4: ( branchdeg v) = 2 by A1, A2, Def4;

      then

       A5: (v ^ <* 0 *>) in ( dom p) by Th2;

      (v ^ <*1*>) in ( dom p) by A4, Th2;

      hence thesis by A3, A5;

    end;

    theorem :: PRELAMB:7

    ((p . v) `2 ) = 4 implies ex w,u be Element of ( dom p), T, X, Y, x, y, z st w = (v ^ <* 0 *>) & u = (v ^ <*1*>) & ((p . v) `1 ) = [(((X ^ T) ^ <*(y \ x)*>) ^ Y), z] & ((p . w) `1 ) = [T, y] & ((p . u) `1 ) = [((X ^ <*x*>) ^ Y), z]

    proof



       A1: v is correct by Def12;

      assume

       A2: ((p . v) `2 ) = 4;

      then

       A3: ex T, X, Y, x, y, z st ((p . v) `1 ) = [(((X ^ T) ^ <*(y \ x)*>) ^ Y), z] & ((p . (v ^ <* 0 *>)) `1 ) = [T, y] & ((p . (v ^ <*1*>)) `1 ) = [((X ^ <*x*>) ^ Y), z] by A1, Def4;



       A4: ( branchdeg v) = 2 by A1, A2, Def4;

      then

       A5: (v ^ <* 0 *>) in ( dom p) by Th2;

      (v ^ <*1*>) in ( dom p) by A4, Th2;

      hence thesis by A3, A5;

    end;

    theorem :: PRELAMB:8

    ((p . v) `2 ) = 5 implies ex w be Element of ( dom p), X, x, y, Y st w = (v ^ <* 0 *>) & ((p . v) `1 ) = [((X ^ <*(x * y)*>) ^ Y), z] & ((p . w) `1 ) = [(((X ^ <*x*>) ^ <*y*>) ^ Y), z]

    proof



       A1: v is correct by Def12;

      assume

       A2: ((p . v) `2 ) = 5;

      then

       A3: ex X, x, y, Y st ((p . v) `1 ) = [((X ^ <*(x * y)*>) ^ Y), z] & ((p . (v ^ <* 0 *>)) `1 ) = [(((X ^ <*x*>) ^ <*y*>) ^ Y), z] by A1, Def4;

      ( branchdeg v) = 1 by A1, A2, Def4;

      then (v ^ <* 0 *>) in ( dom p) by Th1;

      hence thesis by A3;

    end;

    theorem :: PRELAMB:9

    ((p . v) `2 ) = 6 implies ex w,u be Element of ( dom p), X, Y, x, y st w = (v ^ <* 0 *>) & u = (v ^ <*1*>) & ((p . v) `1 ) = [(X ^ Y), (x * y)] & ((p . w) `1 ) = [X, x] & ((p . u) `1 ) = [Y, y]

    proof



       A1: v is correct by Def12;

      assume

       A2: ((p . v) `2 ) = 6;

      then

       A3: ex X, Y, x, y st ((p . v) `1 ) = [(X ^ Y), (x * y)] & ((p . (v ^ <* 0 *>)) `1 ) = [X, x] & ((p . (v ^ <*1*>)) `1 ) = [Y, y] by A1, Def4;



       A4: ( branchdeg v) = 2 by A1, A2, Def4;

      then

       A5: (v ^ <* 0 *>) in ( dom p) by Th2;

      (v ^ <*1*>) in ( dom p) by A4, Th2;

      hence thesis by A3, A5;

    end;

    theorem :: PRELAMB:10



     Th10: ((p . v) `2 ) = 7 implies ex w,u be Element of ( dom p), T, X, Y, y, z st w = (v ^ <* 0 *>) & u = (v ^ <*1*>) & ((p . v) `1 ) = [((X ^ T) ^ Y), z] & ((p . w) `1 ) = [T, y] & ((p . u) `1 ) = [((X ^ <*y*>) ^ Y), z]

    proof



       A1: v is correct by Def12;

      assume

       A2: ((p . v) `2 ) = 7;

      then

       A3: ex T, X, Y, y, z st ((p . v) `1 ) = [((X ^ T) ^ Y), z] & ((p . (v ^ <* 0 *>)) `1 ) = [T, y] & ((p . (v ^ <*1*>)) `1 ) = [((X ^ <*y*>) ^ Y), z] by A1, Def4;



       A4: ( branchdeg v) = 2 by A1, A2, Def4;

      then

       A5: (v ^ <* 0 *>) in ( dom p) by Th2;

      (v ^ <*1*>) in ( dom p) by A4, Th2;

      hence thesis by A3, A5;

    end;

    theorem :: PRELAMB:11

    ((p . v) `2 ) = 0 or ... or ((p . v) `2 ) = 7

    proof

      v is correct by Def12;

      hence thesis by Def4;

    end;

    definition

      let s;

      let IT be PreProof of s;

      :: PRELAMB:def13

      attr IT is cut-free means for v be Element of ( dom IT) holds ((IT . v) `2 ) <> 7;

    end

    definition

      let s;

      :: PRELAMB:def14

      func size_w.r.t. s -> Function of the carrier of s, NAT means for x holds (it . x) = ( card ( dom ( repr_of x)));

      existence

      proof

        deffunc F( type of s) = ( card ( dom ( repr_of $1)));

        thus ex S be Function of the carrier of s, NAT st for x holds (S . x) = F(x) from FUNCT_2:sch 4;

      end;

      uniqueness

      proof

        let f,g be Function of the carrier of s, NAT ;

        deffunc F( type of s) = ( card ( dom ( repr_of $1)));

        assume that

         A1: (f . x) = F(x) and

         A2: (g . x) = F(x);

        now

          let c be Element of s;



          thus (f . c) = F(c) by A1

          .= (g . c) by A2;

        end;

        hence f = g by FUNCT_2: 63;

      end;

    end

    definition

      let D be non empty set, T be FinSequence of D, f be Function of D, NAT ;

      :: original: *

      redefine

      func f * T -> FinSequence of REAL ;

      coherence

      proof



         A1: (f * T) is FinSequence of NAT by FINSEQ_2: 32;

        ( rng (f * T)) c= REAL ;

        hence thesis by A1, FINSEQ_1:def 4;

      end;

    end



     Lm1: for D be non empty set, T be FinSequence of D holds for f be Function of D, NAT holds ( Sum (f * T)) is Nat

    proof

      let D be non empty set, T be FinSequence of D;

      let f be Function of D, NAT ;

      defpred P[ FinSequence of REAL ] means $1 is FinSequence of NAT implies ( Sum $1) is Nat;



       A1: P[( <*> REAL )] by RVSUM_1: 72;



       A2: for p be FinSequence of REAL , x be Element of REAL st P[p] holds P[(p ^ <*x*>)]

      proof

        let p be FinSequence of REAL , x be Element of REAL ;

        assume

         A3: P[p];

        assume (p ^ <*x*>) is FinSequence of NAT ;

        then

         A4: ( rng (p ^ <*x*>)) c= NAT by FINSEQ_1:def 4;

        ( rng p) c= ( rng (p ^ <*x*>)) by FINSEQ_1: 29;

        then

         A5: ( rng p) c= NAT by A4;

        ( rng <*x*>) c= ( rng (p ^ <*x*>)) by FINSEQ_1: 30;

        then

         A6: ( rng <*x*>) c= NAT by A4;

        ( rng <*x*>) = {x} by FINSEQ_1: 38;

        then

        reconsider n = x as Element of NAT by A6, ZFMISC_1: 31;

        reconsider s = ( Sum p) as Nat by A3, A5, FINSEQ_1:def 4;

        ( Sum (p ^ <*x*>)) = (s + n) by RVSUM_1: 74;

        hence thesis;

      end;



       A7: for p be FinSequence of REAL holds P[p] from FINSEQ_2:sch 2( A1, A2);

      (f * T) is FinSequence of NAT by FINSEQ_2: 32;

      hence thesis by A7;

    end;

    definition

      let s;

      let p be Proof of s;

      :: PRELAMB:def15

      func cutdeg p -> Nat means ex T, X, Y, y, z st ((p . {} ) `1 ) = [((X ^ T) ^ Y), z] & ((p . <* 0 *>) `1 ) = [T, y] & ((p . <*1*>) `1 ) = [((X ^ <*y*>) ^ Y), z] & it = (((( size_w.r.t. s) . y) + (( size_w.r.t. s) . z)) + ( Sum (( size_w.r.t. s) * ((X ^ T) ^ Y)))) if ((p . {} ) `2 ) = 7

      otherwise it = 0 ;

      existence

      proof

        thus ((p . {} ) `2 ) = 7 implies ex r be Nat st ex T, X, Y, y, z st ((p . {} ) `1 ) = [((X ^ T) ^ Y), z] & ((p . <* 0 *>) `1 ) = [T, y] & ((p . <*1*>) `1 ) = [((X ^ <*y*>) ^ Y), z] & r = (((( size_w.r.t. s) . y) + (( size_w.r.t. s) . z)) + ( Sum (( size_w.r.t. s) * ((X ^ T) ^ Y))))

        proof



           A1: ( {} ^ <* 0 *>) = <* 0 *> by FINSEQ_1: 34;



           A2: ( {} ^ <*1*>) = <*1*> by FINSEQ_1: 34;

          reconsider v = {} as Element of ( dom p) by TREES_1: 22;

          assume ((p . {} ) `2 ) = 7;

          then

          consider w,u be Element of ( dom p), T, X, Y, y, z such that

           A3: w = (v ^ <* 0 *>) and

           A4: u = (v ^ <*1*>) and

           A5: ((p . v) `1 ) = [((X ^ T) ^ Y), z] and

           A6: ((p . w) `1 ) = [T, y] and

           A7: ((p . u) `1 ) = [((X ^ <*y*>) ^ Y), z] by Th10;

          reconsider a = ( Sum (( size_w.r.t. s) * ((X ^ T) ^ Y))) as Nat by Lm1;

          reconsider tt = (((( size_w.r.t. s) . y) + (( size_w.r.t. s) . z)) + a) as Nat;

          take tt;

          thus thesis by A1, A2, A3, A4, A5, A6, A7;

        end;

        thus thesis;

      end;

      uniqueness

      proof

        let r1,r2 be Nat;

        thus ((p . {} ) `2 ) = 7 & (ex T, X, Y, y, z st ((p . {} ) `1 ) = [((X ^ T) ^ Y), z] & ((p . <* 0 *>) `1 ) = [T, y] & ((p . <*1*>) `1 ) = [((X ^ <*y*>) ^ Y), z] & r1 = (((( size_w.r.t. s) . y) + (( size_w.r.t. s) . z)) + ( Sum (( size_w.r.t. s) * ((X ^ T) ^ Y))))) & (ex T, X, Y, y, z st ((p . {} ) `1 ) = [((X ^ T) ^ Y), z] & ((p . <* 0 *>) `1 ) = [T, y] & ((p . <*1*>) `1 ) = [((X ^ <*y*>) ^ Y), z] & r2 = (((( size_w.r.t. s) . y) + (( size_w.r.t. s) . z)) + ( Sum (( size_w.r.t. s) * ((X ^ T) ^ Y))))) implies r1 = r2

        proof

          assume ((p . {} ) `2 ) = 7;

          given T, X, Y, y, z such that

           A8: ((p . {} ) `1 ) = [((X ^ T) ^ Y), z] and

           A9: ((p . <* 0 *>) `1 ) = [T, y] and ((p . <*1*>) `1 ) = [((X ^ <*y*>) ^ Y), z] and

           A10: r1 = (((( size_w.r.t. s) . y) + (( size_w.r.t. s) . z)) + ( Sum (( size_w.r.t. s) * ((X ^ T) ^ Y))));

          given T9, X9, Y9, y9, z9 such that

           A11: ((p . {} ) `1 ) = [((X9 ^ T9) ^ Y9), z9] and

           A12: ((p . <* 0 *>) `1 ) = [T9, y9] and ((p . <*1*>) `1 ) = [((X9 ^ <*y9*>) ^ Y9), z9] and

           A13: r2 = (((( size_w.r.t. s) . y9) + (( size_w.r.t. s) . z9)) + ( Sum (( size_w.r.t. s) * ((X9 ^ T9) ^ Y9))));



           A14: ((X ^ T) ^ Y) = ( [((X ^ T) ^ Y), z] `1 )

          .= ( [((X9 ^ T9) ^ Y9), z9] `1 ) by A8, A11

          .= ((X9 ^ T9) ^ Y9);



           A15: y = ( [T, y] `2 )

          .= ( [T9, y9] `2 ) by A9, A12

          .= y9;

          z = ( [((X ^ T) ^ Y), z] `2 )

          .= ( [((X9 ^ T9) ^ Y9), z9] `2 ) by A8, A11

          .= z9;

          hence thesis by A10, A13, A14, A15;

        end;

        thus thesis;

      end;

      consistency ;

    end

    reserve A for non empty set,

a,a1,a2,b for Element of (A * );

    definition

      let s, A;

      :: PRELAMB:def16

      mode Model of s,A -> Function of the carrier of s, ( bool (A * )) means for x, y holds (it . (x * y)) = { (a ^ b) : a in (it . x) & b in (it . y) } & (it . (x /" y)) = { a1 : for b st b in (it . y) holds (a1 ^ b) in (it . x) } & (it . (y \ x)) = { a2 : for b st b in (it . y) holds (b ^ a2) in (it . x) };

      existence

      proof

         {} in (A * ) by FINSEQ_1: 49;

        then { {} } c= (A * ) by ZFMISC_1: 31;

        then

        reconsider f = (the carrier of s --> { {} }) as Function of the carrier of s, ( bool (A * )) by FUNCOP_1: 45;



         A1: for t be set st t in (f . x) holds t = {}

        proof

          let t be set;

          assume t in (f . x);

          then t in { {} } by FUNCOP_1: 7;

          hence thesis by TARSKI:def 1;

        end;



         A2: {} in (f . x)

        proof

          (f . x) = { {} } by FUNCOP_1: 7;

          hence thesis by TARSKI:def 1;

        end;



         A3: {} is Element of (A * ) by FINSEQ_1: 49;

        take f;

        let x, y;

        thus (f . (x * y)) = { (a ^ b) : a in (f . x) & b in (f . y) }

        proof

          thus (f . (x * y)) c= { (a ^ b) : a in (f . x) & b in (f . y) }

          proof

            let t be object;

            assume t in (f . (x * y));

            then

             A4: t = {} by A1;



             A5: t = ( {} ^ {} ) by A4;



             A6: {} in (f . x) by A2;

             {} in (f . y) by A2;

            hence thesis by A5, A6;

          end;

          let t be object;

          assume t in { (a ^ b) : a in (f . x) & b in (f . y) };

          then

          consider a, b such that

           A7: t = (a ^ b) and

           A8: a in (f . x) and

           A9: b in (f . y);



           A10: a = {} by A1, A8;

          b = {} by A1, A9;

          then (a ^ b) = {} by A10, FINSEQ_1: 34;

          hence thesis by A2, A7;

        end;

        thus (f . (x /" y)) = { a : for b st b in (f . y) holds (a ^ b) in (f . x) }

        proof

          thus (f . (x /" y)) c= { a : for b st b in (f . y) holds (a ^ b) in (f . x) }

          proof

            let t be object;

            assume t in (f . (x /" y));

            then

             A11: t = {} by A1;

            now

              let b;

              assume b in (f . y);

              then b = {} by A1;

              then ( {} ^ b) = {} by FINSEQ_1: 34;

              hence ( {} ^ b) in (f . x) by A2;

            end;

            hence thesis by A3, A11;

          end;

          let t be object;

          assume t in { a : for b st b in (f . y) holds (a ^ b) in (f . x) };

          then

          consider a such that

           A12: t = a and

           A13: for b st b in (f . y) holds (a ^ b) in (f . x);

           {} in (f . y) by A2;

          then (a ^ {} ) in (f . x) by A13;

          then a = {} by A1;

          hence thesis by A2, A12;

        end;

        thus (f . (y \ x)) = { a : for b st b in (f . y) holds (b ^ a) in (f . x) }

        proof

          thus (f . (y \ x)) c= { a : for b st b in (f . y) holds (b ^ a) in (f . x) }

          proof

            let t be object;

            assume t in (f . (y \ x));

            then

             A14: t = {} by A1;

            now

              let b;

              assume b in (f . y);

              then b = {} by A1;

              then (b ^ {} ) = {} by FINSEQ_1: 34;

              hence (b ^ {} ) in (f . x) by A2;

            end;

            hence thesis by A3, A14;

          end;

          let t be object;

          assume t in { a : for b st b in (f . y) holds (b ^ a) in (f . x) };

          then

          consider a such that

           A15: t = a and

           A16: for b st b in (f . y) holds (b ^ a) in (f . x);

           {} in (f . y) by A2;

          then ( {} ^ a) in (f . x) by A16;

          then a = {} by A1;

          hence thesis by A2, A15;

        end;

      end;

    end

    definition

      struct ( typealg) typestr (# the carrier -> set,

the left_quotient, right_quotient, inner_product -> BinOp of the carrier,

the derivability -> Relation of ( the carrier * ), the carrier #)

       attr strict strict;

    end

    registration

      cluster non empty strict for typestr;

      existence

      proof

        set l = the BinOp of { {} }, d = the Relation of ( { {} } * ), { {} };

        take typestr (# { {} }, l, l, l, d #);

        thus the carrier of typestr (# { {} }, l, l, l, d #) is non empty;

        thus thesis;

      end;

    end

    reserve s for non empty typestr,

x for type of s;

    definition

      let s;

      let f be FinSequence of s, x;

      :: PRELAMB:def17

      pred f ==>. x means [f, x] in the derivability of s;

    end

    definition

      let IT be non empty typestr;

      :: PRELAMB:def18

      attr IT is SynTypes_Calculus-like means

      : Def18: (for x be type of IT holds <*x*> ==>. x) & (for T be FinSequence of IT, x,y be type of IT st (T ^ <*y*>) ==>. x holds T ==>. (x /" y)) & (for T be FinSequence of IT, x,y be type of IT st ( <*y*> ^ T) ==>. x holds T ==>. (y \ x)) & (for T,X,Y be FinSequence of IT, x,y,z be type of IT st T ==>. y & ((X ^ <*x*>) ^ Y) ==>. z holds (((X ^ <*(x /" y)*>) ^ T) ^ Y) ==>. z) & (for T,X,Y be FinSequence of IT, x,y,z be type of IT st T ==>. y & ((X ^ <*x*>) ^ Y) ==>. z holds (((X ^ T) ^ <*(y \ x)*>) ^ Y) ==>. z) & (for X,Y be FinSequence of IT, x,y,z be type of IT st (((X ^ <*x*>) ^ <*y*>) ^ Y) ==>. z holds ((X ^ <*(x * y)*>) ^ Y) ==>. z) & for X,Y be FinSequence of IT, x,y be type of IT st X ==>. x & Y ==>. y holds (X ^ Y) ==>. (x * y);

    end

    registration

      cluster SynTypes_Calculus-like for non empty typestr;

      existence

      proof

         [:( { 0 } * ), { 0 }:] c= [:( { 0 } * ), { 0 }:];

        then

        reconsider DER = [:( { 0 } * ), { 0 }:] as non empty Relation of ( { 0 } * ), { 0 };

        reconsider EM = typestr (# { 0 }, op2 , op2 , op2 , DER #) as non empty typestr;

        take EM;

        thus for x be type of EM holds <*x*> ==>. x;

        thus thesis;

      end;

    end

    definition

      mode SynTypes_Calculus is SynTypes_Calculus-like non empty typestr;

    end

    reserve s for SynTypes_Calculus,

T,X,Y for FinSequence of s,

x,y,z for type of s;

    deffunc e( typestr) = ( <*> the carrier of $1);



     Lm2: T ==>. y & (X ^ <*x*>) ==>. z implies ((X ^ <*(x /" y)*>) ^ T) ==>. z

    proof

      assume that

       A1: T ==>. y and

       A2: (X ^ <*x*>) ==>. z;

      ((X ^ <*x*>) ^ e(s)) ==>. z by A2, FINSEQ_1: 34;

      then (((X ^ <*(x /" y)*>) ^ T) ^ e(s)) ==>. z by A1, Def18;

      hence thesis by FINSEQ_1: 34;

    end;



     Lm3: T ==>. y & ( <*x*> ^ Y) ==>. z implies (( <*(x /" y)*> ^ T) ^ Y) ==>. z

    proof

      assume that

       A1: T ==>. y and

       A2: ( <*x*> ^ Y) ==>. z;

      (( e(s) ^ <*x*>) ^ Y) ==>. z by A2, FINSEQ_1: 34;

      then ((( e(s) ^ <*(x /" y)*>) ^ T) ^ Y) ==>. z by A1, Def18;

      hence thesis by FINSEQ_1: 34;

    end;



     Lm4: T ==>. y & <*x*> ==>. z implies ( <*(x /" y)*> ^ T) ==>. z

    proof

      assume that

       A1: T ==>. y and

       A2: <*x*> ==>. z;

      ( e(s) ^ <*x*>) ==>. z by A2, FINSEQ_1: 34;

      then (( e(s) ^ <*(x /" y)*>) ^ T) ==>. z by A1, Lm2;

      hence thesis by FINSEQ_1: 34;

    end;



     Lm5: T ==>. y & (X ^ <*x*>) ==>. z implies ((X ^ T) ^ <*(y \ x)*>) ==>. z

    proof

      assume that

       A1: T ==>. y and

       A2: (X ^ <*x*>) ==>. z;

      ((X ^ <*x*>) ^ e(s)) ==>. z by A2, FINSEQ_1: 34;

      then (((X ^ T) ^ <*(y \ x)*>) ^ e(s)) ==>. z by A1, Def18;

      hence thesis by FINSEQ_1: 34;

    end;



     Lm6: T ==>. y & ( <*x*> ^ Y) ==>. z implies ((T ^ <*(y \ x)*>) ^ Y) ==>. z

    proof

      assume that

       A1: T ==>. y and

       A2: ( <*x*> ^ Y) ==>. z;

      (( e(s) ^ <*x*>) ^ Y) ==>. z by A2, FINSEQ_1: 34;

      then ((( e(s) ^ T) ^ <*(y \ x)*>) ^ Y) ==>. z by A1, Def18;

      hence thesis by FINSEQ_1: 34;

    end;



     Lm7: T ==>. y & <*x*> ==>. z implies (T ^ <*(y \ x)*>) ==>. z

    proof

      assume that

       A1: T ==>. y and

       A2: <*x*> ==>. z;

      ( e(s) ^ <*x*>) ==>. z by A2, FINSEQ_1: 34;

      then (( e(s) ^ T) ^ <*(y \ x)*>) ==>. z by A1, Lm5;

      hence thesis by FINSEQ_1: 34;

    end;



     Lm8: (( <*x*> ^ <*y*>) ^ Y) ==>. z implies ( <*(x * y)*> ^ Y) ==>. z

    proof

      assume (( <*x*> ^ <*y*>) ^ Y) ==>. z;

      then ((( e(s) ^ <*x*>) ^ <*y*>) ^ Y) ==>. z by FINSEQ_1: 34;

      then (( e(s) ^ <*(x * y)*>) ^ Y) ==>. z by Def18;

      hence thesis by FINSEQ_1: 34;

    end;



     Lm9: ((X ^ <*x*>) ^ <*y*>) ==>. z implies (X ^ <*(x * y)*>) ==>. z

    proof

      assume ((X ^ <*x*>) ^ <*y*>) ==>. z;

      then (((X ^ <*x*>) ^ <*y*>) ^ e(s)) ==>. z by FINSEQ_1: 34;

      then ((X ^ <*(x * y)*>) ^ e(s)) ==>. z by Def18;

      hence thesis by FINSEQ_1: 34;

    end;



     Lm10: ( <*x*> ^ <*y*>) ==>. z implies <*(x * y)*> ==>. z

    proof

      assume ( <*x*> ^ <*y*>) ==>. z;

      then (( e(s) ^ <*x*>) ^ <*y*>) ==>. z by FINSEQ_1: 34;

      then ( e(s) ^ <*(x * y)*>) ==>. z by Lm9;

      hence thesis by FINSEQ_1: 34;

    end;

    theorem :: PRELAMB:12



     Th12: ( <*(x /" y)*> ^ <*y*>) ==>. x & ( <*y*> ^ <*(y \ x)*>) ==>. x

    proof



       A1: <*x*> ==>. x by Def18;

       <*y*> ==>. y by Def18;

      hence thesis by A1, Lm4, Lm7;

    end;

    theorem :: PRELAMB:13



     Th13: <*x*> ==>. (y /" (x \ y)) & <*x*> ==>. ((y /" x) \ y)

    proof



       A1: ( <*(y /" x)*> ^ <*x*>) ==>. y by Th12;

      ( <*x*> ^ <*(x \ y)*>) ==>. y by Th12;

      hence thesis by A1, Def18;

    end;

    theorem :: PRELAMB:14



     Th14: <*(x /" y)*> ==>. ((x /" z) /" (y /" z))

    proof



       A1: ( <*(x /" y)*> ^ <*y*>) ==>. x by Th12;

       <*z*> ==>. z by Def18;

      then (( <*(x /" y)*> ^ <*(y /" z)*>) ^ <*z*>) ==>. x by A1, Lm2;

      then ( <*(x /" y)*> ^ <*(y /" z)*>) ==>. (x /" z) by Def18;

      hence thesis by Def18;

    end;

    theorem :: PRELAMB:15



     Th15: <*(y \ x)*> ==>. ((z \ y) \ (z \ x))

    proof



       A1: ( <*y*> ^ <*(y \ x)*>) ==>. x by Th12;

       <*z*> ==>. z by Def18;

      then (( <*z*> ^ <*(z \ y)*>) ^ <*(y \ x)*>) ==>. x by A1, Lm6;

      then ( <*z*> ^ ( <*(z \ y)*> ^ <*(y \ x)*>)) ==>. x by FINSEQ_1: 32;

      then ( <*(z \ y)*> ^ <*(y \ x)*>) ==>. (z \ x) by Def18;

      hence thesis by Def18;

    end;

    theorem :: PRELAMB:16

     <*x*> ==>. y implies <*(x /" z)*> ==>. (y /" z) & <*(z \ x)*> ==>. (z \ y)

    proof

      assume

       A1: <*x*> ==>. y;



       A2: <*z*> ==>. z by Def18;

      then

       A3: ( <*(x /" z)*> ^ <*z*>) ==>. y by A1, Lm4;

      ( <*z*> ^ <*(z \ x)*>) ==>. y by A1, A2, Lm7;

      hence thesis by A3, Def18;

    end;

    theorem :: PRELAMB:17



     Th17: <*x*> ==>. y implies <*(z /" y)*> ==>. (z /" x) & <*(y \ z)*> ==>. (x \ z)

    proof

      assume

       A1: <*x*> ==>. y;



       A2: <*z*> ==>. z by Def18;

      then

       A3: ( <*(z /" y)*> ^ <*x*>) ==>. z by A1, Lm4;

      ( <*x*> ^ <*(y \ z)*>) ==>. z by A1, A2, Lm7;

      hence thesis by A3, Def18;

    end;

    theorem :: PRELAMB:18



     Th18: <*(y /" ((y /" x) \ y))*> ==>. (y /" x)

    proof

       <*x*> ==>. ((y /" x) \ y) by Th13;

      hence thesis by Th17;

    end;

    theorem :: PRELAMB:19



     Th19: <*x*> ==>. y implies ( <*> the carrier of s) ==>. (y /" x) & ( <*> the carrier of s) ==>. (x \ y)

    proof

      assume

       A1: <*x*> ==>. y;



       A2: ( e(s) ^ <*x*>) = <*x*> by FINSEQ_1: 34;

      ( <*x*> ^ e(s)) = <*x*> by FINSEQ_1: 34;

      hence thesis by A1, A2, Def18;

    end;

    theorem :: PRELAMB:20



     Th20: ( <*> the carrier of s) ==>. (x /" x) & ( <*> the carrier of s) ==>. (x \ x)

    proof

       <*x*> ==>. x by Def18;

      hence thesis by Th19;

    end;

    theorem :: PRELAMB:21

    ( <*> the carrier of s) ==>. ((y /" (x \ y)) /" x) & ( <*> the carrier of s) ==>. (x \ ((y /" x) \ y))

    proof



       A1: <*x*> ==>. (y /" (x \ y)) by Th13;

       <*x*> ==>. ((y /" x) \ y) by Th13;

      hence thesis by A1, Th19;

    end;

    theorem :: PRELAMB:22

    ( <*> the carrier of s) ==>. (((x /" z) /" (y /" z)) /" (x /" y)) & ( <*> the carrier of s) ==>. ((y \ x) \ ((z \ y) \ (z \ x)))

    proof



       A1: <*(x /" y)*> ==>. ((x /" z) /" (y /" z)) by Th14;

       <*(y \ x)*> ==>. ((z \ y) \ (z \ x)) by Th15;

      hence thesis by A1, Th19;

    end;

    theorem :: PRELAMB:23

    ( <*> the carrier of s) ==>. x implies ( <*> the carrier of s) ==>. (y /" (y /" x)) & ( <*> the carrier of s) ==>. ((x \ y) \ y)

    proof



       A1: <*y*> ==>. y by Def18;

      then

       A2: ( e(s) ^ <*y*>) ==>. y by FINSEQ_1: 34;



       A3: ( <*y*> ^ e(s)) ==>. y by A1, FINSEQ_1: 34;

      assume

       A4: e(s) ==>. x;

      then

       A5: (( e(s) ^ <*(y /" x)*>) ^ e(s)) ==>. y by A2, Lm2;



       A6: (( e(s) ^ <*(x \ y)*>) ^ e(s)) ==>. y by A3, A4, Lm6;



       A7: ( e(s) ^ <*(y /" x)*>) ==>. y by A5, FINSEQ_1: 34;

      ( <*(x \ y)*> ^ e(s)) ==>. y by A6, FINSEQ_1: 34;

      hence thesis by A7, Def18;

    end;

    theorem :: PRELAMB:24

     <*(x /" (y /" y))*> ==>. x

    proof

       <*x*> ==>. x by Def18;

      then ( <*(x /" (y /" y))*> ^ e(s)) ==>. x by Lm4, Th20;

      hence thesis by FINSEQ_1: 34;

    end;

    definition

      let s, x, y;

      :: PRELAMB:def19

      pred x <==>. y means <*x*> ==>. y & <*y*> ==>. x;

      reflexivity by Def18;

      symmetry ;

    end

    theorem :: PRELAMB:25

    (x /" y) <==>. (x /" ((x /" y) \ x)) by Th13, Th18;

    theorem :: PRELAMB:26

    (x /" (z * y)) <==>. ((x /" y) /" z)

    proof



       A1: <*z*> ==>. z by Def18;



       A2: <*y*> ==>. y by Def18;



       A3: <*x*> ==>. x by Def18;

      ( <*z*> ^ <*y*>) ==>. (z * y) by A1, A2, Def18;

      then ( <*(x /" (z * y))*> ^ ( <*z*> ^ <*y*>)) ==>. x by A3, Lm4;

      then (( <*(x /" (z * y))*> ^ <*z*>) ^ <*y*>) ==>. x by FINSEQ_1: 32;

      then ( <*(x /" (z * y))*> ^ <*z*>) ==>. (x /" y) by Def18;

      then

       A4: <*(x /" (z * y))*> ==>. ((x /" y) /" z) by Def18;

      ( <*(x /" y)*> ^ <*y*>) ==>. x by A2, A3, Lm4;

      then (( <*((x /" y) /" z)*> ^ <*z*>) ^ <*y*>) ==>. x by A1, Lm3;

      then ( <*((x /" y) /" z)*> ^ <*(z * y)*>) ==>. x by Lm9;

      then <*((x /" y) /" z)*> ==>. (x /" (z * y)) by Def18;

      hence thesis by A4;

    end;

    theorem :: PRELAMB:27

     <*(x * (y /" z))*> ==>. ((x * y) /" z)

    proof



       A1: <*x*> ==>. x by Def18;

       <*y*> ==>. y by Def18;

      then

       A2: ( <*x*> ^ <*y*>) ==>. (x * y) by A1, Def18;

       <*z*> ==>. z by Def18;

      then (( <*x*> ^ <*(y /" z)*>) ^ <*z*>) ==>. (x * y) by A2, Lm2;

      then ( <*(x * (y /" z))*> ^ <*z*>) ==>. (x * y) by Lm8;

      hence thesis by Def18;

    end;

    theorem :: PRELAMB:28

     <*x*> ==>. ((x * y) /" y) & <*x*> ==>. (y \ (y * x))

    proof



       A1: <*x*> ==>. x by Def18;



       A2: <*y*> ==>. y by Def18;

      then

       A3: ( <*x*> ^ <*y*>) ==>. (x * y) by A1, Def18;

      ( <*y*> ^ <*x*>) ==>. (y * x) by A1, A2, Def18;

      hence thesis by A3, Def18;

    end;

    theorem :: PRELAMB:29

    ((x * y) * z) <==>. (x * (y * z))

    proof



       A1: <*x*> ==>. x by Def18;



       A2: <*y*> ==>. y by Def18;



       A3: <*z*> ==>. z by Def18;

      ( <*x*> ^ <*y*>) ==>. (x * y) by A1, A2, Def18;

      then (( <*x*> ^ <*y*>) ^ <*z*>) ==>. ((x * y) * z) by A3, Def18;

      then ( <*x*> ^ <*(y * z)*>) ==>. ((x * y) * z) by Lm9;

      then

       A4: <*(x * (y * z))*> ==>. ((x * y) * z) by Lm10;

      ( <*y*> ^ <*z*>) ==>. (y * z) by A2, A3, Def18;

      then ( <*x*> ^ ( <*y*> ^ <*z*>)) ==>. (x * (y * z)) by A1, Def18;

      then (( <*x*> ^ <*y*>) ^ <*z*>) ==>. (x * (y * z)) by FINSEQ_1: 32;

      then ( <*(x * y)*> ^ <*z*>) ==>. (x * (y * z)) by Lm8;

      then <*((x * y) * z)*> ==>. (x * (y * z)) by Lm10;

      hence thesis by A4;

    end;