abcmiz_0.miz



    begin

    registration

      cluster reflexive -> complete for 1 -element RelStr;

      coherence ;

    end

    definition

      let T be RelStr;

      mode type of T is Element of T;

    end

    definition

      let T be RelStr;

      :: ABCMIZ_0:def1

      attr T is Noetherian means

      : Def1: the InternalRel of T is co-well_founded;

    end

    registration

      cluster -> Noetherian for 1 -element RelStr;

      coherence

      proof

        let S be 1 -element RelStr;

        let Y be set;

        set R = the InternalRel of S;

        assume

         A1: Y c= ( field R);

        assume Y <> {} ;

        then

        reconsider X = Y as non empty set;

        set a = the Element of X;

        take a;

        thus a in Y;

        

         A2: a in ( field R) by A1;

        let b be object;

        

         A3: ( field R) c= (the carrier of S \/ the carrier of S) by RELSET_1: 8;

        assume b in Y;

        then b in ( field R) by A1;

        hence thesis by A2, A3, ZFMISC_1:def 10;

      end;

    end

    definition

      let T be non empty RelStr;

      :: original: Noetherian

      redefine

      :: ABCMIZ_0:def2

      attr T is Noetherian means

      : Def2: for A be non empty Subset of T holds ex a be Element of T st a in A & for b be Element of T st b in A holds not a < b;

      compatibility

      proof

        set R = the InternalRel of T;

        thus T is Noetherian implies for A be non empty Subset of T holds ex a be Element of T st a in A & for b be Element of T st b in A holds not a < b

        proof

          assume

           A1: for Y be set st Y c= ( field R) & Y <> {} holds ex a be object st a in Y & for b be object st b in Y & a <> b holds not [a, b] in R;

          let A be non empty Subset of T;

          set a = the Element of A;

          reconsider a as Element of T;

          set Y = (A /\ ( field R));

          per cases ;

            suppose

             A2: A misses ( field R);

            take a;

            thus a in A;

            let b be Element of T;

            assume that b in A and

             A3: a < b;

            a <= b by A3, ORDERS_2:def 6;

            then [a, b] in R by ORDERS_2:def 5;

            then a in ( field R) by RELAT_1: 15;

            hence contradiction by A2, XBOOLE_0: 3;

          end;

            suppose A meets ( field R);

            then Y <> {} ;

            then

            consider x be object such that

             A4: x in Y and

             A5: for y be object st y in Y & x <> y holds not [x, y] in R by A1, XBOOLE_1: 17;

            reconsider x as Element of T by A4;

            take x;

            thus x in A by A4, XBOOLE_0:def 4;

            let b be Element of T;

            assume that

             A6: b in A and

             A7: x < b;

            x <= b by A7, ORDERS_2:def 6;

            then

             A8: [x, b] in R by ORDERS_2:def 5;

            then b in ( field R) by RELAT_1: 15;

            then b in Y by A6, XBOOLE_0:def 4;

            hence contradiction by A5, A7, A8;

          end;

        end;

        assume

         A9: for A be non empty Subset of T holds ex a be Element of T st a in A & for b be Element of T st b in A holds not a < b;

        let Y be set;

        assume that

         A10: Y c= ( field R) and

         A11: Y <> {} ;

        ( field R) c= (the carrier of T \/ the carrier of T) by RELSET_1: 8;

        then

        reconsider A = Y as non empty Subset of T by A10, A11, XBOOLE_1: 1;

        consider a be Element of T such that

         A12: a in A and

         A13: for b be Element of T st b in A holds not a < b by A9;

        take a;

        thus a in Y by A12;

        let b be object;

        assume that

         A14: b in Y and

         A15: a <> b;

        b in A by A14;

        then

        reconsider b as Element of T;

         not a < b by A13, A14;

        then not a <= b by A15, ORDERS_2:def 6;

        hence thesis by ORDERS_2:def 5;

      end;

    end

    definition

      let T be Poset;

      :: ABCMIZ_0:def3

      attr T is Mizar-widening-like means T is sup-Semilattice & T is Noetherian;

    end

    registration

      cluster Mizar-widening-like -> Noetherian with_suprema upper-bounded for Poset;

      coherence

      proof

        let T be Poset;

        assume that

         A1: T is sup-Semilattice and

         A2: T is Noetherian;

        reconsider S = T as sup-Semilattice by A1;

        the carrier of S c= the carrier of S;

        then

        consider a be Element of T such that a in the carrier of T and

         A3: for b be Element of T st b in the carrier of T holds not a < b by A2, Def2;

        thus T is Noetherian with_suprema by A1, A2;

        take a;

        let b be Element of T;

        

         A4: (a "\/" b) in the carrier of S;

        then

         A5: (a "\/" b) >= a by YELLOW_0: 22;

         not a < (a "\/" b) by A3, A4;

        then (a "\/" b) = a by A5, ORDERS_2:def 6;

        hence thesis by A1, YELLOW_0: 22;

      end;

    end

    registration

      cluster Noetherian -> Mizar-widening-like for sup-Semilattice;

      coherence ;

    end

    registration

      cluster Mizar-widening-like for complete sup-Semilattice;

      existence

      proof

        set T = the 1 -element LATTICE;

        take T;

        thus T is sup-Semilattice;

        thus thesis;

      end;

    end

    registration

      let T be Noetherian RelStr;

      cluster the InternalRel of T -> co-well_founded;

      coherence by Def1;

    end

    theorem :: ABCMIZ_0:1

    

     Th1: for T be Noetherian sup-Semilattice holds for I be Ideal of T holds ex_sup_of (I,T) & ( sup I) in I

    proof

      let T be Noetherian sup-Semilattice;

      let I be Ideal of T;

      consider a be Element of T such that

       A1: a in I and

       A2: for b be Element of T st b in I holds not a < b by Def2;

      

       A3: I is_<=_than a

      proof

        let d be Element of T;

        assume d in I;

        then (a "\/" d) in I by A1, WAYBEL_0: 40;

        then

         A4: not a < (a "\/" d) by A2;

        a <= (a "\/" d) by YELLOW_0: 22;

        then a = (a "\/" d) by A4, ORDERS_2:def 6;

        hence thesis by YELLOW_0: 22;

      end;

      for c be Element of T st I is_<=_than c holds a <= c by A1;

      hence thesis by A1, A3, YELLOW_0: 30;

    end;

    begin

    definition

      struct AdjectiveStr (# the adjectives -> set,

the non-op -> UnOp of the adjectives #)

       attr strict strict;

    end

    definition

      let A be AdjectiveStr;

      :: ABCMIZ_0:def4

      attr A is void means

      : Def4: the adjectives of A is empty;

      mode adjective of A is Element of the adjectives of A;

    end

    theorem :: ABCMIZ_0:2

    for A1,A2 be AdjectiveStr st the adjectives of A1 = the adjectives of A2 holds A1 is void implies A2 is void;

    definition

      let A be AdjectiveStr;

      let a be Element of the adjectives of A;

      :: ABCMIZ_0:def5

      func non- a -> adjective of A equals (the non-op of A . a);

      coherence

      proof

        per cases ;

          suppose

           A1: the adjectives of A is empty;

          then

           A2: ( dom the non-op of A) = the adjectives of A;

          a = {} by A1, SUBSET_1:def 1;

          hence thesis by A1, A2, FUNCT_1:def 2;

        end;

          suppose the adjectives of A is non empty;

          hence thesis by FUNCT_2: 5;

        end;

      end;

    end

    theorem :: ABCMIZ_0:3

    for A1,A2 be AdjectiveStr st the AdjectiveStr of A1 = the AdjectiveStr of A2 holds for a1 be adjective of A1, a2 be adjective of A2 st a1 = a2 holds ( non- a1) = ( non- a2);

    definition

      let A be AdjectiveStr;

      :: ABCMIZ_0:def6

      attr A is involutive means

      : Def6: for a be adjective of A holds ( non- ( non- a)) = a;

      :: ABCMIZ_0:def7

      attr A is without_fixpoints means not ex a be adjective of A st ( non- a) = a;

    end

    theorem :: ABCMIZ_0:4

    

     Th4: for a1,a2 be set st a1 <> a2 holds for A be AdjectiveStr st the adjectives of A = {a1, a2} & (the non-op of A . a1) = a2 & (the non-op of A . a2) = a1 holds A is non void involutive without_fixpoints

    proof

      let a1,a2 be set such that

       A1: a1 <> a2;

      let A be AdjectiveStr such that

       A2: the adjectives of A = {a1, a2} and

       A3: (the non-op of A . a1) = a2 and

       A4: (the non-op of A . a2) = a1;

      thus the adjectives of A is non empty by A2;

      hereby

        let a be adjective of A;

        a = a1 or a = a2 by A2, TARSKI:def 2;

        hence ( non- ( non- a)) = a by A3, A4;

      end;

      let a be adjective of A;

      assume

       A5: ( non- a) = a;

      a = a1 or a = a2 by A2, TARSKI:def 2;

      hence thesis by A1, A3, A4, A5;

    end;

    theorem :: ABCMIZ_0:5

    

     Th5: for A1,A2 be AdjectiveStr st the AdjectiveStr of A1 = the AdjectiveStr of A2 holds A1 is involutive implies A2 is involutive

    proof

      let A1,A2 be AdjectiveStr such that

       A1: the AdjectiveStr of A1 = the AdjectiveStr of A2;

      assume

       A2: for a be adjective of A1 holds ( non- ( non- a)) = a;

      let a be adjective of A2;

      reconsider b = a as adjective of A1 by A1;

      

      thus ( non- ( non- a)) = ( non- ( non- b)) by A1

      .= a by A2;

    end;

    theorem :: ABCMIZ_0:6

    

     Th6: for A1,A2 be AdjectiveStr st the AdjectiveStr of A1 = the AdjectiveStr of A2 holds A1 is without_fixpoints implies A2 is without_fixpoints

    proof

      let A1,A2 be AdjectiveStr such that

       A1: the AdjectiveStr of A1 = the AdjectiveStr of A2;

      assume

       A2: not ex a be adjective of A1 st ( non- a) = a;

      given a be adjective of A2 such that

       A3: ( non- a) = a;

      reconsider b = a as adjective of A1 by A1;

      ( non- b) = b by A1, A3;

      hence contradiction by A2;

    end;

    registration

      cluster non void involutive without_fixpoints for strict AdjectiveStr;

      existence

      proof

        reconsider x = 0 , y = 1 as Element of { 0 , 1} by TARSKI:def 2;

        reconsider n = (( 0 ,1) --> (y,x)) as UnOp of { 0 , 1};

        take AdjectiveStr (# { 0 , 1}, n #);

        

         A1: (n . y) = x by FUNCT_4: 63;

        (n . x) = y by FUNCT_4: 63;

        hence thesis by A1, Th4;

      end;

    end

    registration

      let A be non void AdjectiveStr;

      cluster the adjectives of A -> non empty;

      coherence by Def4;

    end

    definition

      struct ( RelStr, AdjectiveStr) TA-structure (# the carrier, adjectives -> set,

the InternalRel -> Relation of the carrier,

the non-op -> UnOp of the adjectives,

the adj-map -> Function of the carrier, ( Fin the adjectives) #)

       attr strict strict;

    end

    registration

      let X be non empty set;

      let A be set;

      let r be Relation of X;

      let n be UnOp of A;

      let a be Function of X, ( Fin A);

      cluster TA-structure (# X, A, r, n, a #) -> non empty;

      coherence ;

    end

    registration

      let X be set;

      let A be non empty set;

      let r be Relation of X;

      let n be UnOp of A;

      let a be Function of X, ( Fin A);

      cluster TA-structure (# X, A, r, n, a #) -> non void;

      coherence ;

    end

    registration

      cluster 1 -element reflexive non void involutive without_fixpoints strict for TA-structure;

      existence

      proof

        set R = the reflexive1 -element RelStr, A = the non void involutive without_fixpoints AdjectiveStr, f = the Function of the carrier of R, ( Fin the adjectives of A);

        take T = TA-structure (# the carrier of R, the adjectives of A, the InternalRel of R, the non-op of A, f #);

        thus T is 1 -element by STRUCT_0:def 19;

         the RelStr of R = the RelStr of T;

        hence T is reflexive by WAYBEL_8: 12;

        thus T is non void;

         the AdjectiveStr of A = the AdjectiveStr of T;

        hence T is involutive without_fixpoints by Th5, Th6;

        thus thesis;

      end;

    end

    definition

      let T be TA-structure;

      let t be Element of T;

      :: ABCMIZ_0:def8

      func adjs t -> Subset of the adjectives of T equals (the adj-map of T . t);

      coherence

      proof

        per cases ;

          suppose

           A1: the carrier of T is empty;

          then ( dom the adj-map of T) = the carrier of T;

          then (the adj-map of T . t) = ( {} the adjectives of T) by A1, FUNCT_1:def 2;

          hence thesis;

        end;

          suppose the carrier of T is non empty;

          then (the adj-map of T . t) in ( Fin the adjectives of T) by FUNCT_2: 5;

          hence thesis by FINSUB_1: 16;

        end;

      end;

    end

    theorem :: ABCMIZ_0:7

    for T1,T2 be TA-structure st the TA-structure of T1 = the TA-structure of T2 holds for t1 be type of T1, t2 be type of T2 st t1 = t2 holds ( adjs t1) = ( adjs t2);

    definition

      let T be TA-structure;

      :: ABCMIZ_0:def9

      attr T is consistent means

      : Def9: for t be type of T holds for a be adjective of T st a in ( adjs t) holds not ( non- a) in ( adjs t);

    end

    theorem :: ABCMIZ_0:8

    

     Th8: for T1,T2 be TA-structure st the TA-structure of T1 = the TA-structure of T2 holds T1 is consistent implies T2 is consistent

    proof

      let T1,T2 be TA-structure such that

       A1: the TA-structure of T1 = the TA-structure of T2 and

       A2: for t be type of T1 holds for a be adjective of T1 st a in ( adjs t) holds not ( non- a) in ( adjs t);

      let t2 be type of T2, a2 be adjective of T2;

      reconsider a1 = a2 as adjective of T1 by A1;

      reconsider t1 = t2 as type of T1 by A1;

      assume a2 in ( adjs t2);

      then not ( non- a1) in ( adjs t1) by A1, A2;

      hence thesis by A1;

    end;

    definition

      let T be non empty TA-structure;

      :: ABCMIZ_0:def10

      attr T is adj-structured means the adj-map of T is join-preserving Function of T, (( BoolePoset the adjectives of T) opp );

    end

    theorem :: ABCMIZ_0:9

    

     Th9: for T1,T2 be non empty TA-structure st the TA-structure of T1 = the TA-structure of T2 holds T1 is adj-structured implies T2 is adj-structured

    proof

      let T1,T2 be non empty TA-structure such that

       A1: the TA-structure of T1 = the TA-structure of T2;

      assume the adj-map of T1 is join-preserving Function of T1, (( BoolePoset the adjectives of T1) opp );

      then

      reconsider f = the adj-map of T1 as join-preserving Function of T1, (( BoolePoset the adjectives of T1) opp );

      reconsider g = f as Function of T2, (( BoolePoset the adjectives of T2) opp ) by A1;

      

       A2: the RelStr of T1 = the RelStr of T2 by A1;

      g is join-preserving

      proof

        let x,y be type of T2;

        reconsider x9 = x, y9 = y as type of T1 by A1;

        assume

         A3: ex_sup_of ( {x, y},T2);

        then

         A4: ex_sup_of ( {x9, y9},T1) by A2, YELLOW_0: 14;

        

         A5: f preserves_sup_of {x9, y9} by WAYBEL_0:def 35;

        hence ex_sup_of ((g .: {x, y}),(( BoolePoset the adjectives of T2) opp )) by A1, A4;

        ( sup (f .: {x9, y9})) = (f . ( sup {x9, y9})) by A4, A5;

        hence thesis by A1, A2, A3, YELLOW_0: 26;

      end;

      hence the adj-map of T2 is join-preserving Function of T2, (( BoolePoset the adjectives of T2) opp ) by A1;

    end;

    definition

      let T be reflexive transitive antisymmetric with_suprema TA-structure;

      :: original: adj-structured

      redefine

      :: ABCMIZ_0:def11

      attr T is adj-structured means

      : Def11: for t1,t2 be type of T holds ( adjs (t1 "\/" t2)) = (( adjs t1) /\ ( adjs t2));

      compatibility

      proof

        

         A1: ( dom the adj-map of T) = the carrier of T by FUNCT_2:def 1;

        

         A2: ( Fin the adjectives of T) c= ( bool the adjectives of T) by FINSUB_1: 13;

        ( BoolePoset the adjectives of T) = ( InclPoset ( bool the adjectives of T)) by YELLOW_1: 4

        .= RelStr (# ( bool the adjectives of T), ( RelIncl ( bool the adjectives of T)) #) by YELLOW_1:def 1;

        then ( rng the adj-map of T) c= the carrier of (( BoolePoset the adjectives of T) opp ) by A2;

        then

        reconsider f = the adj-map of T as Function of T, (( BoolePoset the adjectives of T) opp ) by A1, FUNCT_2: 2;

        thus T is adj-structured implies for t1,t2 be type of T holds ( adjs (t1 "\/" t2)) = (( adjs t1) /\ ( adjs t2))

        proof

          assume the adj-map of T is join-preserving Function of T, (( BoolePoset the adjectives of T) opp );

          then

          reconsider f = the adj-map of T as join-preserving Function of T, (( BoolePoset the adjectives of T) opp );

          let t1,t2 be type of T;

          

          thus ( adjs (t1 "\/" t2)) = ((f . t1) "\/" (f . t2)) by WAYBEL_6: 2

          .= (( ~ (f . t1)) "/\" ( ~ (f . t2))) by YELLOW_7: 22

          .= (( adjs t1) /\ ( adjs t2)) by YELLOW_1: 17;

        end;

        assume

         A3: for t1,t2 be type of T holds ( adjs (t1 "\/" t2)) = (( adjs t1) /\ ( adjs t2));

        now

          let t1,t2 be type of T;

          

          thus (f . (t1 "\/" t2)) = ( adjs (t1 "\/" t2))

          .= (( adjs t1) /\ ( adjs t2)) by A3

          .= (( ~ (f . t1)) "/\" ( ~ (f . t2))) by YELLOW_1: 17

          .= ((f . t1) "\/" (f . t2)) by YELLOW_7: 22;

        end;

        hence the adj-map of T is join-preserving Function of T, (( BoolePoset the adjectives of T) opp ) by WAYBEL_6: 2;

      end;

    end

    theorem :: ABCMIZ_0:10

    

     Th10: for T be reflexive transitive antisymmetric with_suprema TA-structure st T is adj-structured holds for t1,t2 be type of T st t1 <= t2 holds ( adjs t2) c= ( adjs t1)

    proof

      let T be reflexive transitive antisymmetric with_suprema TA-structure such that

       A1: for t1,t2 be type of T holds ( adjs (t1 "\/" t2)) = (( adjs t1) /\ ( adjs t2));

      let t1,t2 be type of T;

      assume t1 <= t2;

      then (t1 "\/" t2) = t2 by YELLOW_0: 24;

      then ( adjs t2) = (( adjs t1) /\ ( adjs t2)) by A1;

      hence thesis by XBOOLE_1: 17;

    end;

    definition

      let T be TA-structure;

      let a be Element of the adjectives of T;

      :: ABCMIZ_0:def12

      func types a -> Subset of T means

      : Def12: for x be object holds x in it iff ex t be type of T st x = t & a in ( adjs t);

      existence

      proof

        defpred P[ object] means ex t be type of T st $1 = t & a in ( adjs t);

        consider tt be set such that

         A1: for x be object holds x in tt iff x in the carrier of T & P[x] from XBOOLE_0:sch 1;

        tt c= the carrier of T by A1;

        then

        reconsider tt as Subset of T;

        take tt;

        let x be object;

        thus x in tt implies ex t be type of T st x = t & a in ( adjs t) by A1;

        given t be type of T such that

         A2: x = t and

         A3: a in ( adjs t);

        now

          

           A4: ( dom the adj-map of T) = the carrier of T by FUNCT_2:def 1;

          assume not x in the carrier of T;

          hence contradiction by A2, A3, A4, FUNCT_1:def 2;

        end;

        hence thesis by A1, A2, A3;

      end;

      uniqueness

      proof

        defpred P[ object] means ex t be type of T st $1 = t & a in ( adjs t);

        let X1,X2 be Subset of T such that

         A5: for x be object holds x in X1 iff P[x] and

         A6: for x be object holds x in X2 iff P[x];

        thus thesis from XBOOLE_0:sch 2( A5, A6);

      end;

    end

    definition

      let T be non empty TA-structure;

      let A be Subset of the adjectives of T;

      :: ABCMIZ_0:def13

      func types A -> Subset of T means

      : Def13: for t be type of T holds t in it iff for a be adjective of T st a in A holds t in ( types a);

      existence

      proof

        defpred P[ object] means for a be adjective of T st a in A holds $1 in ( types a);

        consider tt be set such that

         A1: for x be object holds x in tt iff x in the carrier of T & P[x] from XBOOLE_0:sch 1;

        tt c= the carrier of T by A1;

        then

        reconsider tt as Subset of T;

        take tt;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let X1,X2 be Subset of T such that

         A2: for t be type of T holds t in X1 iff for a be adjective of T st a in A holds t in ( types a) and

         A3: for t be type of T holds t in X2 iff for a be adjective of T st a in A holds t in ( types a);

        now

          let x be object;

          x in X1 iff x is type of T & for a be adjective of T st a in A holds x in ( types a) by A2;

          hence x in X1 iff x in X2 by A3;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    theorem :: ABCMIZ_0:11

    

     Th11: for T1,T2 be TA-structure st the TA-structure of T1 = the TA-structure of T2 holds for a1 be adjective of T1, a2 be adjective of T2 st a1 = a2 holds ( types a1) = ( types a2)

    proof

      let T1,T2 be TA-structure such that

       A1: the TA-structure of T1 = the TA-structure of T2;

      let a1 be adjective of T1, a2 be adjective of T2 such that

       A2: a1 = a2;

      now

        thus ( types a1) is Subset of T2 by A1;

        let x be object;

        hereby

          assume x in ( types a1);

          then

          consider t1 be type of T1 such that

           A3: x = t1 and

           A4: a1 in ( adjs t1) by Def12;

          reconsider t2 = t1 as type of T2 by A1;

          ( adjs t1) = ( adjs t2) by A1;

          hence ex t2 be type of T2 st x = t2 & a2 in ( adjs t2) by A2, A3, A4;

        end;

        given t2 be type of T2 such that

         A5: x = t2 and

         A6: a2 in ( adjs t2);

        reconsider t1 = t2 as type of T1 by A1;

        ( adjs t1) = ( adjs t2) by A1;

        hence x in ( types a1) by A2, A5, A6, Def12;

      end;

      hence thesis by Def12;

    end;

    theorem :: ABCMIZ_0:12

    for T be non empty TA-structure holds for a be adjective of T holds ( types a) = { t where t be type of T : a in ( adjs t) }

    proof

      let T be non empty TA-structure;

      let a be adjective of T;

      set X = { t where t be type of T : a in ( adjs t) };

      X c= the carrier of T

      proof

        let x be object;

        assume x in X;

        then ex t be type of T st x = t & a in ( adjs t);

        hence thesis;

      end;

      then

      reconsider X as Subset of T;

      for x be object holds x in X iff ex t be type of T st x = t & a in ( adjs t);

      hence thesis by Def12;

    end;

    theorem :: ABCMIZ_0:13

    

     Th13: for T be TA-structure holds for t be type of T, a be adjective of T holds a in ( adjs t) iff t in ( types a)

    proof

      let T be TA-structure;

      let t be type of T, a be adjective of T;

      thus a in ( adjs t) implies t in ( types a) by Def12;

      assume t in ( types a);

      then ex t9 be type of T st t = t9 & a in ( adjs t9) by Def12;

      hence thesis;

    end;

    theorem :: ABCMIZ_0:14

    

     Th14: for T be non empty TA-structure holds for t be type of T, A be Subset of the adjectives of T holds A c= ( adjs t) iff t in ( types A)

    proof

      let T be non empty TA-structure;

      let t be type of T, a be Subset of the adjectives of T;

      hereby

        assume a c= ( adjs t);

        then for b be adjective of T st b in a holds t in ( types b) by Th13;

        hence t in ( types a) by Def13;

      end;

      assume

       A1: t in ( types a);

      let x be object;

      assume

       A2: x in a;

      then

      reconsider x as adjective of T;

      t in ( types x) by A1, A2, Def13;

      hence thesis by Th13;

    end;

    theorem :: ABCMIZ_0:15

    for T be non void TA-structure holds for t be type of T holds ( adjs t) = { a where a be adjective of T : t in ( types a) }

    proof

      let T be non void TA-structure;

      let t be type of T;

      set X = { a where a be adjective of T : t in ( types a) };

      thus ( adjs t) c= X

      proof

        let x be object;

        assume

         A1: x in ( adjs t);

        then

        reconsider a = x as adjective of T;

        t in ( types a) by A1, Th13;

        hence thesis;

      end;

      let x be object;

      assume x in X;

      then ex a be adjective of T st x = a & t in ( types a);

      hence thesis by Th13;

    end;

    theorem :: ABCMIZ_0:16

    

     Th16: for T be non empty TA-structure holds ( types ( {} the adjectives of T)) = the carrier of T

    proof

      let T be non empty TA-structure;

      thus ( types ( {} the adjectives of T)) c= the carrier of T;

      let x be object;

      assume x in the carrier of T;

      then

      reconsider t = x as type of T;

      for a be adjective of T st a in ( {} the adjectives of T) holds t in ( types a);

      hence thesis by Def13;

    end;

    definition

      let T be TA-structure;

      :: ABCMIZ_0:def14

      attr T is adjs-typed means for a be adjective of T holds (( types a) \/ ( types ( non- a))) is non empty;

    end

    theorem :: ABCMIZ_0:17

    

     Th17: for T1,T2 be TA-structure st the TA-structure of T1 = the TA-structure of T2 holds T1 is adjs-typed implies T2 is adjs-typed

    proof

      let T1,T2 be TA-structure such that

       A1: the TA-structure of T1 = the TA-structure of T2 and

       A2: for a be adjective of T1 holds (( types a) \/ ( types ( non- a))) is non empty;

      let b be adjective of T2;

      reconsider a = b as adjective of T1 by A1;

      

       A3: (( types a) \/ ( types ( non- a))) is non empty by A2;

      ( types a) = ( types b) by A1, Th11;

      hence thesis by A1, A3, Th11;

    end;

    registration

      cluster non void Mizar-widening-like involutive without_fixpoints consistent adj-structured adjs-typed for complete upper-bounded1 -element reflexive transitive antisymmetric strict TA-structure;

      existence

      proof

         { 0 } c= { 0 , 1} by ZFMISC_1: 7;

        then

        reconsider A = { 0 } as Element of ( Fin { 0 , 1}) by FINSUB_1:def 5;

        reconsider x = 0 , y = 1 as Element of { 0 , 1} by TARSKI:def 2;

        set R = the reflexive1 -element RelStr;

        reconsider n = (( 0 ,1) --> (y,x)) as UnOp of { 0 , 1};

        set f = (the carrier of R --> A);

        set T = TA-structure (# the carrier of R, { 0 , 1}, the InternalRel of R, n, f #);

         the RelStr of T = the RelStr of R;

        then

        reconsider T as strict1 -element reflexive TA-structure by STRUCT_0:def 19, WAYBEL_8: 12;

        take T;

        thus T is non void;

        thus T is Mizar-widening-like;

        

         A1: (n . y) = x by FUNCT_4: 63;

        

         A2: (n . x) = y by FUNCT_4: 63;

        hence T is involutive without_fixpoints by A1, Th4;

        hereby

          let t be type of T;

          let a be adjective of T;

          

           A3: ( adjs t) = A by FUNCOP_1: 7;

          a = 0 or a = 1 by TARSKI:def 2;

          hence a in ( adjs t) implies not ( non- a) in ( adjs t) by A2, A3, TARSKI:def 1;

        end;

        set t = the type of T;

        hereby

          let t1,t2 be type of T;

          

           A4: ( adjs t2) = A by FUNCOP_1: 7;

          ( adjs t1) = A by FUNCOP_1: 7;

          hence ( adjs (t1 "\/" t2)) = (( adjs t1) /\ ( adjs t2)) by A4, FUNCOP_1: 7;

        end;

        let a be adjective of T;

        

         A5: ( adjs t) = A by FUNCOP_1: 7;

        a = 0 or a = 1 by TARSKI:def 2;

        then a in ( adjs t) or ( non- a) in ( adjs t) by A1, A5, TARSKI:def 1;

        then t in ( types a) or t in ( types ( non- a)) by Th13;

        hence thesis;

      end;

    end

    theorem :: ABCMIZ_0:18

    for T be consistent TA-structure holds for a be adjective of T holds ( types a) misses ( types ( non- a))

    proof

      let T be consistent TA-structure;

      let a be adjective of T;

      assume ( types a) meets ( types ( non- a));

      then

      consider x be object such that

       A1: x in ( types a) and

       A2: x in ( types ( non- a)) by XBOOLE_0: 3;

      

       A3: ex t2 be type of T st x = t2 & ( non- a) in ( adjs t2) by A2, Def12;

      ex t1 be type of T st x = t1 & a in ( adjs t1) by A1, Def12;

      hence thesis by A3, Def9;

    end;

    registration

      let T be adj-structured reflexive transitive antisymmetric with_suprema TA-structure;

      let a be adjective of T;

      cluster ( types a) -> lower directed;

      coherence

      proof

        thus ( types a) is lower

        proof

          let x,y be Element of T;

          assume that

           A1: x in ( types a) and

           A2: y <= x;

          

           A3: ( adjs x) c= ( adjs y) by A2, Th10;

          a in ( adjs x) by A1, Th13;

          hence thesis by A3, Th13;

        end;

        let x,y be Element of T;

        assume that

         A4: x in ( types a) and

         A5: y in ( types a);

        take (x "\/" y);

        

         A6: a in ( adjs y) by A5, Th13;

        a in ( adjs x) by A4, Th13;

        then a in (( adjs x) /\ ( adjs y)) by A6, XBOOLE_0:def 4;

        then a in ( adjs (x "\/" y)) by Def11;

        hence thesis by Th13, YELLOW_0: 22;

      end;

    end

    registration

      let T be adj-structured reflexive transitive antisymmetric with_suprema TA-structure;

      let A be Subset of the adjectives of T;

      cluster ( types A) -> lower directed;

      coherence

      proof

        thus ( types A) is lower

        proof

          let x,y be Element of T;

          assume that

           A1: x in ( types A) and

           A2: y <= x;

          now

            let a be adjective of T;

            assume a in A;

            then x in ( types a) by A1, Def13;

            then

             A3: a in ( adjs x) by Th13;

            ( adjs x) c= ( adjs y) by A2, Th10;

            hence y in ( types a) by A3, Th13;

          end;

          hence thesis by Def13;

        end;

        let x,y be Element of T;

        assume that

         A4: x in ( types A) and

         A5: y in ( types A);

        take (x "\/" y);

        now

          let a be adjective of T;

          assume

           A6: a in A;

          then y in ( types a) by A5, Def13;

          then

           A7: a in ( adjs y) by Th13;

          x in ( types a) by A4, A6, Def13;

          then a in ( adjs x) by Th13;

          then a in (( adjs x) /\ ( adjs y)) by A7, XBOOLE_0:def 4;

          then a in ( adjs (x "\/" y)) by Def11;

          hence (x "\/" y) in ( types a) by Th13;

        end;

        hence thesis by Def13, YELLOW_0: 22;

      end;

    end

    begin

    definition

      let T be TA-structure;

      let t be Element of T;

      let a be adjective of T;

      :: ABCMIZ_0:def15

      pred a is_applicable_to t means ex t9 be type of T st t9 in ( types a) & t9 <= t;

    end

    definition

      let T be TA-structure;

      let t be type of T;

      let A be Subset of the adjectives of T;

      :: ABCMIZ_0:def16

      pred A is_applicable_to t means ex t9 be type of T st A c= ( adjs t9) & t9 <= t;

    end

    theorem :: ABCMIZ_0:19

    

     Th19: for T be adj-structured reflexive transitive antisymmetric with_suprema TA-structure holds for a be adjective of T holds for t be type of T st a is_applicable_to t holds (( types a) /\ ( downarrow t)) is Ideal of T

    proof

      let T be adj-structured reflexive transitive antisymmetric with_suprema TA-structure;

      let a be adjective of T;

      let t be type of T;

      given t9 be type of T such that

       A1: t9 in ( types a) and

       A2: t9 <= t;

      t9 in ( downarrow t) by A2, WAYBEL_0: 17;

      hence thesis by A1, WAYBEL_0: 27, WAYBEL_0: 44, XBOOLE_0:def 4;

    end;

    definition

      let T be non empty reflexive transitive TA-structure;

      let t be Element of T;

      let a be adjective of T;

      :: ABCMIZ_0:def17

      func a ast t -> type of T equals ( sup (( types a) /\ ( downarrow t)));

      coherence ;

    end

    theorem :: ABCMIZ_0:20

    

     Th20: for T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema TA-structure holds for t be type of T holds for a be adjective of T st a is_applicable_to t holds (a ast t) <= t

    proof

      let T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema TA-structure;

      let t be type of T;

      let a be adjective of T;

      assume a is_applicable_to t;

      then (( types a) /\ ( downarrow t)) is Ideal of T by Th19;

      then ( sup (( types a) /\ ( downarrow t))) in (( types a) /\ ( downarrow t)) by Th1;

      then (a ast t) in ( downarrow t) by XBOOLE_0:def 4;

      hence thesis by WAYBEL_0: 17;

    end;

    theorem :: ABCMIZ_0:21

    

     Th21: for T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema TA-structure holds for t be type of T holds for a be adjective of T st a is_applicable_to t holds a in ( adjs (a ast t))

    proof

      let T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema TA-structure;

      let t be type of T;

      let a be adjective of T;

      assume a is_applicable_to t;

      then (( types a) /\ ( downarrow t)) is Ideal of T by Th19;

      then ( sup (( types a) /\ ( downarrow t))) in (( types a) /\ ( downarrow t)) by Th1;

      then (a ast t) in ( types a) by XBOOLE_0:def 4;

      hence thesis by Th13;

    end;

    theorem :: ABCMIZ_0:22

    

     Th22: for T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema TA-structure holds for t be type of T holds for a be adjective of T st a is_applicable_to t holds (a ast t) in ( types a)

    proof

      let T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema TA-structure;

      let t be type of T;

      let a be adjective of T;

      assume a is_applicable_to t;

      then (( types a) /\ ( downarrow t)) is Ideal of T by Th19;

      then ( sup (( types a) /\ ( downarrow t))) in (( types a) /\ ( downarrow t)) by Th1;

      hence thesis by XBOOLE_0:def 4;

    end;

    theorem :: ABCMIZ_0:23

    

     Th23: for T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema TA-structure holds for t be type of T holds for a be adjective of T holds for t9 be type of T st t9 <= t & a in ( adjs t9) holds a is_applicable_to t & t9 <= (a ast t)

    proof

      let T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema TA-structure;

      let t be type of T;

      let a be adjective of T;

      let t9 be type of T;

      assume that

       A1: t9 <= t and

       A2: a in ( adjs t9);

      

       A3: t9 in ( downarrow t) by A1, WAYBEL_0: 17;

      thus a is_applicable_to t by A1, A2, Th13;

      then (( types a) /\ ( downarrow t)) is Ideal of T by Th19;

      then ex_sup_of ((( types a) /\ ( downarrow t)),T) by Th1;

      then

       A4: (a ast t) is_>=_than (( types a) /\ ( downarrow t)) by YELLOW_0: 30;

      t9 in ( types a) by A2, Th13;

      then t9 in (( types a) /\ ( downarrow t)) by A3, XBOOLE_0:def 4;

      hence thesis by A4;

    end;

    theorem :: ABCMIZ_0:24

    

     Th24: for T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema TA-structure holds for t be type of T holds for a be adjective of T st a in ( adjs t) holds a is_applicable_to t & (a ast t) = t

    proof

      let T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema TA-structure;

      let t be type of T;

      let a be adjective of T;

      assume

       A1: a in ( adjs t);

      hence a is_applicable_to t by Th23;

      then

       A2: (a ast t) <= t by Th20;

      t <= (a ast t) by A1, Th23;

      hence thesis by A2, YELLOW_0:def 3;

    end;

    theorem :: ABCMIZ_0:25

    for T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema TA-structure holds for t be type of T holds for a,b be adjective of T st a is_applicable_to t & b is_applicable_to (a ast t) holds b is_applicable_to t & a is_applicable_to (b ast t) & (a ast (b ast t)) = (b ast (a ast t))

    proof

      let T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema TA-structure;

      let t be type of T;

      let a,b be adjective of T such that

       A1: a is_applicable_to t and

       A2: b is_applicable_to (a ast t);

      consider t9 be type of T such that

       A3: t9 in ( types b) and

       A4: t9 <= (a ast t) by A2;

      

       A5: b in ( adjs t9) by A3, Th13;

      

       A6: (a ast t) <= t by A1, Th20;

      thus

       A7: b is_applicable_to t by A6, A3, A4, YELLOW_0:def 2;

      

       A8: t9 <= t by A6, A4, YELLOW_0:def 2;

      thus

       A9: a is_applicable_to (b ast t)

      proof

        take t9;

        (a ast t) in ( types a) by A1, Th22;

        hence t9 in ( types a) by A4, WAYBEL_0:def 19;

        thus t9 <= (b ast t) by A8, A5, Th23;

      end;

      then

       A10: (a ast (b ast t)) <= (b ast t) by Th20;

      

       A11: (a ast t) in ( types a) by A1, Th22;

      

       A12: (a ast (b ast t)) is_>=_than (( types b) /\ ( downarrow (a ast t)))

      proof

        let t9 be type of T;

        assume

         A13: t9 in (( types b) /\ ( downarrow (a ast t)));

        then t9 in ( types b) by XBOOLE_0:def 4;

        then

         A14: b in ( adjs t9) by Th13;

        t9 in ( downarrow (a ast t)) by A13, XBOOLE_0:def 4;

        then

         A15: t9 <= (a ast t) by WAYBEL_0: 17;

        then t9 in ( types a) by A11, WAYBEL_0:def 19;

        then

         A16: a in ( adjs t9) by Th13;

        t9 <= t by A6, A15, YELLOW_0:def 2;

        then t9 <= (b ast t) by A14, Th23;

        hence thesis by A16, Th23;

      end;

      (b ast t) <= t by A7, Th20;

      then

       A17: (a ast (b ast t)) <= t by A10, YELLOW_0:def 2;

      a in ( adjs (a ast (b ast t))) by A9, Th21;

      then (a ast (b ast t)) <= (a ast t) by A17, Th23;

      then

       A18: (a ast (b ast t)) in ( downarrow (a ast t)) by WAYBEL_0: 17;

      

       A19: (a ast (b ast t)) <= (b ast t) by A9, Th20;

      (b ast t) in ( types b) by A7, Th22;

      then (a ast (b ast t)) in ( types b) by A19, WAYBEL_0:def 19;

      then (a ast (b ast t)) in (( types b) /\ ( downarrow (a ast t))) by A18, XBOOLE_0:def 4;

      then for t9 be type of T st t9 is_>=_than (( types b) /\ ( downarrow (a ast t))) holds (a ast (b ast t)) <= t9;

      hence thesis by A12, YELLOW_0: 30;

    end;

    theorem :: ABCMIZ_0:26

    

     Th26: for T be adj-structured reflexive transitive antisymmetric with_suprema TA-structure holds for A be Subset of the adjectives of T holds for t be type of T st A is_applicable_to t holds (( types A) /\ ( downarrow t)) is Ideal of T

    proof

      let T be adj-structured reflexive transitive antisymmetric with_suprema TA-structure;

      let A be Subset of the adjectives of T;

      let t be type of T;

      given t9 be type of T such that

       A1: A c= ( adjs t9) and

       A2: t9 <= t;

      

       A3: t9 in ( downarrow t) by A2, WAYBEL_0: 17;

      t9 in ( types A) by A1, Th14;

      hence thesis by A3, WAYBEL_0: 27, WAYBEL_0: 44, XBOOLE_0:def 4;

    end;

    definition

      let T be non empty reflexive transitive TA-structure;

      let t be type of T;

      let A be Subset of the adjectives of T;

      :: ABCMIZ_0:def18

      func A ast t -> type of T equals ( sup (( types A) /\ ( downarrow t)));

      coherence ;

    end

    theorem :: ABCMIZ_0:27

    

     Th27: for T be non empty reflexive transitive antisymmetric TA-structure holds for t be type of T holds (( {} the adjectives of T) ast t) = t

    proof

      let T be non empty reflexive transitive antisymmetric TA-structure;

      let t be type of T;

      set A = ( {} the adjectives of T);

      ( types A) = the carrier of T by Th16;

      then (( types A) /\ ( downarrow t)) = ( downarrow t) by XBOOLE_1: 28;

      hence thesis by WAYBEL_0: 34;

    end;

    definition

      let T be non empty non void reflexive transitive TA-structure;

      let t be type of T;

      let p be FinSequence of the adjectives of T;

      :: ABCMIZ_0:def19

      func apply (p,t) -> FinSequence of the carrier of T means

      : Def19: ( len it ) = (( len p) + 1) & (it . 1) = t & for i be Element of NAT , a be adjective of T, t be type of T st i in ( dom p) & a = (p . i) & t = (it . i) holds (it . (i + 1)) = (a ast t);

      existence

      proof

        defpred P[ set, set, set] means ex a be adjective of T st a = (p . $1) & ( not $2 is type of T & $3 = 0 or ex t be type of T st t = $2 & $3 = (a ast t));

        

         A1: for i be Nat st 1 <= i & i < (( len p) + 1) holds for x be set holds ex y be set st P[i, x, y]

        proof

          let i be Nat;

          assume

           A2: 1 <= i;

          assume i < (( len p) + 1);

          then i <= ( len p) by NAT_1: 13;

          then i in ( dom p) by A2, FINSEQ_3: 25;

          then (p . i) in ( rng p) by FUNCT_1: 3;

          then

          reconsider a = (p . i) as adjective of T;

          let x be set;

          per cases ;

            suppose

             A3: not x is type of T;

            take 0 , a;

            thus thesis by A3;

          end;

            suppose x is type of T;

            then

            reconsider t = x as type of T;

            take (a ast t), a;

            thus a = (p . i);

            thus thesis;

          end;

        end;

        consider q be FinSequence such that

         A4: ( len q) = (( len p) + 1) and

         A5: (q . 1) = t or (( len p) + 1) = 0 and

         A6: for i be Nat st 1 <= i & i < (( len p) + 1) holds P[i, (q . i), (q . (i + 1))] from RECDEF_1:sch 3( A1);

        defpred P[ Nat] means $1 in ( dom q) implies (q . $1) is type of T;

         A7:

        now

          let k be Nat such that

           A8: P[k];

          now

            assume (k + 1) in ( dom q);

            then (k + 1) <= ( len q) by FINSEQ_3: 25;

            then

             A9: k < ( len q) by NAT_1: 13;

            

             A10: k <> 0 implies k >= ( 0 + 1) by NAT_1: 13;

            then k <> 0 implies ex a be adjective of T st a = (p . k) & ( not (q . k) is type of T & (q . (k + 1)) = 0 or ex t be type of T st t = (q . k) & (q . (k + 1)) = (a ast t)) by A4, A6, A9;

            hence (q . (k + 1)) is type of T by A5, A8, A10, A9, FINSEQ_3: 25;

          end;

          hence P[(k + 1)];

        end;

        

         A11: P[ 0 ] by FINSEQ_3: 24;

        

         A12: for k be Nat holds P[k] from NAT_1:sch 2( A11, A7);

        ( rng q) c= the carrier of T

        proof

          let a be object;

          assume a in ( rng q);

          then ex x be object st x in ( dom q) & a = (q . x) by FUNCT_1:def 3;

          then a is type of T by A12;

          hence thesis;

        end;

        then

        reconsider q as FinSequence of the carrier of T by FINSEQ_1:def 4;

        take q;

        thus ( len q) = (( len p) + 1) & (q . 1) = t by A4, A5;

        let i be Element of NAT , a be adjective of T, t be type of T;

        assume that

         A13: i in ( dom p) and

         A14: a = (p . i) and

         A15: t = (q . i);

        i <= ( len p) by A13, FINSEQ_3: 25;

        then

         A16: i < (( len p) + 1) by NAT_1: 13;

        i >= 1 by A13, FINSEQ_3: 25;

        then ex a be adjective of T st a = (p . i) & ( not (q . i) is type of T & (q . (i + 1)) = 0 or ex t be type of T st t = (q . i) & (q . (i + 1)) = (a ast t)) by A6, A16;

        hence thesis by A14, A15;

      end;

      correctness

      proof

        let q1,q2 be FinSequence of the carrier of T such that

         A17: ( len q1) = (( len p) + 1) and

         A18: (q1 . 1) = t and

         A19: for i be Element of NAT , a be adjective of T, t be type of T st i in ( dom p) & a = (p . i) & t = (q1 . i) holds (q1 . (i + 1)) = (a ast t) and

         A20: ( len q2) = (( len p) + 1) and

         A21: (q2 . 1) = t and

         A22: for i be Element of NAT , a be adjective of T, t be type of T st i in ( dom p) & a = (p . i) & t = (q2 . i) holds (q2 . (i + 1)) = (a ast t);

        defpred P[ Nat] means $1 in ( dom q1) implies (q1 . $1) = (q2 . $1);

         A23:

        now

          let i be Nat such that

           A24: P[i];

          now

            assume (i + 1) in ( dom q1);

            then

             A25: (i + 1) <= ( len q1) by FINSEQ_3: 25;

            then

             A26: i <= ( len q1) by NAT_1: 13;

            

             A27: i <= ( len p) by A17, A25, XREAL_1: 6;

            per cases ;

              suppose i = 0 ;

              hence (q1 . (i + 1)) = (q2 . (i + 1)) by A18, A21;

            end;

              suppose i > 0 ;

              then

               A28: i >= ( 0 + 1) by NAT_1: 13;

              then

               A29: i in ( dom p) by A27, FINSEQ_3: 25;

              then

              reconsider a = (p . i) as adjective of T by FINSEQ_2: 11;

              i in ( dom q1) by A26, A28, FINSEQ_3: 25;

              then

              reconsider t = (q1 . i) as type of T by FINSEQ_2: 11;

              

              thus (q1 . (i + 1)) = (a ast t) by A19, A29

              .= (q2 . (i + 1)) by A22, A24, A26, A28, A29, FINSEQ_3: 25;

            end;

          end;

          hence P[(i + 1)];

        end;

        

         A30: P[ 0 ] by FINSEQ_3: 25;

        

         A31: for i be Nat holds P[i] from NAT_1:sch 2( A30, A23);

        ( dom q1) = ( dom q2) by A17, A20, FINSEQ_3: 29;

        hence thesis by A31;

      end;

    end

    registration

      let T be non empty non void reflexive transitive TA-structure;

      let t be type of T;

      let p be FinSequence of the adjectives of T;

      cluster ( apply (p,t)) -> non empty;

      coherence

      proof

        ( len ( apply (p,t))) = (( len p) + 1) by Def19;

        hence thesis;

      end;

    end

    theorem :: ABCMIZ_0:28

    for T be non empty non void reflexive transitive TA-structure holds for t be type of T holds ( apply (( <*> the adjectives of T),t)) = <*t*>

    proof

      let T be non empty non void reflexive transitive TA-structure;

      let t be type of T;

      

       A1: (( apply (( <*> the adjectives of T),t)) . 1) = t by Def19;

      ( len ( apply (( <*> the adjectives of T),t))) = ( 0 + 1) by Def19, CARD_1: 27;

      hence thesis by A1, FINSEQ_1: 40;

    end;

    theorem :: ABCMIZ_0:29

    

     Th29: for T be non empty non void reflexive transitive TA-structure holds for t be type of T, a be adjective of T holds ( apply ( <*a*>,t)) = <*t, (a ast t)*>

    proof

      let T be non empty non void reflexive transitive TA-structure;

      let t be type of T, a be adjective of T;

      

       A1: ( <*a*> . 1) = a by FINSEQ_1: 40;

      

       A2: (( apply ( <*a*>,t)) . 1) = t by Def19;

      

       A3: ( len <*a*>) = 1 by FINSEQ_1: 40;

      then

       A4: ( len ( apply ( <*a*>,t))) = (1 + 1) by Def19;

      1 in ( dom <*a*>) by A3, FINSEQ_3: 25;

      then (( apply ( <*a*>,t)) . (( len <*a*>) + 1)) = (a ast t) by A3, A2, A1, Def19;

      hence thesis by A3, A4, A2, FINSEQ_1: 44;

    end;

    definition

      let T be non empty non void reflexive transitive TA-structure;

      let t be type of T;

      let v be FinSequence of the adjectives of T;

      :: ABCMIZ_0:def20

      func v ast t -> type of T equals (( apply (v,t)) . (( len v) + 1));

      coherence

      proof

        

         A1: (( len v) + 1) >= 1 by NAT_1: 11;

        ( len ( apply (v,t))) = (( len v) + 1) by Def19;

        then (( len v) + 1) in ( dom ( apply (v,t))) by A1, FINSEQ_3: 25;

        hence thesis by FINSEQ_2: 11;

      end;

    end

    theorem :: ABCMIZ_0:30

    for T be non empty non void reflexive transitive TA-structure holds for t be type of T holds (( <*> the adjectives of T) ast t) = t by Def19;

    theorem :: ABCMIZ_0:31

    

     Th31: for T be non empty non void reflexive transitive TA-structure holds for t be type of T holds for a be adjective of T holds ( <*a*> ast t) = (a ast t)

    proof

      let T be non empty non void reflexive transitive TA-structure;

      let t be type of T;

      let a be adjective of T;

      

       A1: ( len <*a*>) = 1 by FINSEQ_1: 40;

      ( apply ( <*a*>,t)) = <*t, (a ast t)*> by Th29;

      hence thesis by A1, FINSEQ_1: 44;

    end;

    theorem :: ABCMIZ_0:32

    for p,q be FinSequence holds for i be Nat st i >= 1 & i < ( len p) holds ((p $^ q) . i) = (p . i)

    proof

      let p,q be FinSequence;

      let i be Nat;

      assume that

       A1: i >= 1 and

       A2: i < ( len p);

      per cases ;

        suppose q = {} ;

        hence thesis by REWRITE1: 1;

      end;

        suppose q <> {} ;

        then

        consider j be Nat, r be FinSequence such that

         A3: ( len p) = (j + 1) and

         A4: r = (p | ( Seg j)) and

         A5: (p $^ q) = (r ^ q) by A2, CARD_1: 27, REWRITE1:def 1;

        

         A6: p = (r ^ <*(p . ( len p))*>) by A3, A4, FINSEQ_3: 55;

        j < ( len p) by A3, NAT_1: 13;

        then

         A7: ( len r) = j by A4, FINSEQ_1: 17;

        i <= j by A2, A3, NAT_1: 13;

        then

         A8: i in ( dom r) by A1, A7, FINSEQ_3: 25;

        then ((p $^ q) . i) = (r . i) by A5, FINSEQ_1:def 7;

        hence thesis by A8, A6, FINSEQ_1:def 7;

      end;

    end;

    theorem :: ABCMIZ_0:33

    

     Th33: for p be non empty FinSequence, q be FinSequence holds for i be Nat st i < ( len q) holds ((p $^ q) . (( len p) + i)) = (q . (i + 1))

    proof

      let p be non empty FinSequence, q be FinSequence;

      let i be Nat;

      

       A1: (i + 1) >= 1 by NAT_1: 11;

      assume

       A2: i < ( len q);

      then

      consider j be Nat, r be FinSequence such that

       A3: ( len p) = (j + 1) and

       A4: r = (p | ( Seg j)) and

       A5: (p $^ q) = (r ^ q) by CARD_1: 27, REWRITE1:def 1;

      (i + 1) <= ( len q) by A2, NAT_1: 13;

      then

       A6: (i + 1) in ( dom q) by A1, FINSEQ_3: 25;

      j < ( len p) by A3, NAT_1: 13;

      then ( len r) = j by A4, FINSEQ_1: 17;

      then (( len p) + i) = (( len r) + (i + 1)) by A3;

      hence thesis by A5, A6, FINSEQ_1:def 7;

    end;

    theorem :: ABCMIZ_0:34

    

     Th34: for T be non empty non void reflexive transitive TA-structure holds for t be type of T holds for v1,v2 be FinSequence of the adjectives of T holds ( apply ((v1 ^ v2),t)) = (( apply (v1,t)) $^ ( apply (v2,(v1 ast t))))

    proof

      let T be non empty non void reflexive transitive TA-structure;

      let t be type of T;

      let v1,v2 be FinSequence of the adjectives of T;

      consider tt be FinSequence of the carrier of T, q be Element of T such that

       A1: ( apply (v1,t)) = (tt ^ <*q*>) by HILBERT2: 4;

      set s = (( apply (v1,t)) $^ ( apply (v2,(v1 ast t)))), p = (v1 ^ v2);

      

       A2: ( len ( apply (v1,t))) = (( len v1) + 1) by Def19;

      

       A3: (( apply (v1,t)) $^ ( apply (v2,(v1 ast t)))) = (tt ^ ( apply (v2,(v1 ast t)))) by A1, REWRITE1: 2;

      ( len <*q*>) = 1 by FINSEQ_1: 39;

      then

       A4: (( len v1) + 1) = (( len tt) + 1) by A2, A1, FINSEQ_1: 22;

      

       A5: (s . 1) = t

      proof

        per cases ;

          suppose

           A6: ( len v1) = 0 ;

          then tt = {} by A4;

          then

           A7: s = ( apply (v2,(v1 ast t))) by A3, FINSEQ_1: 34;

          (v1 ast t) = t by A6, Def19;

          hence thesis by A7, Def19;

        end;

          suppose ( len v1) > 0 ;

          then ( len tt) >= ( 0 + 1) by A4, NAT_1: 13;

          then

           A8: 1 in ( dom tt) by FINSEQ_3: 25;

          then

           A9: (tt . 1) = (( apply (v1,t)) . 1) by A1, FINSEQ_1:def 7;

          (s . 1) = (tt . 1) by A3, A8, FINSEQ_1:def 7;

          hence thesis by A9, Def19;

        end;

      end;

       A10:

      now

        

         A11: ( len p) = (( len v1) + ( len v2)) by FINSEQ_1: 22;

        

         A12: ( len ( apply (v2,(v1 ast t)))) = (( len v2) + 1) by Def19;

        let i be Element of NAT , a be adjective of T, t9 be type of T such that

         A13: i in ( dom p) and

         A14: a = (p . i) and

         A15: t9 = (s . i);

        

         A16: 1 <= i by A13, FINSEQ_3: 25;

        

         A17: i <= ( len p) by A13, FINSEQ_3: 25;

        per cases by XXREAL_0: 1;

          suppose

           A18: i < ( len v1);

          

           A19: (i + 1) >= 1 by NAT_1: 11;

          (i + 1) <= ( len v1) by A18, NAT_1: 13;

          then

           A20: (i + 1) in ( dom tt) by A4, A19, FINSEQ_3: 25;

          then

           A21: (s . (i + 1)) = (tt . (i + 1)) by A3, FINSEQ_1:def 7;

          

           A22: i in ( dom tt) by A4, A16, A18, FINSEQ_3: 25;

          then

           A23: (s . i) = (tt . i) by A3, FINSEQ_1:def 7;

          

           A24: (tt . (i + 1)) = (( apply (v1,t)) . (i + 1)) by A1, A20, FINSEQ_1:def 7;

          

           A25: (tt . i) = (( apply (v1,t)) . i) by A1, A22, FINSEQ_1:def 7;

          

           A26: i in ( dom v1) by A16, A18, FINSEQ_3: 25;

          then (p . i) = (v1 . i) by FINSEQ_1:def 7;

          hence (s . (i + 1)) = (a ast t9) by A14, A15, A26, A23, A25, A21, A24, Def19;

        end;

          suppose

           A27: i = ( len v1);

          1 <= ( len ( apply (v2,(v1 ast t)))) by A12, NAT_1: 11;

          then 1 in ( dom ( apply (v2,(v1 ast t)))) by FINSEQ_3: 25;

          then

           A28: (s . (i + 1)) = (( apply (v2,(v1 ast t))) . 1) by A3, A4, A27, FINSEQ_1:def 7;

          

           A29: i in ( dom tt) by A4, A16, A27, FINSEQ_3: 25;

          then

           A30: (s . i) = (tt . i) by A3, FINSEQ_1:def 7;

          

           A31: (tt . i) = (( apply (v1,t)) . i) by A1, A29, FINSEQ_1:def 7;

          

           A32: i in ( dom v1) by A16, A27, FINSEQ_3: 25;

          then (p . i) = (v1 . i) by FINSEQ_1:def 7;

          then (a ast t9) = (v1 ast t) by A14, A15, A27, A32, A30, A31, Def19;

          hence (s . (i + 1)) = (a ast t9) by A28, Def19;

        end;

          suppose i > ( len v1);

          then i >= (( len v1) + 1) by NAT_1: 13;

          then

          consider j be Nat such that

           A33: i = ((( len v1) + 1) + j) by NAT_1: 10;

          

           A34: ((1 + j) + 1) >= 1 by NAT_1: 11;

          

           A35: (((j + 1) + ( len v1)) + 1) = (((j + 1) + 1) + ( len v1));

          

           A36: (1 + j) >= 1 by NAT_1: 11;

          

           A37: i = ((j + 1) + ( len v1)) by A33;

          then

           A38: (1 + j) <= ( len v2) by A17, A11, XREAL_1: 6;

          then ((1 + j) + 0 ) <= (( len v2) + 1) by XREAL_1: 7;

          then (j + 1) in ( dom ( apply (v2,(v1 ast t)))) by A12, A36, FINSEQ_3: 25;

          then

           A39: (s . i) = (( apply (v2,(v1 ast t))) . (j + 1)) by A3, A4, A37, FINSEQ_1:def 7;

          ((1 + j) + 1) <= (( len v2) + 1) by A38, XREAL_1: 7;

          then ((j + 1) + 1) in ( dom ( apply (v2,(v1 ast t)))) by A12, A34, FINSEQ_3: 25;

          then

           A40: (s . (i + 1)) = (( apply (v2,(v1 ast t))) . ((j + 1) + 1)) by A3, A4, A33, A35, FINSEQ_1:def 7;

          

           A41: (j + 1) in ( dom v2) by A36, A38, FINSEQ_3: 25;

          then (p . i) = (v2 . (j + 1)) by A37, FINSEQ_1:def 7;

          hence (s . (i + 1)) = (a ast t9) by A14, A15, A41, A39, A40, Def19;

        end;

      end;

      ( len ( apply (v2,(v1 ast t)))) = (( len v2) + 1) by Def19;

      

      then ( len s) = (( len tt) + (( len v2) + 1)) by A3, FINSEQ_1: 22

      .= ((( len v1) + ( len v2)) + 1) by A4

      .= (( len p) + 1) by FINSEQ_1: 22;

      hence thesis by A3, A5, A10, Def19;

    end;

    theorem :: ABCMIZ_0:35

    

     Th35: for T be non empty non void reflexive transitive TA-structure holds for t be type of T holds for v1,v2 be FinSequence of the adjectives of T holds for i be Nat st i in ( dom v1) holds (( apply ((v1 ^ v2),t)) . i) = (( apply (v1,t)) . i)

    proof

      let T be non empty non void reflexive transitive TA-structure;

      let t be type of T;

      let v1,v2 be FinSequence of the adjectives of T;

      set v = (v1 ^ v2);

      consider tt be FinSequence of the carrier of T, q be Element of T such that

       A1: ( apply (v1,t)) = (tt ^ <*q*>) by HILBERT2: 4;

      let i be Nat;

      

       A2: ( len ( apply (v1,t))) = (( len v1) + 1) by Def19;

      assume

       A3: i in ( dom v1);

      then

       A4: i >= 1 by FINSEQ_3: 25;

      ( len <*q*>) = 1 by FINSEQ_1: 39;

      then (( len v1) + 1) = (( len tt) + 1) by A2, A1, FINSEQ_1: 22;

      then i <= ( len tt) by A3, FINSEQ_3: 25;

      then

       A5: i in ( dom tt) by A4, FINSEQ_3: 25;

      ( apply (v,t)) = (( apply (v1,t)) $^ ( apply (v2,(v1 ast t)))) by Th34

      .= (tt ^ ( apply (v2,(v1 ast t)))) by A1, REWRITE1: 2;

      then (( apply (v,t)) . i) = (tt . i) by A5, FINSEQ_1:def 7;

      hence thesis by A1, A5, FINSEQ_1:def 7;

    end;

    theorem :: ABCMIZ_0:36

    

     Th36: for T be non empty non void reflexive transitive TA-structure holds for t be type of T holds for v1,v2 be FinSequence of the adjectives of T holds (( apply ((v1 ^ v2),t)) . (( len v1) + 1)) = (v1 ast t)

    proof

      let T be non empty non void reflexive transitive TA-structure;

      let t be type of T;

      let v1,v2 be FinSequence of the adjectives of T;

      set v = (v1 ^ v2);

      

       A1: ( len ( apply (v2,(v1 ast t)))) = (( len v2) + 1) by Def19;

      

       A2: ( apply (v,t)) = (( apply (v1,t)) $^ ( apply (v2,(v1 ast t)))) by Th34;

      ( len ( apply (v1,t))) = (( len v1) + 1) by Def19;

      then (( apply (v,t)) . ((( len v1) + 1) + 0 )) = (( apply (v2,(v1 ast t))) . ( 0 + 1)) by A1, A2, Th33;

      hence thesis by Def19;

    end;

    theorem :: ABCMIZ_0:37

    

     Th37: for T be non empty non void reflexive transitive TA-structure holds for t be type of T holds for v1,v2 be FinSequence of the adjectives of T holds (v2 ast (v1 ast t)) = ((v1 ^ v2) ast t)

    proof

      let T be non empty non void reflexive transitive TA-structure;

      let t be type of T;

      let v1,v2 be FinSequence of the adjectives of T;

      set v = (v1 ^ v2);

      consider tt be FinSequence of the carrier of T, q be Element of T such that

       A1: ( apply (v1,t)) = (tt ^ <*q*>) by HILBERT2: 4;

      

       A2: ( len ( apply (v1,t))) = (( len v1) + 1) by Def19;

      ( len <*q*>) = 1 by FINSEQ_1: 39;

      then

       A3: (( len v1) + 1) = (( len tt) + 1) by A2, A1, FINSEQ_1: 22;

      

       A4: (( len v2) + 1) >= 1 by NAT_1: 11;

      ( len ( apply (v2,(v1 ast t)))) = (( len v2) + 1) by Def19;

      then

       A5: (( len v2) + 1) in ( dom ( apply (v2,(v1 ast t)))) by A4, FINSEQ_3: 25;

      ( apply (v,t)) = (( apply (v1,t)) $^ ( apply (v2,(v1 ast t)))) by Th34

      .= (tt ^ ( apply (v2,(v1 ast t)))) by A1, REWRITE1: 2;

      

      hence (v2 ast (v1 ast t)) = (( apply (v,t)) . (( len tt) + (( len v2) + 1))) by A5, FINSEQ_1:def 7

      .= (( apply (v,t)) . ((( len v1) + ( len v2)) + 1)) by A3

      .= (v ast t) by FINSEQ_1: 22;

    end;

    definition

      let T be non empty non void reflexive transitive TA-structure;

      let t be type of T;

      let v be FinSequence of the adjectives of T;

      :: ABCMIZ_0:def21

      pred v is_applicable_to t means for i be Nat, a be adjective of T, s be type of T st i in ( dom v) & a = (v . i) & s = (( apply (v,t)) . i) holds a is_applicable_to s;

    end

    theorem :: ABCMIZ_0:38

    for T be non empty non void reflexive transitive TA-structure holds for t be type of T holds ( <*> the adjectives of T) is_applicable_to t;

    theorem :: ABCMIZ_0:39

    for T be non empty non void reflexive transitive TA-structure holds for t be type of T, a be adjective of T holds a is_applicable_to t iff <*a*> is_applicable_to t

    proof

      let T be non empty non void reflexive transitive TA-structure;

      let t be type of T;

      let a be adjective of T;

      set v = <*a*>;

      

       A1: (v . 1) = a by FINSEQ_1: 40;

      hereby

        assume

         A2: a is_applicable_to t;

        thus <*a*> is_applicable_to t

        proof

          let i be Nat, b be adjective of T, s be type of T;

          assume i in ( dom v);

          then i in ( Seg 1) by FINSEQ_1: 38;

          then

           A3: i = 1 by FINSEQ_1: 2, TARSKI:def 1;

          then (v . i) = a by FINSEQ_1: 40;

          hence thesis by A2, A3, Def19;

        end;

      end;

      assume

       A4: for i be Nat, a9 be adjective of T, s be type of T st i in ( dom v) & a9 = (v . i) & s = (( apply (v,t)) . i) holds a9 is_applicable_to s;

      ( len v) = 1 by FINSEQ_1: 40;

      then

       A5: 1 in ( dom v) by FINSEQ_3: 25;

      (( apply (v,t)) . 1) = t by Def19;

      hence thesis by A4, A5, A1;

    end;

    theorem :: ABCMIZ_0:40

    

     Th40: for T be non empty non void reflexive transitive TA-structure holds for t be type of T holds for v1,v2 be FinSequence of the adjectives of T st (v1 ^ v2) is_applicable_to t holds v1 is_applicable_to t & v2 is_applicable_to (v1 ast t)

    proof

      let T be non empty non void reflexive transitive TA-structure;

      let t be type of T;

      let v1,v2 be FinSequence of the adjectives of T;

      set v = (v1 ^ v2);

      

       A1: ( apply (v,t)) = (( apply (v1,t)) $^ ( apply (v2,(v1 ast t)))) by Th34;

      

       A2: ( len ( apply (v2,(v1 ast t)))) = (( len v2) + 1) by Def19;

      assume

       A3: for i be Nat, a be adjective of T, s be type of T st i in ( dom v) & a = (v . i) & s = (( apply (v,t)) . i) holds a is_applicable_to s;

      hereby

        

         A4: ( dom v1) c= ( dom v) by FINSEQ_1: 26;

        let i be Nat, a be adjective of T, s be type of T such that

         A5: i in ( dom v1) and

         A6: a = (v1 . i) and

         A7: s = (( apply (v1,t)) . i);

        

         A8: a = (v . i) by A5, A6, FINSEQ_1:def 7;

        s = (( apply (v,t)) . i) by A5, A7, Th35;

        hence a is_applicable_to s by A3, A5, A4, A8;

      end;

      let i be Nat, a be adjective of T, s be type of T such that

       A9: i in ( dom v2) and

       A10: a = (v2 . i) and

       A11: s = (( apply (v2,(v1 ast t))) . i);

      

       A12: a = (v . (( len v1) + i)) by A9, A10, FINSEQ_1:def 7;

      i >= 1 by A9, FINSEQ_3: 25;

      then

      consider j be Nat such that

       A13: i = (1 + j) by NAT_1: 10;

      i <= ( len v2) by A9, FINSEQ_3: 25;

      then j < ( len v2) by A13, NAT_1: 13;

      then

       A14: j < ( len ( apply (v2,(v1 ast t)))) by A2, NAT_1: 13;

      ( len ( apply (v1,t))) = (( len v1) + 1) by Def19;

      then (( len v1) + i) = (( len ( apply (v1,t))) + j) by A13;

      then s = (( apply (v,t)) . (( len v1) + i)) by A11, A1, A13, A14, Th33;

      hence thesis by A3, A9, A12, FINSEQ_1: 28;

    end;

    theorem :: ABCMIZ_0:41

    

     Th41: for T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema non void TA-structure holds for t be type of T holds for v be FinSequence of the adjectives of T st v is_applicable_to t holds for i1,i2 be Nat st 1 <= i1 & i1 <= i2 & i2 <= (( len v) + 1) holds for t1,t2 be type of T st t1 = (( apply (v,t)) . i1) & t2 = (( apply (v,t)) . i2) holds t2 <= t1

    proof

      let T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema non void TA-structure;

      let t be type of T;

      let v be FinSequence of the adjectives of T such that

       A1: for i be Nat, a be adjective of T, s be type of T st i in ( dom v) & a = (v . i) & s = (( apply (v,t)) . i) holds a is_applicable_to s;

      let i1,i2 be Nat such that

       A2: 1 <= i1 and

       A3: i1 <= i2 and

       A4: i2 <= (( len v) + 1);

      consider j be Nat such that

       A5: i2 = (i1 + j) by A3, NAT_1: 10;

      let s1,s2 be type of T;

      defpred P[ Nat] means (i1 + $1) <= ( len ( apply (v,t))) implies for s be type of T st s = (( apply (v,t)) . (i1 + $1)) holds s <= s1;

      

       A6: ( len ( apply (v,t))) = (( len v) + 1) by Def19;

      

       A7: for i be Nat st P[i] holds P[(i + 1)]

      proof

        let i be Nat such that

         A8: P[i] and

         A9: (i1 + (i + 1)) <= ( len ( apply (v,t)));

        i1 <= (i1 + i) by NAT_1: 11;

        then

         A10: 1 <= (i1 + i) by A2, XXREAL_0: 2;

        

         A11: (i1 + (i + 1)) = ((i1 + i) + 1);

        then (i1 + i) <= ( len v) by A6, A9, XREAL_1: 6;

        then

         A12: (i1 + i) in ( dom v) by A10, FINSEQ_3: 25;

        then (v . (i1 + i)) in ( rng v) by FUNCT_1: 3;

        then

        reconsider a = (v . (i1 + i)) as adjective of T;

        (i1 + i) < (( len v) + 1) by A6, A9, A11, NAT_1: 13;

        then (i1 + i) in ( dom ( apply (v,t))) by A6, A10, FINSEQ_3: 25;

        then (( apply (v,t)) . (i1 + i)) in ( rng ( apply (v,t))) by FUNCT_1: 3;

        then

        reconsider s = (( apply (v,t)) . (i1 + i)) as type of T;

        

         A13: (( apply (v,t)) . ((i1 + i) + 1)) = (a ast s) by A12, Def19;

        

         A14: (a ast s) <= s by A1, A12, Th20;

        s <= s1 by A8, A9, A11, NAT_1: 13;

        hence thesis by A13, A14, YELLOW_0:def 2;

      end;

      assume that

       A15: s1 = (( apply (v,t)) . i1) and

       A16: s2 = (( apply (v,t)) . i2);

      

       A17: P[ 0 ] by A15;

      for i be Nat holds P[i] from NAT_1:sch 2( A17, A7);

      hence thesis by A4, A5, A6, A16;

    end;

    theorem :: ABCMIZ_0:42

    

     Th42: for T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema non void TA-structure holds for t be type of T holds for v be FinSequence of the adjectives of T st v is_applicable_to t holds for s be type of T st s in ( rng ( apply (v,t))) holds (v ast t) <= s & s <= t

    proof

      let T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema non void TA-structure;

      let t be type of T;

      let v be FinSequence of the adjectives of T such that

       A1: v is_applicable_to t;

      

       A2: ( len ( apply (v,t))) = (( len v) + 1) by Def19;

      let s be type of T;

      assume s in ( rng ( apply (v,t)));

      then

      consider x be object such that

       A3: x in ( dom ( apply (v,t))) and

       A4: s = (( apply (v,t)) . x) by FUNCT_1:def 3;

      reconsider x as Element of NAT by A3;

      

       A5: x <= ( len ( apply (v,t))) by A3, FINSEQ_3: 25;

      

       A6: (( apply (v,t)) . 1) = t by Def19;

      x >= 1 by A3, FINSEQ_3: 25;

      hence thesis by A1, A4, A5, A2, A6, Th41;

    end;

    theorem :: ABCMIZ_0:43

    

     Th43: for T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema non void TA-structure holds for t be type of T holds for v be FinSequence of the adjectives of T st v is_applicable_to t holds (v ast t) <= t

    proof

      let T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema non void TA-structure;

      let t be type of T;

      let v be FinSequence of the adjectives of T such that

       A1: v is_applicable_to t;

      

       A2: (( len v) + 1) >= 1 by NAT_1: 11;

      ( len ( apply (v,t))) = (( len v) + 1) by Def19;

      then (( len v) + 1) in ( dom ( apply (v,t))) by A2, FINSEQ_3: 25;

      then (( apply (v,t)) . (( len v) + 1)) in ( rng ( apply (v,t))) by FUNCT_1: 3;

      hence thesis by A1, Th42;

    end;

    theorem :: ABCMIZ_0:44

    

     Th44: for T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema non void TA-structure holds for t be type of T holds for v be FinSequence of the adjectives of T st v is_applicable_to t holds ( rng v) c= ( adjs (v ast t))

    proof

      let T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema non void TA-structure;

      let t be type of T;

      let v be FinSequence of the adjectives of T such that

       A1: v is_applicable_to t;

      let a be object;

      assume

       A2: a in ( rng v);

      then

      consider x be object such that

       A3: x in ( dom v) and

       A4: a = (v . x) by FUNCT_1:def 3;

      reconsider a as adjective of T by A2;

      reconsider x as Element of NAT by A3;

      

       A5: x >= 1 by A3, FINSEQ_3: 25;

      then

       A6: (x + 1) >= 1 by NAT_1: 13;

      

       A7: ( len ( apply (v,t))) = (( len v) + 1) by Def19;

      

       A8: x <= ( len v) by A3, FINSEQ_3: 25;

      then (x + 1) <= ( len ( apply (v,t))) by A7, XREAL_1: 6;

      then (x + 1) in ( dom ( apply (v,t))) by A6, FINSEQ_3: 25;

      then

       A9: (( apply (v,t)) . (x + 1)) in ( rng ( apply (v,t))) by FUNCT_1: 3;

      x < ( len ( apply (v,t))) by A8, A7, NAT_1: 13;

      then x in ( dom ( apply (v,t))) by A5, FINSEQ_3: 25;

      then (( apply (v,t)) . x) in ( rng ( apply (v,t))) by FUNCT_1: 3;

      then

      reconsider s = (( apply (v,t)) . x) as type of T;

      (a ast s) = (( apply (v,t)) . (x + 1)) by A3, A4, Def19;

      then (a ast s) >= (v ast t) by A1, A9, Th42;

      then

       A10: ( adjs (a ast s)) c= ( adjs (v ast t)) by Th10;

      a is_applicable_to s by A1, A3, A4;

      then a in ( adjs (a ast s)) by Th21;

      hence thesis by A10;

    end;

    theorem :: ABCMIZ_0:45

    

     Th45: for T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema non void TA-structure holds for t be type of T holds for v be FinSequence of the adjectives of T st v is_applicable_to t holds for A be Subset of the adjectives of T st A = ( rng v) holds A is_applicable_to t

    proof

      let T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema non void TA-structure;

      let t be type of T;

      let v be FinSequence of the adjectives of T;

      assume

       A1: v is_applicable_to t;

      then

       A2: ( rng v) c= ( adjs (v ast t)) by Th44;

      (v ast t) <= t by A1, Th43;

      hence thesis by A2;

    end;

    theorem :: ABCMIZ_0:46

    

     Th46: for T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema non void TA-structure holds for t be type of T holds for v1,v2 be FinSequence of the adjectives of T st v1 is_applicable_to t & ( rng v2) c= ( rng v1) holds for s be type of T st s in ( rng ( apply (v2,t))) holds (v1 ast t) <= s

    proof

      let T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema non void TA-structure;

      let t be type of T;

      let v,v9 be FinSequence of the adjectives of T such that

       A1: v is_applicable_to t and

       A2: ( rng v9) c= ( rng v);

      defpred P[ Nat] means $1 <= ( len ( apply (v9,t))) implies for s be type of T st s = (( apply (v9,t)) . $1) holds (v ast t) <= s;

      

       A3: for i be non zero Nat st P[i] holds P[(i + 1)]

      proof

        

         A4: ( rng v) c= ( adjs (v ast t)) by A1, Th44;

        let i be non zero Nat such that

         A5: P[i] and

         A6: (i + 1) <= ( len ( apply (v9,t)));

        

         A7: ( 0 + 1) <= i by NAT_1: 13;

        

         A8: ( len ( apply (v9,t))) = (( len v9) + 1) by Def19;

        then i < (( len v9) + 1) by A6, NAT_1: 13;

        then i in ( dom ( apply (v9,t))) by A8, A7, FINSEQ_3: 25;

        then (( apply (v9,t)) . i) in ( rng ( apply (v9,t))) by FUNCT_1: 3;

        then

        reconsider s = (( apply (v9,t)) . i) as type of T;

        

         A9: (v ast t) <= s by A5, A6, NAT_1: 13;

        i <= ( len v9) by A6, A8, XREAL_1: 6;

        then

         A10: i in ( dom v9) by A7, FINSEQ_3: 25;

        then

         A11: (v9 . i) in ( rng v9) by FUNCT_1: 3;

        then

        reconsider a = (v9 . i) as adjective of T;

        

         A12: a in ( rng v) by A2, A11;

        (( apply (v9,t)) . (i + 1)) = (a ast s) by A10, Def19;

        hence thesis by A12, A4, A9, Th23;

      end;

      (( apply (v9,t)) . 1) = t by Def19;

      then

       A13: P[1] by A1, Th43;

      

       A14: for i be non zero Nat holds P[i] from NAT_1:sch 10( A13, A3);

      let s be type of T;

      assume s in ( rng ( apply (v9,t)));

      then

      consider x be object such that

       A15: x in ( dom ( apply (v9,t))) and

       A16: s = (( apply (v9,t)) . x) by FUNCT_1:def 3;

      

       A17: x in ( Seg ( len ( apply (v9,t)))) by A15, FINSEQ_1:def 3;

      reconsider x as Element of NAT by A15;

      reconsider x as non zero Element of NAT by A17, FINSEQ_1: 1;

      x <= ( len ( apply (v9,t))) by A15, FINSEQ_3: 25;

      hence thesis by A16, A14;

    end;

    theorem :: ABCMIZ_0:47

    

     Th47: for T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema non void TA-structure holds for t be type of T holds for v1,v2 be FinSequence of the adjectives of T st (v1 ^ v2) is_applicable_to t holds (v2 ^ v1) is_applicable_to t

    proof

      let T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema non void TA-structure;

      let t be type of T;

      let v1,v2 be FinSequence of the adjectives of T;

      

       A1: ( rng (v1 ^ v2)) = (( rng v1) \/ ( rng v2)) by FINSEQ_1: 31;

      assume

       A2: (v1 ^ v2) is_applicable_to t;

      then

       A3: ( rng (v1 ^ v2)) c= ( adjs ((v1 ^ v2) ast t)) by Th44;

      let i be Nat, a be adjective of T, s be type of T such that

       A4: i in ( dom (v2 ^ v1)) and

       A5: a = ((v2 ^ v1) . i) and

       A6: s = (( apply ((v2 ^ v1),t)) . i);

      

       A7: a in ( rng (v2 ^ v1)) by A4, A5, FUNCT_1: 3;

      

       A8: ( len ( apply ((v2 ^ v1),t))) = (( len (v2 ^ v1)) + 1) by Def19;

      

       A9: ( rng (v2 ^ v1)) = (( rng v1) \/ ( rng v2)) by FINSEQ_1: 31;

      i <= ( len (v2 ^ v1)) by A4, FINSEQ_3: 25;

      then

       A10: i < (( len (v2 ^ v1)) + 1) by NAT_1: 13;

      i >= 1 by A4, FINSEQ_3: 25;

      then i in ( dom ( apply ((v2 ^ v1),t))) by A10, A8, FINSEQ_3: 25;

      then s in ( rng ( apply ((v2 ^ v1),t))) by A6, FUNCT_1: 3;

      then ((v1 ^ v2) ast t) <= s by A2, A1, A9, Th46;

      hence thesis by A1, A9, A7, A3, Th23;

    end;

    theorem :: ABCMIZ_0:48

    for T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema non void TA-structure holds for t be type of T holds for v1,v2 be FinSequence of the adjectives of T st (v1 ^ v2) is_applicable_to t holds ((v1 ^ v2) ast t) = ((v2 ^ v1) ast t)

    proof

      let T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema non void TA-structure;

      let t be type of T;

      let v1,v2 be FinSequence of the adjectives of T;

      assume

       A1: (v1 ^ v2) is_applicable_to t;

      

       A2: ( len (v1 ^ v2)) = (( len v1) + ( len v2)) by FINSEQ_1: 22;

      

       A3: ( rng (v1 ^ v2)) = (( rng v1) \/ ( rng v2)) by FINSEQ_1: 31;

      

       A4: ( len (v2 ^ v1)) = (( len v1) + ( len v2)) by FINSEQ_1: 22;

      

       A5: (( len (v1 ^ v2)) + 1) >= 1 by NAT_1: 11;

      

       A6: ( rng (v2 ^ v1)) = (( rng v1) \/ ( rng v2)) by FINSEQ_1: 31;

      ( len ( apply ((v2 ^ v1),t))) = (( len (v2 ^ v1)) + 1) by Def19;

      then (( len (v1 ^ v2)) + 1) in ( dom ( apply ((v2 ^ v1),t))) by A2, A4, A5, FINSEQ_3: 25;

      then ((v2 ^ v1) ast t) in ( rng ( apply ((v2 ^ v1),t))) by A2, A4, FUNCT_1: 3;

      then

       A7: ((v1 ^ v2) ast t) <= ((v2 ^ v1) ast t) by A1, A3, A6, Th46;

      ( len ( apply ((v1 ^ v2),t))) = (( len (v1 ^ v2)) + 1) by Def19;

      then (( len (v1 ^ v2)) + 1) in ( dom ( apply ((v1 ^ v2),t))) by A5, FINSEQ_3: 25;

      then ((v1 ^ v2) ast t) in ( rng ( apply ((v1 ^ v2),t))) by FUNCT_1: 3;

      then ((v2 ^ v1) ast t) <= ((v1 ^ v2) ast t) by A1, A3, A6, Th46, Th47;

      hence thesis by A7, YELLOW_0:def 3;

    end;

    theorem :: ABCMIZ_0:49

    

     Th49: for T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema TA-structure holds for t be type of T holds for A be Subset of the adjectives of T st A is_applicable_to t holds (A ast t) <= t

    proof

      let T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema TA-structure;

      let t be type of T;

      let a be Subset of the adjectives of T;

      assume a is_applicable_to t;

      then (( types a) /\ ( downarrow t)) is Ideal of T by Th26;

      then ( sup (( types a) /\ ( downarrow t))) in (( types a) /\ ( downarrow t)) by Th1;

      then (a ast t) in ( downarrow t) by XBOOLE_0:def 4;

      hence thesis by WAYBEL_0: 17;

    end;

    theorem :: ABCMIZ_0:50

    

     Th50: for T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema TA-structure holds for t be type of T holds for A be Subset of the adjectives of T st A is_applicable_to t holds A c= ( adjs (A ast t))

    proof

      let T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema TA-structure;

      let t be type of T;

      let a be Subset of the adjectives of T;

      assume a is_applicable_to t;

      then (( types a) /\ ( downarrow t)) is Ideal of T by Th26;

      then ( sup (( types a) /\ ( downarrow t))) in (( types a) /\ ( downarrow t)) by Th1;

      then (a ast t) in ( types a) by XBOOLE_0:def 4;

      hence thesis by Th14;

    end;

    theorem :: ABCMIZ_0:51

    for T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema TA-structure holds for t be type of T holds for A be Subset of the adjectives of T st A is_applicable_to t holds (A ast t) in ( types A)

    proof

      let T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema TA-structure;

      let t be type of T;

      let a be Subset of the adjectives of T;

      assume a is_applicable_to t;

      then (( types a) /\ ( downarrow t)) is Ideal of T by Th26;

      then ( sup (( types a) /\ ( downarrow t))) in (( types a) /\ ( downarrow t)) by Th1;

      hence thesis by XBOOLE_0:def 4;

    end;

    theorem :: ABCMIZ_0:52

    

     Th52: for T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema TA-structure holds for t be type of T holds for A be Subset of the adjectives of T holds for t9 be type of T st t9 <= t & A c= ( adjs t9) holds A is_applicable_to t & t9 <= (A ast t)

    proof

      let T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema TA-structure;

      let t be type of T;

      let a be Subset of the adjectives of T;

      let t9 be type of T;

      assume that

       A1: t9 <= t and

       A2: a c= ( adjs t9);

      

       A3: t9 in ( downarrow t) by A1, WAYBEL_0: 17;

      thus a is_applicable_to t by A1, A2;

      then (( types a) /\ ( downarrow t)) is Ideal of T by Th26;

      then ex_sup_of ((( types a) /\ ( downarrow t)),T) by Th1;

      then

       A4: (a ast t) is_>=_than (( types a) /\ ( downarrow t)) by YELLOW_0: 30;

      t9 in ( types a) by A2, Th14;

      then t9 in (( types a) /\ ( downarrow t)) by A3, XBOOLE_0:def 4;

      hence thesis by A4;

    end;

    theorem :: ABCMIZ_0:53

    for T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema TA-structure holds for t be type of T holds for A be Subset of the adjectives of T st A c= ( adjs t) holds A is_applicable_to t & (A ast t) = t

    proof

      let T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema TA-structure;

      let t be type of T;

      let a be Subset of the adjectives of T;

      assume

       A1: a c= ( adjs t);

      hence a is_applicable_to t by Th52;

      then

       A2: (a ast t) <= t by Th49;

      t <= (a ast t) by A1, Th52;

      hence thesis by A2, YELLOW_0:def 3;

    end;

    theorem :: ABCMIZ_0:54

    

     Th54: for T be TA-structure, t be type of T holds for A,B be Subset of the adjectives of T st A is_applicable_to t & B c= A holds B is_applicable_to t

    proof

      let T be TA-structure;

      let t be type of T;

      let A,B be Subset of the adjectives of T;

      given t9 be type of T such that

       A1: A c= ( adjs t9) and

       A2: t9 <= t;

      assume

       A3: B c= A;

      take t9;

      thus thesis by A1, A2, A3;

    end;

    theorem :: ABCMIZ_0:55

    

     Th55: for T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema non void TA-structure holds for t be type of T, a be adjective of T holds for A,B be Subset of the adjectives of T st B = (A \/ {a}) & B is_applicable_to t holds (a ast (A ast t)) = (B ast t)

    proof

      let T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema non void TA-structure;

      let t be type of T, a be adjective of T;

      let A,B be Subset of the adjectives of T such that

       A1: B = (A \/ {a}) and

       A2: B is_applicable_to t;

      

       A3: A is_applicable_to t by A1, A2, Th54, XBOOLE_1: 7;

      

       A4: {a} c= B by A1, XBOOLE_1: 7;

      

       A5: A c= B by A1, XBOOLE_1: 7;

      (( types a) /\ ( downarrow (A ast t))) = (( types B) /\ ( downarrow t))

      proof

        thus (( types a) /\ ( downarrow (A ast t))) c= (( types B) /\ ( downarrow t))

        proof

          let x be object;

          assume

           A6: x in (( types a) /\ ( downarrow (A ast t)));

          then

          reconsider t9 = x as type of T;

          x in ( types a) by A6, XBOOLE_0:def 4;

          then a in ( adjs t9) by Th13;

          then

           A7: {a} c= ( adjs t9) by ZFMISC_1: 31;

          x in ( downarrow (A ast t)) by A6, XBOOLE_0:def 4;

          then

           A8: t9 <= (A ast t) by WAYBEL_0: 17;

          then

           A9: ( adjs (A ast t)) c= ( adjs t9) by Th10;

          (A ast t) <= t by A3, Th49;

          then t9 <= t by A8, YELLOW_0:def 2;

          then

           A10: t9 in ( downarrow t) by WAYBEL_0: 17;

          A c= ( adjs (A ast t)) by A3, Th50;

          then A c= ( adjs t9) by A9;

          then B c= ( adjs t9) by A1, A7, XBOOLE_1: 8;

          then t9 in ( types B) by Th14;

          hence thesis by A10, XBOOLE_0:def 4;

        end;

        let x be object;

        assume

         A11: x in (( types B) /\ ( downarrow t));

        then

        reconsider t9 = x as type of T;

        x in ( downarrow t) by A11, XBOOLE_0:def 4;

        then

         A12: t9 <= t by WAYBEL_0: 17;

        x in ( types B) by A11, XBOOLE_0:def 4;

        then

         A13: B c= ( adjs t9) by Th14;

        then A c= ( adjs t9) by A5;

        then t9 <= (A ast t) by A12, Th52;

        then

         A14: t9 in ( downarrow (A ast t)) by WAYBEL_0: 17;

        a in B by A4, ZFMISC_1: 31;

        then t9 in ( types a) by A13, Th13;

        hence thesis by A14, XBOOLE_0:def 4;

      end;

      hence thesis;

    end;

    theorem :: ABCMIZ_0:56

    

     Th56: for T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema non void TA-structure holds for t be type of T holds for v be FinSequence of the adjectives of T st v is_applicable_to t holds for A be Subset of the adjectives of T st A = ( rng v) holds (v ast t) = (A ast t)

    proof

      let T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema non void TA-structure;

      defpred P[ Nat] means for t be type of T, v be FinSequence of the adjectives of T st $1 = ( len v) & v is_applicable_to t holds for A be Subset of the adjectives of T st A = ( rng v) holds (v ast t) = (A ast t);

      let t be type of T;

      let v be FinSequence of the adjectives of T;

       A1:

      now

        let n be Nat such that

         A2: P[n];

        now

          let t be type of T, v be FinSequence of the adjectives of T such that

           A3: (n + 1) = ( len v) and

           A4: v is_applicable_to t;

          consider v1 be FinSequence of the adjectives of T, a be Element of the adjectives of T such that

           A5: v = (v1 ^ <*a*>) by A3, FINSEQ_2: 19;

          reconsider B = ( rng v1) as Subset of the adjectives of T;

          reconsider a as adjective of T;

          ( len <*a*>) = 1 by FINSEQ_1: 40;

          then

           A6: ( len v) = (( len v1) + 1) by A5, FINSEQ_1: 22;

          v1 is_applicable_to t by A4, A5, Th40;

          then

           A7: (v1 ast t) = (B ast t) by A2, A3, A6;

          let A be Subset of the adjectives of T;

          assume

           A8: A = ( rng v);

          

          then

           A9: A = (B \/ ( rng <*a*>)) by A5, FINSEQ_1: 31

          .= (B \/ {a}) by FINSEQ_1: 38;

          

          thus (v ast t) = ( <*a*> ast (v1 ast t)) by A5, Th37

          .= (a ast (B ast t)) by A7, Th31

          .= (A ast t) by A4, A8, A9, Th45, Th55;

        end;

        hence P[(n + 1)];

      end;

      

       A10: P[ 0 ]

      proof

        let t be type of T;

        let v be FinSequence of the adjectives of T;

        assume

         A11: 0 = ( len v);

        then v = ( <*> the adjectives of T);

        then

         A12: ( rng v) = ( {} the adjectives of T);

        (v ast t) = t by A11, Def19;

        hence thesis by A12, Th27;

      end;

      for n be Nat holds P[n] from NAT_1:sch 2( A10, A1);

      hence thesis;

    end;

    begin

    definition

      let T be non empty non void TA-structure;

      :: ABCMIZ_0:def22

      func sub T -> Function of the adjectives of T, the carrier of T means

      : Def22: for a be adjective of T holds (it . a) = ( sup (( types a) \/ ( types ( non- a))));

      existence

      proof

        deffunc F( Element of the adjectives of T) = ( sup (( types $1) \/ ( types ( non- $1))));

        consider f be Function of the adjectives of T, the carrier of T such that

         A1: for a be Element of the adjectives of T holds (f . a) = F(a) from FUNCT_2:sch 4;

        take f;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let f1,f2 be Function of the adjectives of T, the carrier of T such that

         A2: for a be adjective of T holds (f1 . a) = ( sup (( types a) \/ ( types ( non- a)))) and

         A3: for a be adjective of T holds (f2 . a) = ( sup (( types a) \/ ( types ( non- a))));

        now

          let a be Element of the adjectives of T;

          reconsider b = a as adjective of T;

          

          thus (f1 . a) = ( sup (( types b) \/ ( types ( non- b)))) by A2

          .= (f2 . a) by A3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    definition

      struct ( TA-structure) TAS-structure (# the carrier, adjectives -> set,

the InternalRel -> Relation of the carrier,

the non-op -> UnOp of the adjectives,

the adj-map -> Function of the carrier, ( Fin the adjectives),

the sub-map -> Function of the adjectives, the carrier #)

       attr strict strict;

    end

    registration

      cluster non void reflexive1 -element strict for TAS-structure;

      existence

      proof

        set P = the non void reflexive1 -element TA-structure;

        set s = the Function of the adjectives of P, the carrier of P;

        take T = TAS-structure (# the carrier of P, the adjectives of P, the InternalRel of P, the non-op of P, the adj-map of P, s #);

         the RelStr of P = the RelStr of T;

        hence thesis by STRUCT_0:def 19, WAYBEL_8: 12;

      end;

    end

    definition

      let T be non empty non void TAS-structure;

      let a be adjective of T;

      :: ABCMIZ_0:def23

      func sub a -> type of T equals (the sub-map of T . a);

      coherence ;

    end

    definition

      let T be non empty non void TAS-structure;

      :: ABCMIZ_0:def24

      attr T is non-absorbing means (the sub-map of T * the non-op of T) = the sub-map of T;

      :: ABCMIZ_0:def25

      attr T is subjected means for a be adjective of T holds (( types a) \/ ( types ( non- a))) is_<=_than ( sub a) & (( types a) <> {} & ( types ( non- a)) <> {} implies ( sub a) = ( sup (( types a) \/ ( types ( non- a)))));

    end

    definition

      let T be non empty non void TAS-structure;

      :: original: non-absorbing

      redefine

      :: ABCMIZ_0:def26

      attr T is non-absorbing means for a be adjective of T holds ( sub ( non- a)) = ( sub a);

      compatibility

      proof

        thus T is non-absorbing implies for a be adjective of T holds ( sub ( non- a)) = ( sub a) by FUNCT_2: 15;

        assume

         A1: for a be adjective of T holds ( sub ( non- a)) = ( sub a);

        now

          let x be Element of the adjectives of T;

          reconsider a = x as adjective of T;

          

          thus ((the sub-map of T * the non-op of T) . x) = ( sub ( non- a)) by FUNCT_2: 15

          .= ( sub a) by A1

          .= (the sub-map of T . x);

        end;

        hence (the sub-map of T * the non-op of T) = the sub-map of T by FUNCT_2: 63;

      end;

    end

    definition

      let T be non empty non void TAS-structure;

      let t be Element of T;

      let a be adjective of T;

      :: ABCMIZ_0:def27

      pred a is_properly_applicable_to t means t <= ( sub a) & a is_applicable_to t;

    end

    definition

      let T be non empty non void reflexive transitive TAS-structure;

      let t be type of T;

      let v be FinSequence of the adjectives of T;

      :: ABCMIZ_0:def28

      pred v is_properly_applicable_to t means for i be Nat, a be adjective of T, s be type of T st i in ( dom v) & a = (v . i) & s = (( apply (v,t)) . i) holds a is_properly_applicable_to s;

    end

    theorem :: ABCMIZ_0:57

    

     Th57: for T be non empty non void reflexive transitive TAS-structure holds for t be type of T, v be FinSequence of the adjectives of T st v is_properly_applicable_to t holds v is_applicable_to t

    proof

      let T be non empty non void reflexive transitive TAS-structure;

      let t be type of T;

      let v be FinSequence of the adjectives of T;

      assume

       A1: for i be Nat, a be adjective of T, s be type of T st i in ( dom v) & a = (v . i) & s = (( apply (v,t)) . i) holds a is_properly_applicable_to s;

      let i be Nat, a be adjective of T, s be type of T such that

       A2: i in ( dom v) and

       A3: a = (v . i) and

       A4: s = (( apply (v,t)) . i);

      a is_properly_applicable_to s by A1, A2, A3, A4;

      hence thesis;

    end;

    theorem :: ABCMIZ_0:58

    for T be non empty non void reflexive transitive TAS-structure holds for t be type of T holds ( <*> the adjectives of T) is_properly_applicable_to t;

    theorem :: ABCMIZ_0:59

    for T be non empty non void reflexive transitive TAS-structure holds for t be type of T, a be adjective of T holds a is_properly_applicable_to t iff <*a*> is_properly_applicable_to t

    proof

      let T be non empty non void reflexive transitive TAS-structure;

      let t be type of T;

      let a be adjective of T;

      set v = <*a*>;

      

       A1: (v . 1) = a by FINSEQ_1: 40;

      hereby

        assume

         A2: a is_properly_applicable_to t;

        thus <*a*> is_properly_applicable_to t

        proof

          let i be Nat, b be adjective of T, s be type of T;

          assume i in ( dom v);

          then i in ( Seg 1) by FINSEQ_1: 38;

          then

           A3: i = 1 by FINSEQ_1: 2, TARSKI:def 1;

          then (v . i) = a by FINSEQ_1: 40;

          hence thesis by A2, A3, Def19;

        end;

      end;

      assume

       A4: for i be Nat, a9 be adjective of T, s be type of T st i in ( dom v) & a9 = (v . i) & s = (( apply (v,t)) . i) holds a9 is_properly_applicable_to s;

      ( len v) = 1 by FINSEQ_1: 40;

      then

       A5: 1 in ( dom v) by FINSEQ_3: 25;

      (( apply (v,t)) . 1) = t by Def19;

      hence thesis by A4, A5, A1;

    end;

    theorem :: ABCMIZ_0:60

    

     Th60: for T be non empty non void reflexive transitive TAS-structure holds for t be type of T, v1,v2 be FinSequence of the adjectives of T st (v1 ^ v2) is_properly_applicable_to t holds v1 is_properly_applicable_to t & v2 is_properly_applicable_to (v1 ast t)

    proof

      let T be non empty non void reflexive transitive TAS-structure;

      let t be type of T;

      let v1,v2 be FinSequence of the adjectives of T;

      set v = (v1 ^ v2);

      

       A1: ( apply (v,t)) = (( apply (v1,t)) $^ ( apply (v2,(v1 ast t)))) by Th34;

      

       A2: ( len ( apply (v2,(v1 ast t)))) = (( len v2) + 1) by Def19;

      assume

       A3: for i be Nat, a be adjective of T, s be type of T st i in ( dom v) & a = (v . i) & s = (( apply (v,t)) . i) holds a is_properly_applicable_to s;

      hereby

        

         A4: ( dom v1) c= ( dom v) by FINSEQ_1: 26;

        let i be Nat, a be adjective of T, s be type of T such that

         A5: i in ( dom v1) and

         A6: a = (v1 . i) and

         A7: s = (( apply (v1,t)) . i);

        

         A8: a = (v . i) by A5, A6, FINSEQ_1:def 7;

        s = (( apply (v,t)) . i) by A5, A7, Th35;

        hence a is_properly_applicable_to s by A3, A5, A4, A8;

      end;

      let i be Nat, a be adjective of T, s be type of T such that

       A9: i in ( dom v2) and

       A10: a = (v2 . i) and

       A11: s = (( apply (v2,(v1 ast t))) . i);

      

       A12: a = (v . (( len v1) + i)) by A9, A10, FINSEQ_1:def 7;

      i >= 1 by A9, FINSEQ_3: 25;

      then

      consider j be Nat such that

       A13: i = (1 + j) by NAT_1: 10;

      i <= ( len v2) by A9, FINSEQ_3: 25;

      then j < ( len v2) by A13, NAT_1: 13;

      then

       A14: j < ( len ( apply (v2,(v1 ast t)))) by A2, NAT_1: 13;

      ( len ( apply (v1,t))) = (( len v1) + 1) by Def19;

      then (( len v1) + i) = (( len ( apply (v1,t))) + j) by A13;

      then s = (( apply (v,t)) . (( len v1) + i)) by A11, A1, A13, A14, Th33;

      hence thesis by A3, A9, A12, FINSEQ_1: 28;

    end;

    theorem :: ABCMIZ_0:61

    

     Th61: for T be non empty non void reflexive transitive TAS-structure holds for t be type of T, v1,v2 be FinSequence of the adjectives of T st v1 is_properly_applicable_to t & v2 is_properly_applicable_to (v1 ast t) holds (v1 ^ v2) is_properly_applicable_to t

    proof

      let T be non empty non void reflexive transitive TAS-structure;

      let t be type of T;

      let v1,v2 be FinSequence of the adjectives of T;

      set v = (v1 ^ v2);

      assume

       A1: for i be Nat, a be adjective of T, s be type of T st i in ( dom v1) & a = (v1 . i) & s = (( apply (v1,t)) . i) holds a is_properly_applicable_to s;

      assume

       A2: for i be Nat, a be adjective of T, s be type of T st i in ( dom v2) & a = (v2 . i) & s = (( apply (v2,(v1 ast t))) . i) holds a is_properly_applicable_to s;

      

       A3: ( apply (v,t)) = (( apply (v1,t)) $^ ( apply (v2,(v1 ast t)))) by Th34;

      let i be Nat, a be adjective of T, s be type of T such that

       A4: i in ( dom v) and

       A5: a = (v . i) and

       A6: s = (( apply (v,t)) . i);

      

       A7: i >= 1 by A4, FINSEQ_3: 25;

      

       A8: i <= ( len v) by A4, FINSEQ_3: 25;

      per cases ;

        suppose i <= ( len v1);

        then

         A9: i in ( dom v1) by A7, FINSEQ_3: 25;

        then

         A10: a = (v1 . i) by A5, FINSEQ_1:def 7;

        s = (( apply (v1,t)) . i) by A6, A9, Th35;

        hence thesis by A1, A9, A10;

      end;

        suppose i > ( len v1);

        then i >= (1 + ( len v1)) by NAT_1: 13;

        then

        consider j be Nat such that

         A11: i = ((( len v1) + 1) + j) by NAT_1: 10;

        

         A12: ( len ( apply (v2,(v1 ast t)))) = (( len v2) + 1) by Def19;

        

         A13: ( len v) = (( len v1) + ( len v2)) by FINSEQ_1: 22;

        

         A14: ( len ( apply (v1,t))) = (( len v1) + 1) by Def19;

        i = (( len v1) + (j + 1)) by A11;

        then

         A15: (j + 1) <= ( len v2) by A8, A13, XREAL_1: 6;

        then j < ( len v2) by NAT_1: 13;

        then j < ( len ( apply (v2,(v1 ast t)))) by A12, NAT_1: 13;

        then

         A16: s = (( apply (v2,(v1 ast t))) . (1 + j)) by A6, A3, A11, A14, Th33;

        (j + 1) >= 1 by NAT_1: 11;

        then

         A17: (j + 1) in ( dom v2) by A15, FINSEQ_3: 25;

        (( len v1) + (j + 1)) = (( len ( apply (v1,t))) + j) by A14;

        then a = (v2 . (1 + j)) by A5, A11, A17, FINSEQ_1:def 7;

        hence thesis by A2, A17, A16;

      end;

    end;

    definition

      let T be non empty non void reflexive transitive TAS-structure;

      let t be type of T;

      let A be Subset of the adjectives of T;

      :: ABCMIZ_0:def29

      pred A is_properly_applicable_to t means ex s be FinSequence of the adjectives of T st ( rng s) = A & s is_properly_applicable_to t;

    end

    theorem :: ABCMIZ_0:62

    for T be non empty non void reflexive transitive TAS-structure holds for t be type of T, A be Subset of the adjectives of T st A is_properly_applicable_to t holds A is finite;

    theorem :: ABCMIZ_0:63

    

     Th63: for T be non empty non void reflexive transitive TAS-structure holds for t be type of T holds ( {} the adjectives of T) is_properly_applicable_to t

    proof

      let T be non empty non void reflexive transitive TAS-structure;

      let t be type of T;

      take s = ( <*> the adjectives of T);

      thus ( rng s) = ( {} the adjectives of T);

      let i be Nat;

      thus thesis;

    end;

    scheme :: ABCMIZ_0:sch1

    MinimalFiniteSet { P[ set] } :

ex A be finite set st P[A] & for B be set st B c= A & P[B] holds B = A

      provided

       A1: ex A be finite set st P[A];

      consider A be finite set such that

       A2: P[A] by A1;

      defpred R[ set, set] means $1 c= $2;

      consider Y be set such that

       A3: for x be set holds x in Y iff x in ( bool A) & P[x] from XFAMILY:sch 1;

      A c= A;

      then

      reconsider Y as non empty set by A2, A3;

      Y c= ( bool A) by A3;

      then

      reconsider Y as finite non empty set;

      

       A4: for x,y be Element of Y st R[x, y] & R[y, x] holds x = y;

      

       A5: for x,y,z be Element of Y st R[x, y] & R[y, z] holds R[x, z] by XBOOLE_1: 1;

      

       A6: for X be set st X c= Y & (for x,y be Element of Y st x in X & y in X holds R[x, y] or R[y, x]) holds ex y be Element of Y st for x be Element of Y st x in X holds R[y, x]

      proof

        let X be set such that

         A7: X c= Y and

         A8: for x,y be Element of Y st x in X & y in X holds R[x, y] or R[y, x];

        per cases ;

          suppose

           A9: X = {} ;

          set y = the Element of Y;

          take y;

          thus thesis by A9;

        end;

          suppose

           A10: X <> {} ;

          set x0 = the Element of X;

          x0 in X by A10;

          then

          reconsider x0 as Element of Y by A7;

          deffunc F( set) = ( card { y where y be Element of Y : y in X & y c< $1 });

          consider f be Function such that

           A11: ( dom f) = X & for x be set st x in X holds (f . x) = F(x) from FUNCT_1:sch 5;

          defpred P[ Nat] means ex x be Element of Y st x in X & $1 = (f . x);

          

           A12: for k be Nat st k <> 0 & P[k] holds ex n be Nat st n < k & P[n]

          proof

            let k be Nat such that

             A13: k <> 0 ;

            given x be Element of Y such that

             A14: x in X and

             A15: k = (f . x);

            set fx = { a where a be Element of Y : a in X & a c< x };

            fx c= Y

            proof

              let a be object;

              assume a in fx;

              then ex z be Element of Y st a = z & z in X & z c< x;

              hence thesis;

            end;

            then

            reconsider fx as finite set;

            

             A16: k = ( card fx) by A11, A14, A15;

            set A = { z where z be Element of Y : z in X & z c< x };

            reconsider A as non empty set by A11, A13, A14, A15, CARD_1: 27;

            set z = the Element of A;

            z in A;

            then

            consider y be Element of Y such that

             A17: z = y and

             A18: y in X and

             A19: y c< x;

            set fx0 = { a where a be Element of Y : a in X & a c< y };

            fx0 c= Y

            proof

              let a be object;

              assume a in fx0;

              then ex z be Element of Y st a = z & z in X & z c< y;

              hence thesis;

            end;

            then

            reconsider fx0 as finite set;

            reconsider n = ( card fx0) as Element of NAT ;

            take n;

             not ex a be Element of Y st y = a & a in X & a c< y;

            then

             A20: not y in fx0;

            

             A21: y in fx by A17;

            

             A22: fx0 c= fx

            proof

              let a be object;

              assume a in fx0;

              then

              consider b be Element of Y such that

               A23: a = b and

               A24: b in X and

               A25: b c< y;

              b c< x by A19, A25, XBOOLE_1: 56;

              hence thesis by A23, A24;

            end;

            then ( Segm ( card fx0)) c= ( Segm ( card fx)) by CARD_1: 11;

            then n <= k by A16, NAT_1: 39;

            hence n < k by A16, A22, A21, A20, CARD_2: 102, XXREAL_0: 1;

            take y;

            thus thesis by A11, A18;

          end;

          set fx0 = { y where y be Element of Y : y in X & y c< x0 };

          fx0 c= Y

          proof

            let a be object;

            assume a in fx0;

            then ex y be Element of Y st a = y & y in X & y c< x0;

            hence thesis;

          end;

          then

          reconsider fx0 as finite set;

          (f . x0) = ( card fx0) by A10, A11;

          then

           A26: ex n be Nat st P[n] by A10;

           P[ 0 ] from NAT_1:sch 7( A26, A12);

          then

          consider y be Element of Y such that

           A27: y in X and

           A28: 0 = (f . y);

          take y;

          let x be Element of Y;

          assume

           A29: x in X;

          then x c= y or y c= x by A8, A27;

          then x c< y or y c= x;

          then

           A30: x in { z where z be Element of Y : z in X & z c< y } or y c= x by A29;

          (f . y) = ( card { z where z be Element of Y : z in X & z c< y }) by A11, A27;

          hence thesis by A28, A30;

        end;

      end;

      

       A31: for x be Element of Y holds R[x, x];

      consider x be Element of Y such that

       A32: for y be Element of Y st x <> y holds not R[y, x] from ORDERS_1:sch 2( A31, A4, A5, A6);

      x in ( bool A) by A3;

      then

      reconsider x as finite set;

      take x;

      thus P[x] by A3;

      let B be set;

      assume that

       A33: B c= x and

       A34: P[B];

      x in ( bool A) by A3;

      then B c= A by A33, XBOOLE_1: 1;

      then B in Y by A3, A34;

      hence thesis by A32, A33;

    end;

    theorem :: ABCMIZ_0:64

    

     Th64: for T be non empty non void reflexive transitive TAS-structure holds for t be type of T, A be Subset of the adjectives of T st A is_properly_applicable_to t holds ex B be Subset of the adjectives of T st B c= A & B is_properly_applicable_to t & (A ast t) = (B ast t) & for C be Subset of the adjectives of T st C c= B & C is_properly_applicable_to t & (A ast t) = (C ast t) holds C = B

    proof

      let T be non empty non void reflexive transitive TAS-structure;

      let t be type of T, A be Subset of the adjectives of T;

      defpred P[ set] means ex B be Subset of the adjectives of T st $1 = B & $1 c= A & B is_properly_applicable_to t & (A ast t) = (B ast t);

      assume

       A1: A is_properly_applicable_to t;

      

       A2: ex a be finite set st P[a] by A1;

      consider B be finite set such that

       A3: P[B] and

       A4: for C be set st C c= B & P[C] holds C = B from MinimalFiniteSet( A2);

      reconsider B as Subset of the adjectives of T by A3;

      take B;

      thus B c= A & B is_properly_applicable_to t & (A ast t) = (B ast t) by A3;

      let C be Subset of the adjectives of T;

      assume

       A5: C c= B;

      then C c= A by A3, XBOOLE_1: 1;

      hence thesis by A4, A5;

    end;

    definition

      let T be non empty non void reflexive transitive TAS-structure;

      :: ABCMIZ_0:def30

      attr T is commutative means

      : Def30: for t1,t2 be type of T, a be adjective of T st a is_properly_applicable_to t1 & (a ast t1) <= t2 holds ex A be finite Subset of the adjectives of T st A is_properly_applicable_to (t1 "\/" t2) & (A ast (t1 "\/" t2)) = t2;

    end

    registration

      cluster Mizar-widening-like involutive without_fixpoints consistent adj-structured adjs-typed non-absorbing subjected commutative for complete upper-bounded non void1 -element reflexive transitive antisymmetric strict TAS-structure;

      existence

      proof

        set P = the non void Mizar-widening-like involutive without_fixpoints consistent adj-structured adjs-typed1 -element reflexive complete strict TA-structure;

        set T = TAS-structure (# the carrier of P, the adjectives of P, the InternalRel of P, the non-op of P, the adj-map of P, ( sub P) #);

         the RelStr of P = the RelStr of T;

        then

        reconsider T as non void1 -element reflexive strict TAS-structure by Def4, STRUCT_0:def 19, WAYBEL_8: 12;

        take T;

        thus T is Mizar-widening-like;

         the AdjectiveStr of P = the AdjectiveStr of T;

        hence T is involutive without_fixpoints by Th5, Th6;

        thus T is consistent adj-structured adjs-typed by Th8, Th9, Th17;

        hereby

          let a be adjective of T;

          reconsider b = a as adjective of P;

          

          thus ( sub ( non- a)) = ( sup (( types ( non- b)) \/ ( types ( non- ( non- b))))) by Def22

          .= ( sup (( types ( non- b)) \/ ( types b))) by Def6

          .= ( sub a) by Def22;

        end;

        

         A1: the RelStr of P = the RelStr of T;

        thus T is subjected

        proof

          let a be adjective of T;

          reconsider b = a as adjective of P;

          

           A2: ( types ( non- a)) = ( types ( non- b)) by Th11;

          ( types a) = ( types b) by Th11;

          then ( sup (( types a) \/ ( types ( non- a)))) = ( sup (( types b) \/ ( types ( non- b)))) by A1, A2, YELLOW_0: 17, YELLOW_0: 26;

          then ( sup (( types a) \/ ( types ( non- a)))) = ( sub a) by Def22;

          hence thesis by YELLOW_0: 32;

        end;

        let t1,t2 be type of T, a be adjective of T such that a is_properly_applicable_to t1 and (a ast t1) <= t2;

        take A = ( {} the adjectives of T);

        thus A is_properly_applicable_to (t1 "\/" t2) by Th63;

        thus (A ast (t1 "\/" t2)) = t2 by STRUCT_0:def 10;

      end;

    end

    theorem :: ABCMIZ_0:65

    

     Th65: for T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema non void TAS-structure holds for t be type of T, A be Subset of the adjectives of T st A is_properly_applicable_to t holds ex s be one-to-one FinSequence of the adjectives of T st ( rng s) = A & s is_properly_applicable_to t

    proof

      let T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema non void TAS-structure;

      let t be type of T, A be Subset of the adjectives of T;

      given s9 be FinSequence of the adjectives of T such that

       A1: ( rng s9) = A and

       A2: s9 is_properly_applicable_to t;

      defpred P[ Nat] means ex s be FinSequence of the adjectives of T st $1 = ( len s) & ( rng s) = A & s is_properly_applicable_to t;

      ( len s9) = ( len s9);

      then

       A3: ex k be Nat st P[k] by A1, A2;

      consider k be Nat such that

       A4: P[k] and

       A5: for n be Nat st P[n] holds k <= n from NAT_1:sch 5( A3);

      consider s be FinSequence of the adjectives of T such that

       A6: k = ( len s) and

       A7: ( rng s) = A and

       A8: s is_properly_applicable_to t by A4;

      s is one-to-one

      proof

        let x,y be object;

        assume that

         A9: x in ( dom s) and

         A10: y in ( dom s) and

         A11: (s . x) = (s . y) and

         A12: x <> y;

        reconsider x, y as Element of NAT by A9, A10;

        x < y or x > y by A12, XXREAL_0: 1;

        then

        consider x,y be Element of NAT such that

         A13: x in ( dom s) and

         A14: y in ( dom s) and

         A15: x < y and

         A16: (s . x) = (s . y) by A9, A10, A11;

        

         A17: x >= 1 by A13, FINSEQ_3: 25;

        y >= 1 by A14, FINSEQ_3: 25;

        then

        consider i be Nat such that

         A18: y = (1 + i) by NAT_1: 10;

        reconsider i as Element of NAT by ORDINAL1:def 12;

        reconsider s1 = (s | ( Seg i)) as FinSequence of the adjectives of T by FINSEQ_1: 18;

        

         A19: y <= ( len s) by A14, FINSEQ_3: 25;

        then i <= ( len s) by A18, NAT_1: 13;

        then

         A20: ( len s1) = i by FINSEQ_1: 17;

        x <= i by A15, A18, NAT_1: 13;

        then

         A21: x in ( dom s1) by A20, A17, FINSEQ_3: 25;

        s1 c= s by TREES_1:def 1;

        then

        consider s2 be FinSequence such that

         A22: s = (s1 ^ s2) by TREES_1: 1;

        reconsider s2 as FinSequence of the adjectives of T by A22, FINSEQ_1: 36;

        

         A23: ( len s) = (( len s1) + ( len s2)) by A22, FINSEQ_1: 22;

        then

         A24: ( len s2) >= 1 by A18, A19, A20, XREAL_1: 6;

        then

         A25: 1 in ( dom s2) by FINSEQ_3: 25;

        reconsider s21 = (s2 | ( Seg 1)) as FinSequence of the adjectives of T by FINSEQ_1: 18;

        s21 c= s2 by TREES_1:def 1;

        then

        consider s22 be FinSequence such that

         A26: s2 = (s21 ^ s22) by TREES_1: 1;

        reconsider s22 as FinSequence of the adjectives of T by A26, FINSEQ_1: 36;

        

         A27: ( len s21) = 1 by A24, FINSEQ_1: 17;

        then

         A28: s21 = <*(s21 . 1)*> by FINSEQ_1: 40;

        then

         A29: ( rng s21) = {(s21 . 1)} by FINSEQ_1: 39;

        then

        reconsider a = (s21 . 1) as adjective of T by ZFMISC_1: 31;

        

         A30: ( rng s2) = (( rng s21) \/ ( rng s22)) by A26, FINSEQ_1: 31;

        a = (s2 . 1) by A28, A26, FINSEQ_1: 41

        .= (s . y) by A18, A22, A20, A25, FINSEQ_1:def 7;

        then a = (s1 . x) by A16, A22, A21, FINSEQ_1:def 7;

        then

         A31: a in ( rng s1) by A21, FUNCT_1: 3;

        then ( rng s21) c= ( rng s1) by A29, ZFMISC_1: 31;

        then (( rng s1) \/ ( rng s21)) = ( rng s1) by XBOOLE_1: 12;

        then

         A32: ( rng (s1 ^ s22)) = ((( rng s1) \/ ( rng s21)) \/ ( rng s22)) by FINSEQ_1: 31;

        

         A33: s2 is_properly_applicable_to (s1 ast t) by A8, A22, Th60;

        

         A34: s1 is_properly_applicable_to t by A8, A22, A23, Th60;

        then ( rng s1) c= ( adjs (s1 ast t)) by Th44, Th57;

        

        then (s1 ast t) = (a ast (s1 ast t)) by A31, Th24

        .= (s21 ast (s1 ast t)) by A28, Th31;

        then s22 is_properly_applicable_to (s1 ast t) by A26, A33, Th60;

        then

         A35: (s1 ^ s22) is_properly_applicable_to t by A34, Th61;

        

         A36: ( len s2) = (( len s21) + ( len s22)) by A26, FINSEQ_1: 22;

        ( rng s) = (( rng s1) \/ ( rng s2)) by A22, FINSEQ_1: 31;

        then k <= ( len (s1 ^ s22)) by A5, A7, A35, A32, A30, XBOOLE_1: 4;

        then k <= (( len s1) + ( len s22)) by FINSEQ_1: 22;

        then (( len s21) + ( len s22)) <= ( 0 + ( len s22)) by A6, A23, A36, XREAL_1: 6;

        hence thesis by A27, XREAL_1: 6;

      end;

      hence thesis by A7, A8;

    end;

    begin

    definition

      let T be non empty non void reflexive transitive TAS-structure;

      :: ABCMIZ_0:def31

      func T @--> -> Relation of T means

      : Def31: for t1,t2 be type of T holds [t1, t2] in it iff ex a be adjective of T st not a in ( adjs t2) & a is_properly_applicable_to t2 & (a ast t2) = t1;

      existence

      proof

        defpred P[ Element of T, Element of T] means ex a be adjective of T st not a in ( adjs $2) & a is_properly_applicable_to $2 & (a ast $2) = $1;

        consider R be Relation of the carrier of T such that

         A1: for t1,t2 be Element of T holds [t1, t2] in R iff P[t1, t2] from RELSET_1:sch 2;

        reconsider R as Relation of T;

        take R;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let R1,R2 be Relation of T such that

         A2: for t1,t2 be type of T holds [t1, t2] in R1 iff ex a be adjective of T st not a in ( adjs t2) & a is_properly_applicable_to t2 & (a ast t2) = t1 and

         A3: for t1,t2 be type of T holds [t1, t2] in R2 iff ex a be adjective of T st not a in ( adjs t2) & a is_properly_applicable_to t2 & (a ast t2) = t1;

        let t1,t2 be Element of T;

         [t1, t2] in R1 iff ex a be adjective of T st not a in ( adjs t2) & a is_properly_applicable_to t2 & (a ast t2) = t1 by A2;

        hence [t1, t2] in R1 iff [t1, t2] in R2 by A3;

      end;

    end

    theorem :: ABCMIZ_0:66

    

     Th66: for T be adj-structured antisymmetric non void reflexive transitive with_suprema Noetherian TAS-structure holds (T @--> ) c= the InternalRel of T

    proof

      let T be adj-structured with_suprema antisymmetric non empty non void reflexive transitive Noetherian TAS-structure;

      let t1,t2 be Element of T;

      reconsider q1 = t1, q2 = t2 as type of T;

      assume [t1, t2] in (T @--> );

      then

      consider a be adjective of T such that not a in ( adjs q2) and

       A1: a is_properly_applicable_to q2 and

       A2: (a ast q2) = q1 by Def31;

      a is_applicable_to q2 by A1;

      then q1 <= q2 by A2, Th20;

      hence thesis by ORDERS_2:def 5;

    end;

    scheme :: ABCMIZ_0:sch2

    RedInd { X() -> non empty set , P[ set, set], R() -> Relation of X() } :

for x,y be Element of X() st R() reduces (x,y) holds P[x, y]

      provided

       A1: for x,y be Element of X() st [x, y] in R() holds P[x, y]

       and

       A2: for x be Element of X() holds P[x, x]

       and

       A3: for x,y,z be Element of X() st P[x, y] & P[y, z] holds P[x, z];

      let x,y be Element of X();

      given p be RedSequence of R() such that

       A4: (p . 1) = x and

       A5: (p . ( len p)) = y;

      defpred P[ Nat] means (1 + $1) <= ( len p) implies P[x, (p . (1 + $1))];

       A6:

      now

        let i be Nat such that

         A7: P[i];

        now

          

           A8: (i + 1) >= 1 by NAT_1: 11;

          assume

           A9: (1 + (i + 1)) <= ( len p);

          (1 + (i + 1)) >= 1 by NAT_1: 11;

          then

           A10: (1 + (i + 1)) in ( dom p) by A9, FINSEQ_3: 25;

          (i + 1) < ( len p) by A9, NAT_1: 13;

          then (i + 1) in ( dom p) by A8, FINSEQ_3: 25;

          then

           A11: [(p . (i + 1)), (p . (1 + (i + 1)))] in R() by A10, REWRITE1:def 2;

          then

           A12: (p . (1 + (i + 1))) in X() by ZFMISC_1: 87;

          

           A13: (p . (i + 1)) in X() by A11, ZFMISC_1: 87;

          then P[(p . (i + 1)), (p . (1 + (i + 1)))] by A1, A11, A12;

          hence P[x, (p . (1 + (i + 1)))] by A3, A7, A9, A13, A12, NAT_1: 13;

        end;

        hence P[(i + 1)];

      end;

      

       A14: P[ 0 ] by A2, A4;

      

       A15: for n be Nat holds P[n] from NAT_1:sch 2( A14, A6);

      ( len p) >= ( 0 + 1) by NAT_1: 13;

      then

      consider n be Nat such that

       A16: ( len p) = (1 + n) by NAT_1: 10;

      thus thesis by A5, A16, A15;

    end;

    theorem :: ABCMIZ_0:67

    

     Th67: for T be adj-structured antisymmetric non void reflexive transitive with_suprema Noetherian TAS-structure holds for t1,t2 be type of T st (T @--> ) reduces (t1,t2) holds t1 <= t2

    proof

      let T be adj-structured with_suprema antisymmetric non empty non void reflexive transitive Noetherian TAS-structure;

      let t1,t2 be type of T;

      set R = (T @--> );

      defpred P[ Element of T, Element of T] means $1 <= $2;

      

       A1: for x,y,z be Element of T holds P[x, y] & P[y, z] implies P[x, z] by YELLOW_0:def 2;

       A2:

      now

        let x,y be Element of T;

        R c= the InternalRel of T by Th66;

        hence [x, y] in R implies P[x, y] by ORDERS_2:def 5;

      end;

      

       A3: for x be Element of T holds P[x, x];

      for x,y be Element of T st R reduces (x,y) holds P[x, y] from RedInd( A2, A3, A1);

      hence thesis;

    end;

    theorem :: ABCMIZ_0:68

    

     Th68: for T be Noetherian adj-structured reflexive transitive antisymmetric non void with_suprema TAS-structure holds (T @--> ) is irreflexive

    proof

      let T be Noetherian adj-structured reflexive transitive antisymmetric non void with_suprema TAS-structure;

      set R = (T @--> );

      let x be object;

      assume x in ( field R);

      assume

       A1: [x, x] in R;

      then

      reconsider x as type of T by ZFMISC_1: 87;

      consider a be adjective of T such that

       A2: not a in ( adjs x) and

       A3: a is_properly_applicable_to x and

       A4: (a ast x) = x by A1, Def31;

      a is_applicable_to x by A3;

      hence thesis by A2, A4, Th21;

    end;

    theorem :: ABCMIZ_0:69

    

     Th69: for T be adj-structured antisymmetric non void reflexive transitive with_suprema Noetherian TAS-structure holds (T @--> ) is strongly-normalizing

    proof

      let T be adj-structured with_suprema antisymmetric non empty non void reflexive transitive Noetherian TAS-structure;

      set R = (T @--> ), Q = the InternalRel of T;

      

       A1: ( field R) c= ( field Q) by Th66, RELAT_1: 16;

      

       A2: R c= Q by Th66;

      R is co-well_founded

      proof

        let Y be set;

        assume that

         A3: Y c= ( field R) and

         A4: Y <> {} ;

        Y c= ( field Q) by A1, A3;

        then

        consider a be object such that

         A5: a in Y and

         A6: for b be object st b in Y & a <> b holds not [a, b] in Q by A4, REWRITE1:def 16;

        take a;

        thus thesis by A2, A5, A6;

      end;

      then R is irreflexive co-well_founded Relation by Th68;

      hence thesis;

    end;

    theorem :: ABCMIZ_0:70

    

     Th70: for T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema non void TAS-structure holds for t be type of T, A be finite Subset of the adjectives of T st for C be Subset of the adjectives of T st C c= A & C is_properly_applicable_to t & (A ast t) = (C ast t) holds C = A holds for s be one-to-one FinSequence of the adjectives of T st ( rng s) = A & s is_properly_applicable_to t holds for i be Nat st 1 <= i & i <= ( len s) holds [(( apply (s,t)) . (i + 1)), (( apply (s,t)) . i)] in (T @--> )

    proof

      let T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema non void TAS-structure;

      let t be type of T, A be finite Subset of the adjectives of T such that

       A1: for C be Subset of the adjectives of T st C c= A & C is_properly_applicable_to t & (A ast t) = (C ast t) holds C = A;

      let s be one-to-one FinSequence of the adjectives of T such that

       A2: ( rng s) = A and

       A3: s is_properly_applicable_to t;

      let j be Nat;

      assume that

       A4: 1 <= j and

       A5: j <= ( len s);

      

       A6: ( len ( apply (s,t))) = (( len s) + 1) by Def19;

      j < (( len s) + 1) by A5, NAT_1: 13;

      then j in ( dom ( apply (s,t))) by A6, A4, FINSEQ_3: 25;

      then (( apply (s,t)) . j) in ( rng ( apply (s,t))) by FUNCT_1: 3;

      then

      reconsider tt = (( apply (s,t)) . j) as type of T;

      

       A7: j in ( dom s) by A4, A5, FINSEQ_3: 25;

      then (s . j) in ( rng s) by FUNCT_1: 3;

      then

      reconsider a = (s . j) as adjective of T;

      

       A8: (( apply (s,t)) . (j + 1)) = (a ast tt) by A7, Def19;

      

       A9: not a in ( adjs tt)

      proof

        assume

         A10: a in ( adjs tt);

        consider i be Nat such that

         A11: j = (1 + i) by A4, NAT_1: 10;

        reconsider i as Element of NAT by ORDINAL1:def 12;

        reconsider s1 = (s | ( Seg i)) as FinSequence of the adjectives of T by FINSEQ_1: 18;

        s1 c= s by TREES_1:def 1;

        then

        consider s2 be FinSequence such that

         A12: s = (s1 ^ s2) by TREES_1: 1;

        reconsider s2 as FinSequence of the adjectives of T by A12, FINSEQ_1: 36;

        

         A13: ( len s) = (( len s1) + ( len s2)) by A12, FINSEQ_1: 22;

        then

         A14: s1 is_properly_applicable_to t by A3, A12, Th60;

        reconsider s21 = (s2 | ( Seg 1)) as FinSequence of the adjectives of T by FINSEQ_1: 18;

        i <= ( len s) by A5, A11, NAT_1: 13;

        then

         A15: ( len s1) = i by FINSEQ_1: 17;

        then

         A16: ( len s2) >= 1 by A5, A11, A13, XREAL_1: 6;

        then

         A17: ( len s21) = 1 by FINSEQ_1: 17;

        then

         A18: s21 = <*(s21 . 1)*> by FINSEQ_1: 40;

        then

         A19: ( rng s21) = {(s21 . 1)} by FINSEQ_1: 39;

        then

        reconsider b = (s21 . 1) as adjective of T by ZFMISC_1: 31;

        

         A20: 1 in ( dom s2) by A16, FINSEQ_3: 25;

        s21 c= s2 by TREES_1:def 1;

        then

        consider s22 be FinSequence such that

         A21: s2 = (s21 ^ s22) by TREES_1: 1;

        reconsider s22 as FinSequence of the adjectives of T by A21, FINSEQ_1: 36;

        

         A22: ( rng s2) = (( rng s21) \/ ( rng s22)) by A21, FINSEQ_1: 31;

        then

         A23: ( rng s22) c= ( rng s2) by XBOOLE_1: 7;

        

         A24: b = (s2 . 1) by A18, A21, FINSEQ_1: 41

        .= a by A11, A12, A15, A20, FINSEQ_1:def 7;

        then a in ( rng s21) by A19, TARSKI:def 1;

        then

         A25: a in ( rng s2) by A22, XBOOLE_0:def 3;

        (s1 ast t) = tt by A11, A12, A13, A15, Th36;

        

        then

         A26: (s1 ast t) = (a ast (s1 ast t)) by A10, Th24

        .= (s21 ast (s1 ast t)) by A18, A24, Th31;

        s2 is_properly_applicable_to (s1 ast t) by A3, A12, Th60;

        then s22 is_properly_applicable_to (s1 ast t) by A21, A26, Th60;

        then

         A27: (s1 ^ s22) is_properly_applicable_to t by A14, Th61;

        reconsider B = ( rng (s1 ^ s22)) as Subset of the adjectives of T;

        

         A28: B = (( rng s1) \/ ( rng s22)) by FINSEQ_1: 31;

        

         A29: A = (( rng s1) \/ ( rng s2)) by A2, A12, FINSEQ_1: 31;

        (s ast t) = (s2 ast (s1 ast t)) by A12, Th37

        .= (s22 ast (s1 ast t)) by A21, A26, Th37

        .= ((s1 ^ s22) ast t) by Th37;

        

        then

         A30: (A ast t) = ((s1 ^ s22) ast t) by A2, A3, Th56, Th57

        .= (B ast t) by A27, Th56, Th57;

        B is_properly_applicable_to t by A27;

        then B = A by A1, A30, A28, A29, A23, XBOOLE_1: 9;

        then

         A31: a in B by A29, A25, XBOOLE_0:def 3;

        per cases by A28, A31, XBOOLE_0:def 3;

          suppose a in ( rng s1);

          then

          consider x be object such that

           A32: x in ( dom s1) and

           A33: a = (s1 . x) by FUNCT_1:def 3;

          reconsider x as Element of NAT by A32;

          x <= ( len s1) by A32, FINSEQ_3: 25;

          then

           A34: x < j by A11, A15, NAT_1: 13;

          

           A35: ( dom s1) c= ( dom s) by A12, FINSEQ_1: 26;

          (s . x) = a by A12, A32, A33, FINSEQ_1:def 7;

          hence contradiction by A7, A32, A35, A34, FUNCT_1:def 4;

        end;

          suppose a in ( rng s22);

          then

          consider x be object such that

           A36: x in ( dom s22) and

           A37: a = (s22 . x) by FUNCT_1:def 3;

          reconsider x as Element of NAT by A36;

          

           A38: (1 + x) in ( dom s2) by A17, A21, A36, FINSEQ_1: 28;

          x >= ( 0 + 1) by A36, FINSEQ_3: 25;

          then

           A39: (j + x) > (j + 0 ) by XREAL_1: 6;

          (s2 . (1 + x)) = a by A17, A21, A36, A37, FINSEQ_1:def 7;

          then

           A40: (s . (i + (1 + x))) = a by A12, A15, A38, FINSEQ_1:def 7;

          (i + (1 + x)) in ( dom s) by A12, A15, A38, FINSEQ_1: 28;

          hence contradiction by A7, A11, A39, A40, FUNCT_1:def 4;

        end;

      end;

      a is_properly_applicable_to tt by A3, A7;

      hence thesis by A8, A9, Def31;

    end;

    theorem :: ABCMIZ_0:71

    

     Th71: for T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema non void TAS-structure holds for t be type of T, A be finite Subset of the adjectives of T st for C be Subset of the adjectives of T st C c= A & C is_properly_applicable_to t & (A ast t) = (C ast t) holds C = A holds for s be one-to-one FinSequence of the adjectives of T st ( rng s) = A & s is_properly_applicable_to t holds ( Rev ( apply (s,t))) is RedSequence of (T @--> )

    proof

      let T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema non void TAS-structure;

      let t be type of T, A be finite Subset of the adjectives of T such that

       A1: for C be Subset of the adjectives of T st C c= A & C is_properly_applicable_to t & (A ast t) = (C ast t) holds C = A;

      let s be one-to-one FinSequence of the adjectives of T such that

       A2: ( rng s) = A and

       A3: s is_properly_applicable_to t;

      

       A4: ( len ( Rev ( apply (s,t)))) = ( len ( apply (s,t))) by FINSEQ_5:def 3;

      hence ( len ( Rev ( apply (s,t)))) > 0 ;

      let i be Nat;

      assume that

       A5: i in ( dom ( Rev ( apply (s,t)))) and

       A6: (i + 1) in ( dom ( Rev ( apply (s,t))));

      

       A7: ( len ( apply (s,t))) = (( len s) + 1) by Def19;

      then

       A8: (( Rev ( apply (s,t))) . i) = (( apply (s,t)) . (((( len s) + 1) - i) + 1)) by A5, FINSEQ_5:def 3;

      (i + 1) <= (( len s) + 1) by A4, A7, A6, FINSEQ_3: 25;

      then

      consider j be Nat such that

       A9: (( len s) + 1) = ((i + 1) + j) by NAT_1: 10;

      

       A10: (( Rev ( apply (s,t))) . (i + 1)) = (( apply (s,t)) . (((( len s) + 1) - (i + 1)) + 1)) by A7, A6, FINSEQ_5:def 3;

      

       A11: i >= 1 by A5, FINSEQ_3: 25;

      ( len s) = (i + j) by A9;

      then

       A12: (j + 1) <= ( len s) by A11, XREAL_1: 6;

      (j + 1) >= 1 by NAT_1: 11;

      hence thesis by A1, A2, A3, A8, A10, A9, A12, Th70;

    end;

    theorem :: ABCMIZ_0:72

    

     Th72: for T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema non void TAS-structure holds for t be type of T, A be finite Subset of the adjectives of T st A is_properly_applicable_to t holds (T @--> ) reduces ((A ast t),t)

    proof

      let T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema non void TAS-structure;

      set R = (T @--> );

      let t be type of T, A be finite Subset of the adjectives of T;

      assume A is_properly_applicable_to t;

      then

      consider A9 be Subset of the adjectives of T such that A9 c= A and

       A1: A9 is_properly_applicable_to t and

       A2: (A ast t) = (A9 ast t) and

       A3: for C be Subset of the adjectives of T st C c= A9 & C is_properly_applicable_to t & (A ast t) = (C ast t) holds C = A9 by Th64;

      consider s be one-to-one FinSequence of the adjectives of T such that

       A4: ( rng s) = A9 and

       A5: s is_properly_applicable_to t by A1, Th65;

      reconsider p = ( Rev ( apply (s,t))) as RedSequence of R by A2, A3, A4, A5, Th71;

      take p;

      

      thus (p . 1) = (( apply (s,t)) . ( len ( apply (s,t)))) by FINSEQ_5: 62

      .= (s ast t) by Def19

      .= (A ast t) by A2, A4, A5, Th56, Th57;

      

      thus (p . ( len p)) = (p . ( len ( apply (s,t)))) by FINSEQ_5:def 3

      .= (( apply (s,t)) . 1) by FINSEQ_5: 62

      .= t by Def19;

    end;

    theorem :: ABCMIZ_0:73

    

     Th73: for X be non empty set holds for R be Relation of X holds for r be RedSequence of R st (r . 1) in X holds r is FinSequence of X

    proof

      let X be non empty set;

      let R be Relation of X;

      let p be RedSequence of R such that

       A1: (p . 1) in X;

      let x be object;

      assume x in ( rng p);

      then

      consider i be object such that

       A2: i in ( dom p) and

       A3: x = (p . i) by FUNCT_1:def 3;

      reconsider i as Element of NAT by A2;

      

       A4: i >= 1 by A2, FINSEQ_3: 25;

      per cases by A4, XXREAL_0: 1;

        suppose i = 1;

        hence thesis by A1, A3;

      end;

        suppose i > 1;

        then i >= (1 + 1) by NAT_1: 13;

        then

        consider j be Nat such that

         A5: i = ((1 + 1) + j) by NAT_1: 10;

        

         A6: i = ((j + 1) + 1) by A5;

        

         A7: (j + 1) >= 1 by NAT_1: 11;

        i <= ( len p) by A2, FINSEQ_3: 25;

        then (j + 1) < ( len p) by A6, NAT_1: 13;

        then (j + 1) in ( dom p) by A7, FINSEQ_3: 25;

        then [(p . (j + 1)), x] in R by A2, A3, A6, REWRITE1:def 2;

        hence thesis by ZFMISC_1: 87;

      end;

    end;

    theorem :: ABCMIZ_0:74

    

     Th74: for X be non empty set holds for R be Relation of X holds for x be Element of X, y be set st R reduces (x,y) holds y in X

    proof

      let X be non empty set;

      let R be Relation of X;

      let x be Element of X, y be set;

      given p be RedSequence of R such that

       A1: (p . 1) = x and

       A2: (p . ( len p)) = y;

      ( len p) >= ( 0 + 1) by NAT_1: 13;

      then ( len p) in ( dom p) by FINSEQ_3: 25;

      then

       A3: y in ( rng p) by A2, FUNCT_1: 3;

      p is FinSequence of X by A1, Th73;

      then ( rng p) c= X by FINSEQ_1:def 4;

      hence thesis by A3;

    end;

    theorem :: ABCMIZ_0:75

    

     Th75: for X be non empty set holds for R be Relation of X st R is with_UN_property weakly-normalizing holds for x be Element of X holds ( nf (x,R)) in X

    proof

      let X be non empty set;

      let R be Relation of X such that

       A1: R is with_UN_property weakly-normalizing;

      let x be Element of X;

      ( nf (x,R)) is_a_normal_form_of (x,R) by A1, REWRITE1: 54;

      then R reduces (x,( nf (x,R)));

      hence thesis by Th74;

    end;

    theorem :: ABCMIZ_0:76

    

     Th76: for T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema non void TAS-structure holds for t1,t2 be type of T st (T @--> ) reduces (t1,t2) holds ex A be finite Subset of the adjectives of T st A is_properly_applicable_to t2 & t1 = (A ast t2)

    proof

      let T be Noetherian adj-structured reflexive transitive antisymmetric with_suprema non void TAS-structure;

      let t1,t2 be type of T;

      set R = (T @--> );

      given p be RedSequence of R such that

       A1: (p . 1) = t1 and

       A2: t2 = (p . ( len p));

      defpred P[ object, object] means ex j be Element of NAT , a be adjective of T, t be type of T st $2 = a & $1 = j & (a ast t) = (p . j) & t = (p . (j + 1)) & a is_properly_applicable_to t;

      

       A3: ( len ( Rev p)) = ( len p) by FINSEQ_5:def 3;

      

       A4: ((( len p) - 1) + 1) = ( len p);

      

       A5: ( len p) >= ( 0 + 1) by NAT_1: 13;

      then

      consider i be Nat such that

       A6: ( len p) = (1 + i) by NAT_1: 10;

      reconsider i as Element of NAT by ORDINAL1:def 12;

       A7:

      now

        let x be object;

        assume

         A8: x in ( Seg i);

        then

        reconsider j = x as Element of NAT ;

        

         A9: j >= 1 by A8, FINSEQ_1: 1;

        then

         A10: 1 <= (j + 1) by NAT_1: 13;

        

         A11: j <= i by A8, FINSEQ_1: 1;

        then j < ( len p) by A6, NAT_1: 13;

        then

         A12: j in ( dom p) by A9, FINSEQ_3: 25;

        (j + 1) <= ( len p) by A6, A11, XREAL_1: 6;

        then (j + 1) in ( dom p) by A10, FINSEQ_3: 25;

        then

         A13: [(p . j), (p . (j + 1))] in R by A12, REWRITE1:def 2;

        then

        reconsider q1 = (p . j), q2 = (p . (j + 1)) as type of T by ZFMISC_1: 87;

        ex a be adjective of T st not a in ( adjs q2) & a is_properly_applicable_to q2 & (a ast q2) = q1 by A13, Def31;

        hence ex y be object st y in the adjectives of T & P[x, y];

      end;

      consider f be Function such that

       A14: ( dom f) = ( Seg i) & ( rng f) c= the adjectives of T and

       A15: for x be object st x in ( Seg i) holds P[x, (f . x)] from FUNCT_1:sch 6( A7);

      f is FinSequence by A14, FINSEQ_1:def 2;

      then

      reconsider f as FinSequence of the adjectives of T by A14, FINSEQ_1:def 4;

      

       A16: ( len f) = i by A14, FINSEQ_1:def 3;

      set r = ( Rev f);

      defpred P[ Nat] means (1 + $1) <= ( len p) implies (( Rev p) . (1 + $1)) = (( apply (r,t2)) . (1 + $1));

      

       A17: ( len r) = ( len f) by FINSEQ_5:def 3;

       A18:

      now

        let j be Nat such that

         A19: P[j];

        now

          

           A20: (j + 1) >= 1 by NAT_1: 11;

          assume

           A21: (1 + (j + 1)) <= ( len p);

          then (j + 1) <= i by A6, XREAL_1: 6;

          then

          consider x be Nat such that

           A22: i = ((j + 1) + x) by NAT_1: 10;

          reconsider x as Element of NAT by ORDINAL1:def 12;

          

           A23: ((i + 1) - (j + 1)) = (x + 1) by A22;

          (j + 1) < ( len p) by A21, NAT_1: 13;

          then (j + 1) in ( dom ( Rev p)) by A3, A20, FINSEQ_3: 25;

          then

           A24: (( Rev p) . (j + 1)) = (p . ((x + 1) + 1)) by A6, A23, FINSEQ_5:def 3;

          

           A25: ((i + 1) - (1 + (j + 1))) = x by A22;

          (1 + (j + 1)) >= 1 by NAT_1: 11;

          then (1 + (j + 1)) in ( dom ( Rev p)) by A3, A21, FINSEQ_3: 25;

          then

           A26: (( Rev p) . (1 + (j + 1))) = (p . (x + 1)) by A6, A25, FINSEQ_5:def 3;

          i = ((x + 1) + j) by A22;

          then

           A27: i >= (x + 1) by NAT_1: 11;

          (x + 1) >= 1 by NAT_1: 11;

          then (x + 1) in ( Seg i) by A27;

          then

          consider k be Element of NAT , a be adjective of T, t be type of T such that

           A28: (f . (x + 1)) = a and

           A29: (x + 1) = k and

           A30: (a ast t) = (p . k) and

           A31: t = (p . (k + 1)) and a is_properly_applicable_to t by A15;

          

           A32: (j + 1) >= 1 by NAT_1: 11;

          (j + 1) <= i by A22, NAT_1: 11;

          then

           A33: (j + 1) in ( dom r) by A17, A16, A32, FINSEQ_3: 25;

          

          then (r . (j + 1)) = (f . ((( len f) - (j + 1)) + 1)) by FINSEQ_5:def 3

          .= a by A16, A22, A28;

          hence (( Rev p) . (1 + (j + 1))) = (( apply (r,t2)) . (1 + (j + 1))) by A19, A21, A29, A30, A31, A33, A24, A26, Def19, NAT_1: 13;

        end;

        hence P[(j + 1)];

      end;

      reconsider A = ( rng f) as finite Subset of the adjectives of T;

      take A;

      

       A34: ( len ( apply (r,t2))) = (( len r) + 1) by Def19;

      1 in ( dom ( Rev p)) by A5, A3, FINSEQ_3: 25;

      then (( Rev p) . 1) = t2 by A2, A4, FINSEQ_5:def 3;

      then

       A35: P[ 0 ] by Def19;

      

       A36: for j be Nat holds P[j] from NAT_1:sch 2( A35, A18);

      now

        let j be Nat;

        assume 1 <= j;

        then

        consider k be Nat such that

         A37: j = (1 + k) by NAT_1: 10;

        thus j <= ( len p) implies (( Rev p) . j) = (( apply (r,t2)) . j) by A36, A37;

      end;

      then

       A38: ( Rev p) = ( apply (r,t2)) by A6, A17, A34, A16, A3;

      then

       A39: p = ( Rev ( apply (r,t2)));

      

       A40: r is_properly_applicable_to t2

      proof

        let j be Nat, a be adjective of T, s be type of T;

        assume that

         A41: j in ( dom r) and

         A42: a = (r . j) and

         A43: s = (( apply (r,t2)) . j);

        j <= ( len r) by A41, FINSEQ_3: 25;

        then

        consider k be Nat such that

         A44: ( len r) = (j + k) by NAT_1: 10;

        

         A45: ( len r) = ( len f) by FINSEQ_5:def 3;

        reconsider k as Element of NAT by ORDINAL1:def 12;

        

         A46: (k + 1) >= 1 by NAT_1: 11;

        

         A47: j >= 1 by A41, FINSEQ_3: 25;

        then (k + 1) <= i by A16, A44, A45, XREAL_1: 6;

        then ((( len f) - j) + 1) in ( Seg i) by A44, A45, A46;

        then

        consider o be Element of NAT , b be adjective of T, u be type of T such that

         A48: (f . ((( len f) - j) + 1)) = b and

         A49: ((( len f) - j) + 1) = o and (b ast u) = (p . o) and

         A50: u = (p . (o + 1)) and

         A51: b is_properly_applicable_to u by A15;

        

         A52: (o + 1) >= 1 by NAT_1: 11;

        (i + 1) = ((k + 1) + j) by A17, A16, A44;

        then (o + 1) <= ( len p) by A6, A44, A45, A47, A49, XREAL_1: 6;

        then

         A53: (o + 1) in ( dom p) by A52, FINSEQ_3: 25;

        

         A54: a = b by A41, A42, A48, FINSEQ_5:def 3;

        ((( len ( apply (r,t2))) - (o + 1)) + 1) = j by A17, A34, A49;

        hence thesis by A39, A43, A50, A51, A53, A54, FINSEQ_5:def 3;

      end;

      thus A is_properly_applicable_to t2

      proof

        take r;

        thus thesis by A40, FINSEQ_5: 57;

      end;

      ( rng r) = A by FINSEQ_5: 57;

      

      then (A ast t2) = (r ast t2) by A40, Th56, Th57

      .= (( apply (r,t2)) . (( len r) + 1));

      hence thesis by A1, A34, A3, A38, FINSEQ_5: 62;

    end;

    theorem :: ABCMIZ_0:77

    

     Th77: for T be adj-structured antisymmetric commutative non void reflexive transitive with_suprema Noetherian TAS-structure holds (T @--> ) is with_Church-Rosser_property with_UN_property

    proof

      let T be adj-structured with_suprema antisymmetric commutative non empty non void reflexive transitive Noetherian TAS-structure;

      set R = (T @--> );

      R is locally-confluent

      proof

        let a,b,c be object;

        assume that

         A1: [a, b] in R and

         A2: [a, c] in R;

        reconsider t = a, t1 = b, t2 = c as type of T by A1, A2, ZFMISC_1: 87;

        consider a2 be adjective of T such that not a2 in ( adjs t1) and

         A3: a2 is_properly_applicable_to t1 and

         A4: (a2 ast t1) = t by A1, Def31;

        set tt = (t1 "\/" t2);

        take tt;

        consider a3 be adjective of T such that not a3 in ( adjs t2) and

         A5: a3 is_properly_applicable_to t2 and

         A6: (a3 ast t2) = t by A2, Def31;

        a3 is_applicable_to t2 by A5;

        then t <= t2 by A6, Th20;

        then

         A7: ex B be finite Subset of the adjectives of T st B is_properly_applicable_to (t1 "\/" t2) & (B ast (t1 "\/" t2)) = t2 by A3, A4, Def30;

        a2 is_applicable_to t1 by A3;

        then t <= t1 by A4, Th20;

        then ex A be finite Subset of the adjectives of T st A is_properly_applicable_to (t1 "\/" t2) & (A ast (t1 "\/" t2)) = t1 by A5, A6, Def30;

        hence thesis by A7, Th72;

      end;

      then R is strongly-normalizing locally-confluent Relation by Th69;

      hence thesis;

    end;

    begin

    definition

      let T be adj-structured with_suprema antisymmetric commutative non empty non void reflexive transitive Noetherian TAS-structure;

      let t be type of T;

      :: ABCMIZ_0:def32

      func radix t -> type of T equals ( nf (t,(T @--> )));

      coherence

      proof

        (T @--> ) is with_Church-Rosser_property with_UN_property strongly-normalizing Relation by Th69, Th77;

        hence thesis by Th75;

      end;

    end

    theorem :: ABCMIZ_0:78

    

     Th78: for T be adj-structured with_suprema antisymmetric commutative non empty non void reflexive transitive Noetherian TAS-structure holds for t be type of T holds (T @--> ) reduces (t,( radix t))

    proof

      let T be adj-structured with_suprema antisymmetric commutative non empty non void reflexive transitive Noetherian TAS-structure;

      let t be type of T;

      set R = (T @--> );

      R is with_Church-Rosser_property with_UN_property strongly-normalizing Relation by Th69, Th77;

      then ( nf (t,R)) is_a_normal_form_of (t,R) by REWRITE1: 54;

      hence thesis;

    end;

    theorem :: ABCMIZ_0:79

    for T be adj-structured with_suprema antisymmetric commutative non empty non void reflexive transitive Noetherian TAS-structure holds for t be type of T holds t <= ( radix t) by Th67, Th78;

    theorem :: ABCMIZ_0:80

    

     Th80: for T be adj-structured with_suprema antisymmetric commutative non empty non void reflexive transitive Noetherian TAS-structure holds for t be type of T holds for X be set st X = { t9 where t9 be type of T : ex A be finite Subset of the adjectives of T st A is_properly_applicable_to t9 & (A ast t9) = t } holds ex_sup_of (X,T) & ( radix t) = ( "\/" (X,T))

    proof

      let T be adj-structured with_suprema antisymmetric commutative non empty non void reflexive transitive Noetherian TAS-structure;

      let t be type of T;

      set R = (T @--> );

      set AA = { t9 where t9 be type of T : ex A be finite Subset of the adjectives of T st A is_properly_applicable_to t9 & (A ast t9) = t };

      

       A1: R is with_Church-Rosser_property with_UN_property strongly-normalizing Relation by Th69, Th77;

      

       A2: ( radix t) is_>=_than AA

      proof

        let tt be type of T;

        assume tt in AA;

        then ex t9 be type of T st tt = t9 & ex A be finite Subset of the adjectives of T st A is_properly_applicable_to t9 & (A ast t9) = t;

        then R reduces (t,tt) by Th72;

        then (t,tt) are_convertible_wrt R by REWRITE1: 25;

        then ( nf (t,R)) = ( nf (tt,R)) by A1, REWRITE1: 55;

        then ( nf (t,R)) is_a_normal_form_of (tt,R) by A1, REWRITE1: 54;

        then R reduces (tt,( nf (t,R)));

        hence thesis by Th67;

      end;

      ex A be finite Subset of the adjectives of T st A is_properly_applicable_to ( radix t) & (A ast ( radix t)) = t by Th76, Th78;

      then ( radix t) in AA;

      then for t9 be type of T st t9 is_>=_than AA holds ( radix t) <= t9;

      hence thesis by A2, YELLOW_0: 30;

    end;

    theorem :: ABCMIZ_0:81

    

     Th81: for T be adj-structured with_suprema antisymmetric commutative non empty non void reflexive transitive Noetherian TAS-structure holds for t1,t2 be type of T, a be adjective of T st a is_properly_applicable_to t1 & (a ast t1) <= ( radix t2) holds t1 <= ( radix t2)

    proof

      let T be adj-structured with_suprema antisymmetric commutative non empty non void reflexive transitive Noetherian TAS-structure;

      let t1,t2 be type of T, a be adjective of T;

      set R = (T @--> );

      set AA = { t9 where t9 be type of T : ex A be finite Subset of the adjectives of T st A is_properly_applicable_to t9 & (A ast t9) = t2 };

      assume that

       A1: a is_properly_applicable_to t1 and

       A2: (a ast t1) <= ( radix t2);

      consider A be finite Subset of the adjectives of T such that

       A3: A is_properly_applicable_to (t1 "\/" ( radix t2)) and

       A4: (A ast (t1 "\/" ( radix t2))) = ( radix t2) by A1, A2, Def30;

      consider v1 be FinSequence of the adjectives of T such that

       A5: ( rng v1) = A and

       A6: v1 is_properly_applicable_to (t1 "\/" ( radix t2)) by A3;

      R is with_Church-Rosser_property with_UN_property strongly-normalizing Relation by Th69, Th77;

      then ( nf (t2,R)) is_a_normal_form_of (t2,R) by REWRITE1: 54;

      then R reduces (t2,( nf (t2,R)));

      then

      consider B be finite Subset of the adjectives of T such that

       A7: B is_properly_applicable_to ( radix t2) and

       A8: t2 = (B ast ( radix t2)) by Th76;

      consider v2 be FinSequence of the adjectives of T such that

       A9: ( rng v2) = B and

       A10: v2 is_properly_applicable_to ( radix t2) by A7;

      

       A11: ( rng (v1 ^ v2)) = (A \/ B) by A5, A9, FINSEQ_1: 31;

      

       A12: ( radix t2) = (v1 ast (t1 "\/" ( radix t2))) by A4, A5, A6, Th56, Th57;

      then

       A13: (v1 ^ v2) is_properly_applicable_to (t1 "\/" ( radix t2)) by A6, A10, Th61;

      then

       A14: (A \/ B) is_properly_applicable_to (t1 "\/" ( radix t2)) by A11;

      ((A \/ B) ast (t1 "\/" ( radix t2))) = ((v1 ^ v2) ast (t1 "\/" ( radix t2))) by A11, A13, Th56, Th57

      .= (v2 ast ( radix t2)) by A12, Th37

      .= t2 by A8, A9, A10, Th56, Th57;

      then (t1 "\/" ( radix t2)) in AA by A14;

      then (t1 "\/" ( radix t2)) <= ( "\/" (AA,T)) by Th80, YELLOW_4: 1;

      then

       A15: (t1 "\/" ( radix t2)) <= ( radix t2) by Th80;

      (t1 "\/" ( radix t2)) >= t1 by YELLOW_0: 22;

      hence thesis by A15, YELLOW_0:def 2;

    end;

    theorem :: ABCMIZ_0:82

    for T be adj-structured with_suprema antisymmetric commutative non empty non void reflexive transitive Noetherian TAS-structure holds for t1,t2 be type of T st t1 <= t2 holds ( radix t1) <= ( radix t2)

    proof

      let T be adj-structured with_suprema antisymmetric commutative non empty non void reflexive transitive Noetherian TAS-structure;

      set R = (T @--> );

      let t1,t2 be type of T such that

       A1: t1 <= t2;

      t2 <= ( radix t2) by Th67, Th78;

      then

       A2: t1 <= ( radix t2) by A1, YELLOW_0:def 2;

      set X = the carrier of T;

      defpred P[ Element of X, Element of X] means $1 <= ( radix t2) implies $2 <= ( radix t2);

      

       A3: for x,y,z be Element of X st P[x, y] & P[y, z] holds P[x, z];

       A4:

      now

        let x,y be Element of X;

        reconsider t1 = x, t2 = y as type of T;

        assume [x, y] in R;

        then ex a be adjective of T st not a in ( adjs t2) & a is_properly_applicable_to t2 & (a ast t2) = t1 by Def31;

        hence P[x, y] by Th81;

      end;

      

       A5: for x be Element of X holds P[x, x];

      for x,y be Element of T st R reduces (x,y) holds P[x, y] from RedInd( A4, A5, A3);

      hence thesis by A2, Th78;

    end;

    theorem :: ABCMIZ_0:83

    for T be adj-structured with_suprema antisymmetric commutative non empty non void reflexive transitive Noetherian TAS-structure holds for t be type of T, a be adjective of T st a is_properly_applicable_to t holds ( radix (a ast t)) = ( radix t)

    proof

      let T be adj-structured with_suprema antisymmetric commutative non empty non void reflexive transitive Noetherian TAS-structure;

      let t be type of T, a be adjective of T;

      

       A1: a in ( adjs t) or not a in ( adjs t);

      assume a is_properly_applicable_to t;

      then (a ast t) = t or [(a ast t), t] in (T @--> ) by A1, Def31, Th24;

      then (T @--> ) reduces ((a ast t),t) by REWRITE1: 12, REWRITE1: 15;

      then

       A2: ((a ast t),t) are_convertible_wrt (T @--> ) by REWRITE1: 25;

      (T @--> ) is with_Church-Rosser_property with_UN_property strongly-normalizing Relation by Th69, Th77;

      hence thesis by A2, REWRITE1: 55;

    end;