fomodel1.miz



    begin

    reserve k,m,n for Nat,

kk,mm,nn for Element of NAT ,

X,Y,x,y,z for set;

    registration

      let z be zero Integer;

      cluster |.z.| -> zero;

      coherence by COMPLEX1: 47;

    end

    registration

      let S be non degenerated ZeroOneStr;

      cluster (the carrier of S \ {the OneF of S}) -> non empty;

      coherence ;

    end

    definition

      struct ( ZeroOneStr) Language-like (# the carrier -> set,

the ZeroF, OneF -> Element of the carrier,

the adicity -> Function of ( the carrier \ { the OneF}), INT #)

       attr strict strict;

    end

    definition

      let S be Language-like;

      :: FOMODEL1:def1

      func AllSymbolsOf S -> set equals the carrier of S;

      coherence ;

      :: FOMODEL1:def2

      func LettersOf S -> set equals (the adicity of S " { 0 });

      coherence ;

      :: FOMODEL1:def3

      func OpSymbolsOf S -> set equals (the adicity of S " ( NAT \ { 0 }));

      coherence ;

      :: FOMODEL1:def4

      func RelSymbolsOf S -> set equals (the adicity of S " ( INT \ NAT ));

      coherence ;

      :: FOMODEL1:def5

      func TermSymbolsOf S -> set equals (the adicity of S " NAT );

      coherence ;

      :: FOMODEL1:def6

      func LowerCompoundersOf S -> set equals (the adicity of S " ( INT \ { 0 }));

      coherence ;

      :: FOMODEL1:def7

      func TheEqSymbOf S -> set equals the ZeroF of S;

      coherence ;

      :: FOMODEL1:def8

      func TheNorSymbOf S -> set equals the OneF of S;

      coherence ;

      :: FOMODEL1:def9

      func OwnSymbolsOf S -> set equals (the carrier of S \ {the ZeroF of S, the OneF of S});

      coherence ;

    end

    definition

      let S be Language-like;

      mode Element of S is Element of ( AllSymbolsOf S);

      :: FOMODEL1:def10

      func AtomicFormulaSymbolsOf S -> set equals (( AllSymbolsOf S) \ {( TheNorSymbOf S)});

      coherence ;

      :: FOMODEL1:def11

      func AtomicTermsOf S -> set equals (1 -tuples_on ( LettersOf S));

      coherence ;

      :: FOMODEL1:def12

      attr S is operational means ( OpSymbolsOf S) is non empty;

      :: FOMODEL1:def13

      attr S is relational means (( RelSymbolsOf S) \ {( TheEqSymbOf S)}) is non empty;

    end

    definition

      let S be Language-like;

      let s be Element of S;

      :: FOMODEL1:def14

      attr s is literal means

      : Def14: s in ( LettersOf S);

      :: FOMODEL1:def15

      attr s is low-compounding means

      : Def15: s in ( LowerCompoundersOf S);

      :: FOMODEL1:def16

      attr s is operational means

      : Def16: s in ( OpSymbolsOf S);

      :: FOMODEL1:def17

      attr s is relational means

      : Def17: s in ( RelSymbolsOf S);

      :: FOMODEL1:def18

      attr s is termal means

      : Def18: s in ( TermSymbolsOf S);

      :: FOMODEL1:def19

      attr s is own means s in ( OwnSymbolsOf S);

      :: FOMODEL1:def20

      attr s is ofAtomicFormula means

      : Def20: s in ( AtomicFormulaSymbolsOf S);

    end

    definition

      let S be ZeroOneStr;

      let s be Element of (the carrier of S \ {the OneF of S});

      :: FOMODEL1:def21

      func TrivialArity (s) -> Integer equals

      : Def21: ( - 2) if s = the ZeroF of S

      otherwise 0 ;

      coherence ;

      consistency ;

    end

    definition

      let S be ZeroOneStr;

      let s be Element of (the carrier of S \ {the OneF of S});

      :: original: TrivialArity

      redefine

      func TrivialArity (s) -> Element of INT ;

      coherence by INT_1:def 2;

    end

    definition

      let S be non degenerated ZeroOneStr;

      :: FOMODEL1:def22

      func S TrivialArity -> Function of (the carrier of S \ {the OneF of S}), INT means

      : Def22: for s be Element of (the carrier of S \ {the OneF of S}) holds (it . s) = ( TrivialArity s);

      existence

      proof

        set D = (the carrier of S \ {the OneF of S});

        deffunc F( Element of D) = ( TrivialArity $1);

        consider f be Function of D, INT such that

         A1: for x be Element of D holds (f . x) = F(x) from FUNCT_2:sch 4;

        take f;

        thus thesis by A1;

      end;

      uniqueness

      proof

        set D = (the carrier of S \ {the OneF of S});

        let IT1,IT2 be Function of D, INT ;

        

         A2: ( dom IT1) = D & ( dom IT2) = D by FUNCT_2:def 1;

        assume

         A3: for s be Element of D holds (IT1 . s) = ( TrivialArity s);

        assume

         A4: for s be Element of D holds (IT2 . s) = ( TrivialArity s);

        now

          let x be object;

          assume x in ( dom IT1);

          then

          reconsider s = x as Element of D;

          (IT1 . s) = ( TrivialArity s) by A3

          .= (IT2 . s) by A4;

          hence (IT1 . x) = (IT2 . x);

        end;

        hence thesis by A2, FUNCT_1: 2;

      end;

    end

    registration

      cluster infinite for non degenerated ZeroOneStr;

      existence

      proof

        set X = the infinite set, Z = the Element of X, O = the Element of (X \ {Z});

        reconsider Y = (X \ {Z}) as infinite set;

         not O in {Z} by XBOOLE_0:def 5;

        then

         A1: O <> Z by TARSKI:def 1;

        reconsider OO = O as Element of X;

        set S = ZeroOneStr (# X, Z, OO #);

        ( 1. S) = OO & ( 0. S) = Z;

        then

        reconsider SS = S as non degenerated ZeroOneStr by A1, STRUCT_0:def 8;

        take SS;

        thus thesis;

      end;

    end

    registration

      let S be infinite non degenerated ZeroOneStr;

      cluster ((S TrivialArity ) " { 0 }) -> infinite;

      coherence

      proof

        set I = the carrier of S, F0 = {the ZeroF of S}, F1 = {the OneF of S}, D1 = (I \ F1), D0 = (D1 \ F0), f = (S TrivialArity );

        

         A1: ( dom f) = D1 by FUNCT_2:def 1;

        for x be object st x in D0 holds x in (f " { 0 })

        proof

          let x be object;

          assume

           A2: x in D0;

          then

          reconsider xx = x as Element of D1;

           not xx in F0 by A2, XBOOLE_0:def 5;

          then xx <> the ZeroF of S by TARSKI:def 1;

          then ( TrivialArity xx) = 0 & (f . xx) = ( TrivialArity xx) by Def21, Def22;

          then xx in ( dom f) & (f . xx) in { 0 } by TARSKI:def 1, A1;

          hence thesis by FUNCT_1:def 7;

        end;

        then

         A3: D0 c= (f " { 0 }) by TARSKI:def 3;

        reconsider D11 = D1 as infinite set;

        thus thesis by A3;

      end;

    end

    

     Lm1: for S be non degenerated ZeroOneStr holds ((S TrivialArity ) . the ZeroF of S) = ( - 2)

    proof

      let S be non degenerated ZeroOneStr;

      set f = (S TrivialArity ), x0 = the ZeroF of S, x1 = the OneF of S;

      x0 = ( 0. S) & x1 = ( 1. S) & ( 0. S) <> ( 1. S);

      then not x0 in {x1} by TARSKI:def 1;

      then

      reconsider x = x0 as Element of (the carrier of S \ {the OneF of S}) by XBOOLE_0:def 5;

      (f . x) = ( TrivialArity x) by Def22

      .= ( - 2) by Def21;

      hence thesis;

    end;

    definition

      let S be Language-like;

      :: FOMODEL1:def23

      attr S is eligible means

      : Def23: ( LettersOf S) is infinite & (the adicity of S . ( TheEqSymbOf S)) = ( - 2);

    end

    

     Lm2: ex S be Language-like st S is non degenerated & S is eligible

    proof

      set SS = the infinite non degenerated ZeroOneStr;

      

       A1: ( 0. SS) <> ( 1. SS);

      set f = (SS TrivialArity );

      take S = Language-like (# the carrier of SS, the ZeroF of SS, the OneF of SS, f #);

      ( 0. S) <> ( 1. S) by A1;

      hence S is non degenerated;

      set g = the adicity of S;

      thus ( LettersOf S) is infinite;

      thus thesis by Lm1;

    end;

    registration

      cluster non degenerated for Language-like;

      existence by Lm2;

    end

    registration

      cluster eligible for non degenerated Language-like;

      existence by Lm2;

    end

    definition

      mode Language is eligible non degenerated Language-like;

    end

    reserve S,S1,S2 for Language,

s,s1,s2 for Element of S;

    definition

      let S be non empty Language-like;

      :: original: AllSymbolsOf

      redefine

      func AllSymbolsOf S -> non empty set ;

      coherence ;

    end

    registration

      let S be eligible Language-like;

      cluster ( LettersOf S) -> infinite;

      coherence by Def23;

    end

    definition

      let S be Language;

      :: original: LettersOf

      redefine

      func LettersOf S -> non empty Subset of ( AllSymbolsOf S) ;

      coherence by XBOOLE_1: 1;

    end

    

     Lm3: for S be non degenerated Language-like holds ( TheEqSymbOf S) in (( AllSymbolsOf S) \ {( TheNorSymbOf S)})

    proof

      let S be non degenerated Language-like;

      set EQ = ( TheEqSymbOf S), NOR = ( TheNorSymbOf S), SS = ( AllSymbolsOf S);

      ( 1. S) <> ( 0. S) & EQ = ( 0. S) & NOR = ( 1. S);

      then EQ in SS & not EQ in {NOR} by TARSKI:def 1;

      hence thesis by XBOOLE_0:def 5;

    end;

    registration

      let S be Language;

      cluster ( TheEqSymbOf S) -> relational;

      coherence

      proof

        set E = ( TheEqSymbOf S), R = ( RelSymbolsOf S), a = the adicity of S, D = (( AllSymbolsOf S) \ {( TheNorSymbOf S)});

        ( - 2) in INT & not ( - 2) in NAT by INT_1:def 2;

        then

         A1: ( - 2) in ( INT \ NAT ) by XBOOLE_0:def 5;

        E in D & ( dom a) = D by FUNCT_2:def 1, Lm3;

        then E in ( dom a) & (a . E) in ( INT \ NAT ) by A1, Def23;

        then E in R by FUNCT_1:def 7;

        hence thesis;

      end;

    end

    definition

      let S be non degenerated Language-like;

      :: original: AtomicFormulaSymbolsOf

      redefine

      func AtomicFormulaSymbolsOf S -> non empty Subset of ( AllSymbolsOf S) ;

      coherence ;

    end

    definition

      let S;

      :: original: TheEqSymbOf

      redefine

      func TheEqSymbOf S -> Element of S ;

      coherence ;

    end

    theorem :: FOMODEL1:1

    

     Th1: for S be Language holds (( LettersOf S) /\ ( OpSymbolsOf S)) = {} & (( TermSymbolsOf S) /\ ( LowerCompoundersOf S)) = ( OpSymbolsOf S) & (( RelSymbolsOf S) \ ( OwnSymbolsOf S)) = {( TheEqSymbOf S)} & ( OwnSymbolsOf S) c= ( AtomicFormulaSymbolsOf S) & ( RelSymbolsOf S) c= ( LowerCompoundersOf S) & ( OpSymbolsOf S) c= ( TermSymbolsOf S) & ( LettersOf S) c= ( TermSymbolsOf S) & ( TermSymbolsOf S) c= ( OwnSymbolsOf S) & ( OpSymbolsOf S) c= ( LowerCompoundersOf S) & ( LowerCompoundersOf S) c= ( AtomicFormulaSymbolsOf S)

    proof

      let S be Language;

      set o = the OneF of S, z = the ZeroF of S, f = the adicity of S, R = ( RelSymbolsOf S), O = ( OwnSymbolsOf S), SS = ( AllSymbolsOf S), e = ( TheEqSymbOf S), n = ( TheNorSymbOf S), A = ( AtomicFormulaSymbolsOf S), D = (the carrier of S \ {o}), L = ( LowerCompoundersOf S), T = ( TermSymbolsOf S), OP = ( OpSymbolsOf S), B = ( LettersOf S);

      

      thus (B /\ OP) = (f " ( { 0 } /\ ( NAT \ { 0 }))) by FUNCT_1: 68

      .= (f " {} ) by XBOOLE_1: 79, XBOOLE_0:def 7

      .= {} ;

      

      thus (T /\ L) = (f " ( NAT /\ ( INT \ { 0 }))) by FUNCT_1: 68

      .= (f " (( NAT /\ INT ) \ { 0 })) by XBOOLE_1: 49

      .= OP by XBOOLE_1: 28, XBOOLE_1: 7;

      

       A1: ( TheEqSymbOf S) in R by Def17;

      O = (D \ {z}) by XBOOLE_1: 41;

      

      then (R \ O) = ((R \ D) \/ (R /\ {z})) by XBOOLE_1: 52

      .= ( {} \/ (R /\ {z}))

      .= {z} by ZFMISC_1: 46, A1;

      hence (R \ O) = {( TheEqSymbOf S)};

      thus ( OwnSymbolsOf S) c= ( AtomicFormulaSymbolsOf S) by XBOOLE_1: 34, ZFMISC_1: 7;

      (f " { 0 }) c= (f " NAT ) & ( RelSymbolsOf S) = ((f " INT ) \ (f " NAT )) & ( LowerCompoundersOf S) = ((f " INT ) \ (f " { 0 })) by FUNCT_1: 69, RELAT_1: 143;

      hence ( RelSymbolsOf S) c= ( LowerCompoundersOf S) by XBOOLE_1: 34;

      ( OpSymbolsOf S) = ((f " NAT ) \ (f " { 0 })) by FUNCT_1: 69;

      hence ( OpSymbolsOf S) c= ( TermSymbolsOf S);

      thus ( LettersOf S) c= ( TermSymbolsOf S) by RELAT_1: 143;

      ( - 2) = (f . ( TheEqSymbOf S)) by Def23

      .= (f . z);

      then not (f . z) in NAT ;

      then not z in (f " NAT ) by FUNCT_1:def 7;

      then (f " NAT ) misses {z} & (f " NAT ) c= (the carrier of S \ {o}) by ZFMISC_1: 50;

      then (f " NAT ) c= ((the carrier of S \ {o}) \ {z}) by XBOOLE_1: 86;

      hence ( TermSymbolsOf S) c= ( OwnSymbolsOf S) by XBOOLE_1: 41;

      for x be object st x in NAT holds x in INT by INT_1:def 2;

      then ( NAT \ { 0 }) c= ( INT \ { 0 }) by XBOOLE_1: 33, TARSKI:def 3;

      hence ( OpSymbolsOf S) c= ( LowerCompoundersOf S) by RELAT_1: 143;

      thus thesis;

    end;

    registration

      let S be Language;

      cluster ( TermSymbolsOf S) -> non empty;

      coherence

      proof

        ( LettersOf S) c= ( TermSymbolsOf S) by Th1;

        hence thesis;

      end;

      cluster own -> ofAtomicFormula for Element of S;

      coherence

      proof

        let s be Element of S;

        assume s is own;

        then s in ( OwnSymbolsOf S) & ( OwnSymbolsOf S) c= ( AtomicFormulaSymbolsOf S) by Th1;

        hence thesis;

      end;

      cluster relational -> low-compounding for Element of S;

      coherence

      proof

        let s be Element of S;

        assume s is relational;

        then s in ( RelSymbolsOf S) & ( RelSymbolsOf S) c= ( LowerCompoundersOf S) by Th1;

        hence s is low-compounding;

      end;

      cluster operational -> termal for Element of S;

      coherence

      proof

        let s be Element of S;

        assume s is operational;

        then s in ( OpSymbolsOf S) & ( OpSymbolsOf S) c= ( TermSymbolsOf S) by Th1;

        hence thesis;

      end;

      cluster literal -> termal for Element of S;

      coherence

      proof

        let s be Element of S;

        assume s is literal;

        then ( LettersOf S) c= ( TermSymbolsOf S) & s in ( LettersOf S) by Th1;

        hence thesis;

      end;

      cluster termal -> own for Element of S;

      coherence

      proof

        let s be Element of S;

        assume s is termal;

        then ( TermSymbolsOf S) c= ( OwnSymbolsOf S) & s in ( TermSymbolsOf S) by Th1;

        hence thesis;

      end;

      cluster operational -> low-compounding for Element of S;

      coherence

      proof

        let s be Element of S;

        assume s is operational;

        then s in ( OpSymbolsOf S) & ( OpSymbolsOf S) c= ( LowerCompoundersOf S) by Th1;

        hence thesis;

      end;

      cluster low-compounding -> ofAtomicFormula for Element of S;

      coherence ;

      cluster termal -> non relational for Element of S;

      coherence

      proof

        set T = ( TermSymbolsOf S), R = ( RelSymbolsOf S), f = the adicity of S;

        (T /\ R) = (f " ( NAT /\ ( INT \ NAT ))) by FUNCT_1: 68

        .= (f " (( NAT /\ INT ) \ ( NAT /\ NAT )))

        .= {} ;

        then

         A1: (T \ R) = T by XBOOLE_1: 83, XBOOLE_0:def 7;

        let s be Element of S;

        assume s is termal;

        then s in (T \ R) by A1;

        then not s in R by XBOOLE_0:def 5;

        hence thesis;

      end;

      cluster literal -> non relational for Element of S;

      coherence ;

      cluster literal -> non operational for Element of S;

      coherence

      proof

        set L = ( LettersOf S), P = ( OpSymbolsOf S);

        let s be Element of S;

        assume

         A2: s is literal;

        assume s is operational;

        then s in L & s in P by A2;

        then s in (L /\ P) by XBOOLE_0:def 4;

        hence contradiction by Th1;

      end;

    end

    registration

      let S be Language;

      cluster relational for Element of S;

      existence

      proof

        take s = ( TheEqSymbOf S);

        thus thesis;

      end;

      cluster literal for Element of S;

      existence

      proof

        set s = the Element of ( LettersOf S);

        take s;

        thus thesis;

      end;

    end

    registration

      let S be Language;

      cluster termal -> operational for low-compounding Element of S;

      coherence

      proof

        set L = ( LowerCompoundersOf S), T = ( TermSymbolsOf S), OP = ( OpSymbolsOf S);

        let s be low-compounding Element of S;

        

         A1: s in L by Def15;

        assume s is termal;

        then s in T;

        then s in (L /\ T) by XBOOLE_0:def 4, A1;

        then s in OP by Th1;

        hence thesis;

      end;

    end

    registration

      let S be Language;

      cluster ofAtomicFormula for Element of S;

      existence

      proof

        set s = the literal Element of S;

        take s;

        thus thesis;

      end;

    end

    definition

      let S be Language;

      let s be ofAtomicFormula Element of S;

      :: FOMODEL1:def24

      func ar (s) -> Element of INT equals (the adicity of S . s);

      coherence

      proof

        set f = the adicity of S;

        reconsider g = f as Function of ( AtomicFormulaSymbolsOf S), INT ;

        reconsider ss = s as Element of ( AtomicFormulaSymbolsOf S) by Def20;

        (g . ss) in INT ;

        hence thesis;

      end;

    end

    registration

      let S be Language;

      let s be literal Element of S;

      cluster ( ar s) -> zero;

      coherence

      proof

        set f = the adicity of S;

        s in ( LettersOf S) by Def14;

        then (f . s) in { 0 } by FUNCT_1:def 7;

        hence thesis;

      end;

    end

    definition

      let S be Language;

      :: FOMODEL1:def25

      func S -cons -> BinOp of (( AllSymbolsOf S) * ) equals (( AllSymbolsOf S) -concatenation );

      coherence ;

    end

    definition

      let S be Language;

      :: FOMODEL1:def26

      func S -multiCat -> Function of ((( AllSymbolsOf S) * ) * ), (( AllSymbolsOf S) * ) equals (( AllSymbolsOf S) -multiCat );

      coherence ;

    end

    definition

      let S be Language;

      :: FOMODEL1:def27

      func S -firstChar -> Function of ((( AllSymbolsOf S) * ) \ { {} }), ( AllSymbolsOf S) equals (( AllSymbolsOf S) -firstChar );

      coherence ;

    end

    definition

      let S be Language;

      let X be set;

      :: FOMODEL1:def28

      attr X is S -prefix means

      : Def28: X is ( AllSymbolsOf S) -prefix;

    end

    registration

      let S be Language;

      cluster S -prefix -> ( AllSymbolsOf S) -prefix for set;

      coherence ;

      cluster ( AllSymbolsOf S) -prefix -> S -prefix for set;

      coherence ;

    end

    definition

      let S be Language;

      mode string of S is Element of ((( AllSymbolsOf S) * ) \ { {} });

    end

    registration

      let S;

      cluster ((( AllSymbolsOf S) * ) \ { {} }) -> non empty;

      coherence ;

    end

    registration

      let S;

      cluster -> non empty for string of S;

      coherence ;

    end

    registration

      cluster -> infinite for Language;

      coherence

      proof

        let S be Language;

        set SS = ( AllSymbolsOf S), L = ( LettersOf S);

        reconsider S0 = S as 1-sorted;

        (L \/ SS) = SS by XBOOLE_1: 12;

        hence thesis;

      end;

    end

    registration

      let S be Language;

      cluster ( AllSymbolsOf S) -> infinite;

      coherence ;

    end

    definition

      let S be Language;

      let s be ofAtomicFormula Element of S;

      let Strings be set;

      :: FOMODEL1:def29

      func Compound (s,Strings) -> set equals { ( <*s*> ^ ((S -multiCat ) . StringTuple)) where StringTuple be Element of ((( AllSymbolsOf S) * ) * ) : ( rng StringTuple) c= Strings & StringTuple is |.( ar s).| -element };

      coherence ;

    end

    definition

      let S be Language;

      let s be ofAtomicFormula Element of S;

      let Strings be set;

      :: original: Compound

      redefine

      func Compound (s,Strings) -> Element of ( bool ((( AllSymbolsOf S) * ) \ { {} })) ;

      coherence

      proof

        set Y = ( Compound (s,Strings)), SS = ( AllSymbolsOf S);

        reconsider ss = s as Element of SS;

        now

          let x be object;

          assume x in Y;

          then

          consider StringTuple be Element of ((SS * ) * ) such that

           A1: x = ( <*s*> ^ ((S -multiCat ) . StringTuple)) & ( rng StringTuple) c= Strings & StringTuple is |.( ar s).| -element;

          reconsider head = <*ss*> as non empty FinSequence of SS;

          reconsider tail = ((S -multiCat ) . StringTuple) as FinSequence of SS by FINSEQ_1:def 11;

          (head ^ tail) is non empty FinSequence of SS & x = (head ^ tail) by A1;

          hence x in ((SS * ) \ { {} }) by FOMODEL0: 5;

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    definition

      let S be Language;

      :: FOMODEL1:def30

      func S -termsOfMaxDepth -> Function means

      : Def30: ( dom it ) = NAT & (it . 0 ) = ( AtomicTermsOf S) & for n be Nat holds (it . (n + 1)) = (( union { ( Compound (s,(it . n))) where s be ofAtomicFormula Element of S : s is operational }) \/ (it . n));

      existence

      proof

        deffunc F( set, set) = (( union { ( Compound (s,$2)) where s be ofAtomicFormula Element of S : s is operational }) \/ $2);

        ex f be Function st ( dom f) = NAT & (f . 0 ) = ( AtomicTermsOf S) & for n be Nat holds (f . (n + 1)) = F(n,.) from NAT_1:sch 11;

        hence thesis;

      end;

      uniqueness

      proof

        deffunc F( set, set) = (( union { ( Compound (s,$2)) where s be ofAtomicFormula Element of S : s is operational }) \/ $2);

        let IT1,IT2 be Function;

        assume

         A1: ( dom IT1) = NAT & (IT1 . 0 ) = ( AtomicTermsOf S) & for n be Nat holds (IT1 . (n + 1)) = F(n,.);

        

         A2: ( dom IT1) = NAT by A1;

        

         A3: (IT1 . 0 ) = ( AtomicTermsOf S) by A1;

        

         A4: for n be Nat holds (IT1 . (n + 1)) = F(n,.) by A1;

        assume

         A5: ( dom IT2) = NAT & (IT2 . 0 ) = ( AtomicTermsOf S) & for n be Nat holds (IT2 . (n + 1)) = F(n,.);

        

         A6: ( dom IT2) = NAT by A5;

        

         A7: (IT2 . 0 ) = ( AtomicTermsOf S) by A5;

        

         A8: for n be Nat holds (IT2 . (n + 1)) = F(n,.) by A5;

        thus IT1 = IT2 from NAT_1:sch 15( A2, A3, A4, A6, A7, A8);

      end;

    end

    definition

      let S;

      :: original: AtomicTermsOf

      redefine

      func AtomicTermsOf S -> Subset of (( AllSymbolsOf S) * ) ;

      coherence

      proof

        set SS = ( AllSymbolsOf S), A = ( AtomicTermsOf S);

        reconsider L = ( LettersOf S) as Subset of SS;

        A c= (L * ) by FINSEQ_2: 134;

        hence thesis by XBOOLE_1: 1;

      end;

    end

    

     Lm4: ((S -termsOfMaxDepth ) . m) c= ((( AllSymbolsOf S) * ) \ { {} })

    proof

      set T = (S -termsOfMaxDepth ), SS = ( AllSymbolsOf S), L = ( LettersOf S);

      defpred P[ Nat] means (T . $1) c= ((SS * ) \ { {} });

      

       A1: P[ 0 ]

      proof

        (T . 0 ) = ( AtomicTermsOf S) by Def30

        .= (( 0 + 1) -tuples_on L);

        then

         A2: (T . 0 ) c= ((L * ) \ { {} }) by FOMODEL0: 9;

        ((L * ) \ { {} }) c= ((SS * ) \ { {} }) by XBOOLE_1: 33;

        hence thesis by A2, XBOOLE_1: 1;

      end;

      

       A3: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume

         A4: P[n];

        set TM1 = { ( Compound (s,(T . n))) where s be ofAtomicFormula Element of S : s is operational };

        now

          let X be set;

          assume X in TM1;

          then

          consider s be ofAtomicFormula Element of S such that

           A5: X = ( Compound (s,(T . n))) & s is operational;

          thus X c= ((SS * ) \ { {} }) by A5;

        end;

        then ( union TM1) c= ((SS * ) \ { {} }) & (T . (n + 1)) = (( union TM1) \/ (T . n)) by Def30, ZFMISC_1: 76;

        hence thesis by A4, XBOOLE_1: 8;

      end;

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

      hence thesis;

    end;

    

     Lm5: ((S -termsOfMaxDepth ) . m) c= ((S -termsOfMaxDepth ) . (m + n))

    proof

      set T = (S -termsOfMaxDepth );

      defpred P[ Nat] means (T . m) c= (T . (m + $1));

      

       A1: P[ 0 ];

      

       A2: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume

         A3: P[n];

        (T . ((m + n) + 1)) = ((T . (m + n)) \/ ( union { ( Compound (s,(T . (m + n)))) where s be ofAtomicFormula Element of S : s is operational })) by Def30;

        then (T . (m + n)) c= (T . ((m + n) + 1)) by XBOOLE_1: 7;

        hence thesis by A3, XBOOLE_1: 1;

      end;

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

      hence thesis;

    end;

    definition

      let S be Language;

      :: FOMODEL1:def31

      func AllTermsOf S -> set equals ( union ( rng (S -termsOfMaxDepth )));

      coherence ;

    end

    theorem :: FOMODEL1:2

    

     Th2: ((S -termsOfMaxDepth ) . mm) c= ( AllTermsOf S)

    proof

      set T = (S -termsOfMaxDepth );

      ( dom T) = NAT by Def30;

      hence thesis by ZFMISC_1: 74, FUNCT_1: 3;

    end;

    

     Lm6: x in ( AllTermsOf S) implies ex nn st x in ((S -termsOfMaxDepth ) . nn)

    proof

      set T = (S -termsOfMaxDepth );

      assume x in ( AllTermsOf S);

      then

      consider Y be set such that

       A1: x in Y & Y in ( rng T) by TARSKI:def 4;

      consider mmm be object such that

       A2: mmm in ( dom T) & Y = (T . mmm) by A1, FUNCT_1:def 3;

      reconsider mm = mmm as Element of NAT by A2, Def30;

      take nn = mm;

      thus thesis by A1, A2;

    end;

    definition

      let S be Language;

      let w be string of S;

      :: FOMODEL1:def32

      attr w is termal means

      : Def32: w in ( AllTermsOf S);

    end

    definition

      let m be Nat;

      let S be Language;

      let w be string of S;

      :: FOMODEL1:def33

      attr w is m -termal means

      : Def33: w in ((S -termsOfMaxDepth ) . m);

    end

    registration

      let m be Nat;

      let S be Language;

      cluster m -termal -> termal for string of S;

      coherence

      proof

        reconsider mm = m as Element of NAT by ORDINAL1:def 12;

        let w be string of S;

        assume w is m -termal;

        then w in ((S -termsOfMaxDepth ) . m) & ((S -termsOfMaxDepth ) . mm) c= ( AllTermsOf S) by Th2;

        hence thesis;

      end;

    end

    definition

      let S;

      :: original: -termsOfMaxDepth

      redefine

      func S -termsOfMaxDepth -> sequence of ( bool (( AllSymbolsOf S) * )) ;

      coherence

      proof

        set SS = ( AllSymbolsOf S), T = (S -termsOfMaxDepth );

        

         A1: ( dom T) = NAT by Def30;

        now

          let y be object;

          reconsider yy = y as set by TARSKI: 1;

          assume y in ( rng T);

          then

          consider x be object such that

           A2: x in ( dom T) & y = (T . x) by FUNCT_1:def 3;

          reconsider m = x as Element of NAT by Def30, A2;

          y = (T . m) by A2;

          then yy c= ((SS * ) \ { {} }) & ((SS * ) \ { {} }) c= (SS * ) by Lm4;

          then yy c= (SS * ) by XBOOLE_1: 1;

          hence y in ( bool (SS * ));

        end;

        then ( rng T) c= ( bool (SS * )) by TARSKI:def 3;

        hence thesis by A1, RELSET_1: 4, FUNCT_2: 67;

      end;

    end

    definition

      let S;

      :: original: AllTermsOf

      redefine

      func AllTermsOf S -> non empty Subset of (( AllSymbolsOf S) * ) ;

      coherence

      proof

        set A = ( AllTermsOf S), T = (S -termsOfMaxDepth ), SS = ( AllSymbolsOf S);

         A1:

        now

          let x be object;

          assume x in A;

          then

          consider mm be Element of NAT such that

           A2: x in (T . mm) by Lm6;

          thus x in (SS * ) by A2;

        end;

        A = ((T . 0 ) \/ A) by Th2, XBOOLE_1: 12

        .= (( AtomicTermsOf S) \/ A) by Def30;

        hence thesis by A1, TARSKI:def 3;

      end;

    end

    registration

      let S;

      cluster ( AllTermsOf S) -> non empty;

      coherence ;

    end

    registration

      let S, m;

      cluster ((S -termsOfMaxDepth ) . m) -> non empty;

      coherence

      proof

        set T = (S -termsOfMaxDepth ), Z = ( AtomicTermsOf S), SS = ( AllSymbolsOf S), x = the Element of Z;

        x in Z & Z = (T . 0 ) by Def30;

        then x in (T . 0 ) & (T . 0 ) c= (T . ( 0 + m)) by Lm5;

        hence (T . m) is non empty;

      end;

    end

    registration

      let S, m;

      cluster -> non empty for Element of ((S -termsOfMaxDepth ) . m);

      coherence

      proof

        set T = (S -termsOfMaxDepth ), SS = ( AllSymbolsOf S), A = ( AtomicTermsOf S);

        let w be Element of (T . m);

        w in ((SS * ) \ { {} }) by Lm4, TARSKI:def 3;

        hence thesis;

      end;

    end

    registration

      let S;

      cluster -> non empty for Element of ( AllTermsOf S);

      coherence

      proof

        set T = (S -termsOfMaxDepth ), SS = ( AllSymbolsOf S), A = ( AtomicTermsOf S), AA = ( AllTermsOf S);

        let t be Element of AA;

        consider mm such that

         A1: t in (T . mm) by Lm6;

        reconsider tt = t as Element of (T . mm) by A1;

        tt is non empty;

        hence thesis;

      end;

    end

    registration

      let m be Nat, S be Language;

      cluster m -termal for string of S;

      existence

      proof

        set T = (S -termsOfMaxDepth ), SS = ( AllSymbolsOf S), A = ( AtomicTermsOf S), w = the Element of A;

        

         A1: w in A;

        then w in (T . 0 ) & (T . 0 ) c= ((SS * ) \ { {} }) by Lm4, Def30;

        then

        reconsider ww = w as string of S;

        take ww;

        ww in (T . 0 ) & (T . 0 ) c= (T . ( 0 + m)) by Lm5, A1, Def30;

        hence thesis;

      end;

    end

    registration

      let S;

      cluster 0 -termal -> 1 -element for string of S;

      coherence

      proof

        set A = ( AtomicTermsOf S), L = ( LettersOf S), T = (S -termsOfMaxDepth );

        let w be string of S;

        assume w is 0 -termal;

        then w in (T . 0 );

        then w in A by Def30;

        then

        reconsider ww = w as Element of (1 -tuples_on L);

        ww is 1 -element;

        hence thesis;

      end;

    end

    registration

      let S be Language;

      let w be 0 -termal string of S;

      cluster ((S -firstChar ) . w) -> literal;

      coherence

      proof

        set A = ( AllTermsOf S), T = (S -termsOfMaxDepth ), Z = ( AtomicTermsOf S), SS = ( AllSymbolsOf S), s = ((S -firstChar ) . w), ss = ((SS -firstChar ) . w), L = ( LettersOf S);

        reconsider ww = w as non empty FinSequence of SS by FOMODEL0: 5;

        

         A1: ss = (ww . 1) by FOMODEL0: 6;

        w in (T . 0 ) by Def33;

        then w in Z by Def30;

        then

        consider x such that

         A2: x in L & w = <*x*> by FINSEQ_2: 135;

        w = ( <*x*> ^ {} ) by A2;

        then ss in L by FINSEQ_1: 41, A2, A1;

        hence thesis;

      end;

    end

    

     Lm7: for w be (mm + 1) -termal string of S st not w is mm -termal holds ex s be termal Element of S, T be Element of (((S -termsOfMaxDepth ) . mm) * ) st T is |.( ar s).| -element & w = ( <*s*> ^ ((S -multiCat ) . T))

    proof

      set fam = { ( Compound (s,((S -termsOfMaxDepth ) . mm))) where s be ofAtomicFormula Element of S : s is operational };

      let w be (mm + 1) -termal string of S;

      assume not w is mm -termal;

      then w in ((S -termsOfMaxDepth ) . (mm + 1)) & not w in ((S -termsOfMaxDepth ) . mm) by Def33;

      then w in (( union fam) \/ ((S -termsOfMaxDepth ) . mm)) & not w in ((S -termsOfMaxDepth ) . mm) by Def30;

      then w in ( union fam) by XBOOLE_0:def 3;

      then

      consider C be set such that

       A1: w in C & C in fam by TARSKI:def 4;

      consider sss be ofAtomicFormula Element of S such that

       A2: C = ( Compound (sss,((S -termsOfMaxDepth ) . mm))) & sss is operational by A1;

      reconsider ss = sss as termal Element of S by A2;

      take s = ss;

      consider StringTuple be Element of ((( AllSymbolsOf S) * ) * ) such that

       A3: w = ( <*s*> ^ ((S -multiCat ) . StringTuple)) & ( rng StringTuple) c= ((S -termsOfMaxDepth ) . mm) & StringTuple is |.( ar ss).| -element by A1, A2;

      reconsider TT = StringTuple as FinSequence of ((S -termsOfMaxDepth ) . mm) by A3, FINSEQ_1:def 4;

      reconsider TTT = TT as Element of (((S -termsOfMaxDepth ) . mm) * );

      take T = TTT;

      thus T is |.( ar s).| -element by A3;

      thus thesis by A3;

    end;

    

     Lm8: for w be (mm + 1) -termal string of S holds ex s be termal Element of S, T be Element of (((S -termsOfMaxDepth ) . mm) * ) st T is |.( ar s).| -element & w = ( <*s*> ^ ((S -multiCat ) . T))

    proof

      set TS = ( TermSymbolsOf S), T = (S -termsOfMaxDepth ), C = (S -multiCat ), L = ( LettersOf S);

      defpred P[ Element of omega ] means for w be ($1 + 1) -termal string of S holds ex s be termal Element of S, T be Element of (((S -termsOfMaxDepth ) . $1) * ) st T is |.( ar s).| -element & w = ( <*s*> ^ ((S -multiCat ) . T));

      defpred Q[ Nat] means ex mm be Element of NAT st mm = $1 & P[mm];

      

       A1: Q[ 0 ]

      proof

        take 0 ;

        thus 0 = 0 ;

        thus P[ 0 ]

        proof

          let w be ( 0 + 1) -termal string of S;

          per cases ;

            suppose w is 0 -termal;

            then w in ((S -termsOfMaxDepth ) . 0 );

            then w in ( AtomicTermsOf S) by Def30;

            then w in the set of all <*ss*> where ss be Element of ( LettersOf S) by FINSEQ_2: 96;

            then

            consider ss be Element of ( LettersOf S) such that

             A2: w = <*ss*>;

            reconsider sss = ss as literal Element of S by Def14;

            reconsider TT = {} as FinSequence;

            ( rng TT) = {} ;

            then

            reconsider TTT = TT as FinSequence of ((S -termsOfMaxDepth ) . 0 ) by XBOOLE_1: 2, FINSEQ_1:def 4;

            reconsider TTTT = TTT as Element of (((S -termsOfMaxDepth ) . 0 ) * );

            take s = sss;

            take T = TTTT;

            thus T is |.( ar s).| -element;

            reconsider s = sss as Element of TS by Def18;

            ((S -multiCat ) . {} ) = {} & ( <*sss*> ^ {} ) = <*sss*>;

            hence thesis by A2;

          end;

            suppose w is non 0 -termal;

            hence thesis by Lm7;

          end;

        end;

      end;

      

       A3: for m be Nat st Q[m] holds Q[(m + 1)]

      proof

        let m be Nat;

        reconsider mm = m, mmm = (m + 1) as Element of NAT by ORDINAL1:def 12;

        assume

         A4: Q[m];

        take mmm;

        thus mmm = (m + 1);

        let w be (mmm + 1) -termal string of S;

        per cases ;

          suppose not w is mmm -termal;

          hence thesis by Lm7;

        end;

          suppose w is mmm -termal;

          then

          consider s be termal Element of S, T be Element of (((S -termsOfMaxDepth ) . mm) * ) such that

           A5: T is |.( ar s).| -element & w = ( <*s*> ^ ((S -multiCat ) . T)) by A4;

          set high = ((S -termsOfMaxDepth ) . mmm);

          reconsider low = ((S -termsOfMaxDepth ) . mm) as Subset of high by Lm5;

          T in (low * ) & (low * ) is Subset of (high * );

          then

          reconsider TT = T as Element of (high * );

          take s, TT;

          thus thesis by A5;

        end;

      end;

      

       A6: for m be Nat holds Q[m] from NAT_1:sch 2( A1, A3);

      now

        let mm be Element of NAT ;

        reconsider m = mm as Nat;

        consider nn be Element of NAT such that

         A7: nn = m & P[nn] by A6;

        thus P[mm] by A7;

      end;

      hence thesis;

    end;

    registration

      let S;

      let w be termal string of S;

      cluster ((S -firstChar ) . w) -> termal;

      coherence

      proof

        set A = ( AllTermsOf S), T = (S -termsOfMaxDepth ), Z = ( AtomicTermsOf S), SS = ( AllSymbolsOf S), s = ((S -firstChar ) . w), ss = ((SS -firstChar ) . w), L = ( LettersOf S);

        w in A by Def32;

        then

        consider mm such that

         A1: w in (T . mm) by Lm6;

        reconsider ww = w as non empty FinSequence of SS by FOMODEL0: 5;

        

         A2: ss = (ww . 1) by FOMODEL0: 6;

        per cases ;

          suppose mm = 0 ;

          then

          reconsider www = w as 0 -termal string of S by Def33, A1;

          ((S -firstChar ) . www) is literal;

          hence thesis;

        end;

          suppose mm <> 0 ;

          then

          consider n be Nat such that

           A3: mm = (n + 1) by NAT_1: 6;

          reconsider nn = n as Element of NAT by ORDINAL1:def 12;

          reconsider www = w as (nn + 1) -termal string of S by A3, A1, Def33;

          consider s1 be termal Element of S, T1 be Element of ((T . nn) * ) such that

           A4: T1 is |.( ar s1).| -element & www = ( <*s1*> ^ ((S -multiCat ) . T1)) by Lm8;

          thus thesis by FINSEQ_1: 41, A4, A2;

        end;

      end;

    end

    definition

      let S;

      let t be termal string of S;

      :: FOMODEL1:def34

      func ar (t) -> Element of INT equals ( ar ((S -firstChar ) . t));

      coherence ;

    end

    theorem :: FOMODEL1:3

    

     Th3: for w be (mm + 1) -termal string of S holds ex T be Element of (((S -termsOfMaxDepth ) . mm) * ) st T is |.( ar ((S -firstChar ) . w)).| -element & w = ( <*((S -firstChar ) . w)*> ^ ((S -multiCat ) . T))

    proof

      let w be (mm + 1) -termal string of S;

      consider s be termal Element of S, T be Element of (((S -termsOfMaxDepth ) . mm) * ) such that

       A1: T is |.( ar s).| -element & w = ( <*s*> ^ ((S -multiCat ) . T)) by Lm8;

      reconsider ww = w as non empty FinSequence of ( AllSymbolsOf S) by FINSEQ_1:def 11;

      s = (w . 1) by A1, FINSEQ_1: 41

      .= ((S -firstChar ) . w) by FOMODEL0: 6;

      hence thesis by A1;

    end;

    

     Lm9: ((S -termsOfMaxDepth ) . m) is S -prefix

    proof

      set T = (S -termsOfMaxDepth ), SS = ( AllSymbolsOf S), L = ( LettersOf S), S1 = (1 -tuples_on SS), f = (S -cons ), F = (S -multiCat ), ff = (SS -concatenation ), FF = (SS -multiCat );

      

       A1: ( dom FF) = ((SS * ) * ) by FUNCT_2:def 1;

      reconsider LS = L as non empty Subset of SS;

      set L1 = (1 -tuples_on LS);

      defpred P[ Nat] means (T . $1) is S -prefix;

      

       A2: P[ 0 ]

      proof

        (L1 /\ S1) = (1 -tuples_on (LS /\ SS)) by FOMODEL0: 3

        .= (1 -tuples_on LS) by XBOOLE_1: 28;

        then

        reconsider L11 = (1 -tuples_on LS) as Subset of S1;

        (T . 0 ) = ( AtomicTermsOf S) by Def30

        .= L11;

        hence thesis;

      end;

      

       A3: for m be Nat st P[m] holds P[(m + 1)]

      proof

        let m be Nat;

        assume

         A4: P[m];

        reconsider mm = m, mm1 = (m + 1) as Element of NAT by ORDINAL1:def 12;

        now

          let t1,t2,w1,w2 be set;

          assume

           A5: t1 in ((T . (m + 1)) /\ (SS * )) & t2 in ((T . (m + 1)) /\ (SS * )) & w1 in (SS * ) & w2 in (SS * );

          t1 in (T . mm1) & not t1 in { {} } & t2 in (T . mm1) & not t2 in { {} } by A5;

          then

          reconsider t11 = t1, t22 = t2 as (mm + 1) -termal string of S by Def33, XBOOLE_0:def 5;

          reconsider t111 = t11, t222 = t22 as FinSequence of SS by FINSEQ_1:def 11;

          consider T1 be Element of ((T . mm) * ) such that

           A6: T1 is |.( ar ((S -firstChar ) . t11)).| -element & t11 = ( <*((S -firstChar ) . t11)*> ^ (F . T1)) by Th3;

          consider T2 be Element of ((T . mm) * ) such that

           A7: T2 is |.( ar ((S -firstChar ) . t22)).| -element & t22 = ( <*((S -firstChar ) . t22)*> ^ (F . T2)) by Th3;

          reconsider T11 = T1, T22 = T2 as FinSequence of (T . mm) by FINSEQ_1:def 11;

          reconsider w11 = w1, w22 = w2 as Element of (SS * ) by A5;

          reconsider head1 = (F . T1), head2 = (F . T2), tail1 = w11, tail2 = w22 as FinSequence of SS by FINSEQ_1:def 11;

          assume (f . (t1,w1)) = (f . (t2,w2));

          then (t111 ^ w11) = (f . (t222,w22)) by FOMODEL0: 4;

          then (( <*((S -firstChar ) . t11)*> ^ (F . T1)) ^ w11) = (t222 ^ w22) by FOMODEL0: 4, A6;

          then ( <*((S -firstChar ) . t11)*> ^ ((F . T1) ^ w11)) = (( <*((S -firstChar ) . t22)*> ^ (F . T2)) ^ w22) by A7, FINSEQ_1: 32;

          then ( <*((S -firstChar ) . t11)*> ^ (head1 ^ tail1)) = ( <*((S -firstChar ) . t22)*> ^ (head2 ^ tail2)) by FINSEQ_1: 32;

          then

           A8: (f . ( <*((S -firstChar ) . t11)*>,(head1 ^ tail1))) = ( <*((S -firstChar ) . t22)*> ^ (head2 ^ tail2)) by FOMODEL0: 4;

          (1 -tuples_on SS) c= (1 -tuples_on SS);

          then

          reconsider S1 = (1 -tuples_on SS) as Subset of (1 -tuples_on SS);

          

           A9: S1 is f -unambiguous by FOMODEL0:def 3;

          (S1 /\ (SS * )) = S1 by FINSEQ_2: 134, XBOOLE_1: 28;

          then <*((S -firstChar ) . t11)*> in (S1 /\ (SS * )) & <*((S -firstChar ) . t22)*> in (S1 /\ (SS * )) & (head1 ^ tail1) in (SS * ) & (head2 ^ tail2) in (SS * ) & (f . ( <*((S -firstChar ) . t11)*>,(head1 ^ tail1))) = (f . ( <*((S -firstChar ) . t22)*>,(head2 ^ tail2))) by A8, FOMODEL0: 4, FINSEQ_2: 98;

          then

           A10: <*((S -firstChar ) . t11)*> = <*((S -firstChar ) . t22)*> & (head1 ^ tail1) = (head2 ^ tail2) & (head1 ^ tail1) = (ff . (head1,tail1)) by A9, FOMODEL0: 4;

          

           A11: ((S -firstChar ) . t11) = ((S -firstChar ) . t22) by FINSEQ_1: 76, A10;

          set n = |.( ar ((S -firstChar ) . t11)).|;

          ( len T11) = n & ( len T22) = n by A6, CARD_1:def 7, A11, A7;

          then T11 in (n -tuples_on (T . m)) & T22 in (n -tuples_on (T . m)) & T11 in ( dom FF) & T22 in ( dom FF) by FINSEQ_2: 133, A1;

          then (FF . T11) in (FF .: (n -tuples_on (T . m))) & (FF . T22) in (FF .: (n -tuples_on (T . m))) & (FF . T1) in (SS * ) & (FF . T2) in (SS * ) by FUNCT_1:def 6;

          then

           A12: (FF . T1) in ((FF .: (n -tuples_on (T . m))) /\ (SS * )) & (FF . T2) in ((FF .: (n -tuples_on (T . m))) /\ (SS * )) & w11 in (SS * ) & w22 in (SS * ) & (ff . ((FF . T1),w11)) = (ff . ((FF . T2),w22)) by FOMODEL0: 4, A10, XBOOLE_0:def 4;

          (T . m) is SS -prefix & ((T . m) is SS -prefix implies ((SS -multiCat ) .: (n -tuples_on (T . m))) is SS -prefix) by A4, Def28;

          then ((SS -multiCat ) .: (n -tuples_on (T . m))) is ff -unambiguous;

          hence t1 = t2 & w1 = w2 by A6, A7, A10, A12;

        end;

        then (T . (m + 1)) is SS -prefix by FOMODEL0:def 10;

        hence thesis;

      end;

      for m be Nat holds P[m] from NAT_1:sch 2( A2, A3);

      hence thesis;

    end;

    registration

      let S, m;

      cluster ((S -termsOfMaxDepth ) . m) -> S -prefix;

      coherence by Lm9;

    end

    registration

      let S;

      let V be Element of (( AllTermsOf S) * );

      cluster ((S -multiCat ) . V) -> Relation-like;

      coherence ;

    end

    registration

      let S;

      let V be Element of (( AllTermsOf S) * );

      cluster ((S -multiCat ) . V) -> Function-like;

      coherence ;

    end

    definition

      let S;

      let phi be string of S;

      :: FOMODEL1:def35

      attr phi is 0wff means

      : Def35: ex s be relational Element of S, V be |.( ar s).| -element Element of (( AllTermsOf S) * ) st phi = ( <*s*> ^ ((S -multiCat ) . V));

    end

    registration

      let S;

      cluster 0wff for string of S;

      existence

      proof

        set SS = ( AllSymbolsOf S), s = the relational Element of S, V = the |.( ar s).| -element Element of (( AllTermsOf S) * );

        reconsider ss = s as Element of SS;

        reconsider tail = ((S -multiCat ) . V) as FinSequence of SS by FINSEQ_1:def 11;

        reconsider IT = ( <*ss*> ^ tail) as Element of ((SS * ) \ { {} }) by FOMODEL0: 5;

        take IT;

        thus thesis;

      end;

    end

    registration

      let S;

      let phi be 0wff string of S;

      cluster ((S -firstChar ) . phi) -> relational;

      coherence

      proof

        set SS = ( AllSymbolsOf S), A = ( AllTermsOf S), C = (S -multiCat ), F = (S -firstChar );

        consider s be relational Element of S, V be |.( ar s).| -element Element of (A * ) such that

         A1: phi = ( <*s*> ^ (C . V)) by Def35;

        reconsider ss = s as Element of SS;

        reconsider head = <*ss*> as FinSequence of SS;

        reconsider tail = (C . V) as FinSequence of SS by FINSEQ_1:def 11;

        (F . phi) = ((head ^ tail) . 1) by A1, FOMODEL0: 6

        .= s by FINSEQ_1: 41;

        hence thesis;

      end;

    end

    definition

      let S;

      :: FOMODEL1:def36

      func AtomicFormulasOf S -> set equals { phi where phi be string of S : phi is 0wff };

      coherence ;

    end

    definition

      let S;

      :: original: AtomicFormulasOf

      redefine

      func AtomicFormulasOf S -> Subset of ((( AllSymbolsOf S) * ) \ { {} }) ;

      coherence

      proof

        set SS = ( AllSymbolsOf S), AF = ( AtomicFormulasOf S);

        defpred P[ Element of ((SS * ) \ { {} })] means $1 is 0wff;

        { phi where phi be Element of ((SS * ) \ { {} }) : P[phi] } is Subset of ((SS * ) \ { {} }) from DOMAIN_1:sch 7;

        hence thesis;

      end;

    end

    registration

      let S;

      cluster ( AtomicFormulasOf S) -> non empty;

      coherence

      proof

        set AF = ( AtomicFormulasOf S), phi = the 0wff string of S;

        phi in AF;

        hence thesis;

      end;

    end

    registration

      let S;

      cluster -> 0wff for Element of ( AtomicFormulasOf S);

      coherence

      proof

        set AF = ( AtomicFormulasOf S);

        let phi be Element of AF;

        phi in AF;

        then

        consider x be string of S such that

         A1: phi = x & x is 0wff;

        thus thesis by A1;

      end;

    end

    

     Lm10: ( AllTermsOf S) is S -prefix

    proof

      set SS = ( AllSymbolsOf S), f = (SS -concatenation ), F = (SS -multiCat ), TT = ( AllTermsOf S), T = (S -termsOfMaxDepth );

      now

        let t1,t2,w1,w2 be set;

        assume

         A1: t1 in (TT /\ (SS * )) & t2 in (TT /\ (SS * )) & w1 in (SS * ) & w2 in (SS * ) & (f . (t1,w1)) = (f . (t2,w2));

        consider mm be Element of NAT such that

         A2: t1 in (T . mm) by Lm6, A1;

        consider nn be Element of NAT such that

         A3: t2 in (T . nn) by Lm6, A1;

        set p = (mm + nn);

        

         A4: (T . p) is f -unambiguous by FOMODEL0:def 3;

        (T . mm) c= (T . p) & (T . nn) c= (T . p) by Lm5;

        then t1 in ((T . p) /\ (SS * )) & t2 in ((T . p) /\ (SS * )) & w1 in (SS * ) & w2 in (SS * ) & (f . (t1,w1)) = (f . (t2,w2)) by A1, XBOOLE_0:def 4, A2, A3;

        hence t1 = t2 & w1 = w2 by A4;

      end;

      then TT is SS -prefix by FOMODEL0:def 10;

      hence thesis;

    end;

    registration

      let S;

      cluster ( AllTermsOf S) -> S -prefix;

      coherence by Lm10;

    end

    definition

      let S;

      let t be termal string of S;

      :: FOMODEL1:def37

      func SubTerms (t) -> Element of (( AllTermsOf S) * ) means

      : Def37: it is |.( ar ((S -firstChar ) . t)).| -element & t = ( <*((S -firstChar ) . t)*> ^ ((S -multiCat ) . it ));

      existence

      proof

        set SS = ( AllSymbolsOf S), T = (S -termsOfMaxDepth ), TT = ( AllTermsOf S), s = ((S -firstChar ) . t), n = |.( ar s).|;

        t in TT by Def32;

        then

        consider mmm be Element of NAT such that

         A1: t in (T . mmm) by Lm6;

        reconsider tt = t as mmm -termal string of S by A1, Def33;

        reconsider tttt = t as non empty FinSequence of SS by FOMODEL0: 5;

        per cases ;

          suppose mmm = 0 ;

          then

          reconsider ttt = tt as 0 -termal string of S;

          reconsider e = {} as Element of (( AllTermsOf S) * ) by FINSEQ_1: 49;

          take e;

           |.( ar ((S -firstChar ) . ttt)).| is zero;

          hence e is n -element;

          ( len ttt) = 1 by CARD_1:def 7;

          

          then tttt = <*(tttt . 1)*> by FINSEQ_5: 14

          .= ( <*((SS -firstChar ) . t)*> ^ {} ) by FOMODEL0: 6

          .= ( <*((SS -firstChar ) . t)*> ^ ((S -multiCat ) . e));

          hence thesis;

        end;

          suppose mmm <> 0 ;

          then

          consider m be Nat such that

           A3: mmm = (m + 1) by NAT_1: 6;

          reconsider mm = m as Element of NAT by ORDINAL1:def 12;

          reconsider ttt = tt as (mm + 1) -termal string of S by A3;

          consider ST be Element of ((T . mm) * ) such that

           A4: ST is n -element & ttt = ( <*((S -firstChar ) . ttt)*> ^ ((S -multiCat ) . ST)) by Th3;

          reconsider TM = (T . mm) as Subset of TT by Th2;

          ST in (TM * ) & (TM * ) c= (TT * );

          then

          reconsider STT = ST as Element of (TT * );

          take STT;

          thus thesis by A4;

        end;

      end;

      uniqueness

      proof

        set SS = ( AllSymbolsOf S), T = (S -termsOfMaxDepth ), TT = ( AllTermsOf S), s = ((S -firstChar ) . t), n = |.( ar s).|;

        

         A5: (SS -multiCat ) is (n -tuples_on TT) -one-to-one by FOMODEL0: 8;

        

         A6: ( dom (SS -multiCat )) = ((SS * ) * ) by FUNCT_2:def 1;

        let IT1,IT2 be Element of (TT * );

        reconsider IT11 = IT1, IT22 = IT2 as FinSequence of TT by FINSEQ_1:def 11;

        assume

         A7: IT1 is n -element & t = ( <*s*> ^ ((S -multiCat ) . IT1));

        then ( len IT11) = n by CARD_1:def 7;

        then

        reconsider IT111 = IT11 as Element of (n -tuples_on TT) by FINSEQ_2: 133;

        assume

         A8: IT2 is n -element & t = ( <*s*> ^ ((S -multiCat ) . IT2));

        then ( len IT22) = n by CARD_1:def 7;

        then

        reconsider IT222 = IT22 as Element of (n -tuples_on TT) by FINSEQ_2: 133;

        

         A9: ((SS -multiCat ) . IT111) = ((SS -multiCat ) . IT222) by FINSEQ_1: 33, A7, A8;

        IT111 in ((n -tuples_on TT) /\ ( dom (SS -multiCat ))) & IT222 in ((n -tuples_on TT) /\ ( dom (SS -multiCat ))) by XBOOLE_0:def 4, A6;

        hence thesis by A9, A5;

      end;

    end

    registration

      let S;

      let t be termal string of S;

      cluster ( SubTerms t) -> |.( ar t).| -element;

      coherence by Def37;

    end

    registration

      let S;

      let t0 be 0 -termal string of S;

      cluster ( SubTerms t0) -> empty;

      coherence

      proof

         |.( ar t0).| = 0 ;

        hence thesis;

      end;

    end

    registration

      let mm, S;

      let t be (mm + 1) -termal string of S;

      cluster ( SubTerms t) -> ((S -termsOfMaxDepth ) . mm) -valued;

      coherence

      proof

        set T = (S -termsOfMaxDepth ), F = (S -firstChar ), C = (S -multiCat ), A = ( AllTermsOf S), SS = ( AllSymbolsOf S);

        consider TT be Element of ((T . mm) * ) such that

         A1: TT is |.( ar t).| -element & t = ( <*(F . t)*> ^ (C . TT)) by Th3;

        reconsider X = (T . mm) as Subset of A by Th2;

        reconsider Y = (X * ) as non empty Subset of (A * );

        reconsider TTTT = TT as Element of Y;

        reconsider TTT = TTTT as Element of (A * );

        TTT = ( SubTerms t) by Def37, A1;

        hence thesis;

      end;

    end

    definition

      let S;

      let phi be 0wff string of S;

      :: FOMODEL1:def38

      func SubTerms (phi) -> |.( ar ((S -firstChar ) . phi)).| -element Element of (( AllTermsOf S) * ) means

      : Def38: phi = ( <*((S -firstChar ) . phi)*> ^ ((S -multiCat ) . it ));

      existence

      proof

        set SS = ( AllSymbolsOf S), A = ( AllTermsOf S), C = (S -multiCat ), F = (S -firstChar );

        consider s be relational Element of S, V be |.( ar s).| -element Element of (A * ) such that

         A1: phi = ( <*s*> ^ (C . V)) by Def35;

        reconsider ss = s as Element of SS;

        reconsider head = <*ss*> as FinSequence of SS;

        reconsider tail = (C . V) as FinSequence of SS by FINSEQ_1:def 11;

        

         A2: (F . phi) = ((head ^ tail) . 1) by A1, FOMODEL0: 6

        .= s by FINSEQ_1: 41;

        reconsider VV = V as |.( ar (F . phi)).| -element Element of (A * ) by A2;

        take VV;

        thus thesis by A2, A1;

      end;

      uniqueness

      proof

        set SS = ( AllSymbolsOf S), A = ( AllTermsOf S), C = (S -multiCat ), F = (S -firstChar );

        set n = |.( ar ((S -firstChar ) . phi)).|;

        

         A3: ( dom C) = ((SS * ) * ) & (A * ) c= ((SS * ) * ) by FUNCT_2:def 1;

        reconsider s = (F . phi) as Element of SS;

        reconsider head = <*s*> as FinSequence of SS;

        let IT1,IT2 be n -element Element of (A * );

        reconsider I1 = IT1, I2 = IT2 as FinSequence of A by FINSEQ_1:def 11;

        ( len IT1) = n & ( len IT2) = n by CARD_1:def 7;

        then

        reconsider I11 = I1, I22 = I2 as Element of (n -tuples_on A) by FINSEQ_2: 133;

        reconsider tail1 = (C . IT1), tail2 = (C . IT2) as FinSequence of SS by FINSEQ_1:def 11;

        assume

         A4: phi = ( <*(F . phi)*> ^ (C . IT1)) & phi = ( <*(F . phi)*> ^ (C . IT2));

        IT1 in ( dom C) & I11 in (n -tuples_on A) & IT2 in ( dom C) & I22 in (n -tuples_on A) by A3;

        then

         A5: IT1 in ((n -tuples_on A) /\ ( dom C)) & IT2 in ((n -tuples_on A) /\ ( dom C)) & (C . IT1) = (C . IT2) by A4, FINSEQ_1: 33, XBOOLE_0:def 4;

        C is (n -tuples_on A) -one-to-one by FOMODEL0: 8;

        hence thesis by A5;

      end;

    end

    registration

      let S;

      let phi be 0wff string of S;

      cluster ( SubTerms phi) -> |.( ar ((S -firstChar ) . phi)).| -element;

      coherence ;

    end

    definition

      let S;

      :: original: AllTermsOf

      redefine

      func AllTermsOf S -> Element of ( bool ((( AllSymbolsOf S) * ) \ { {} })) ;

      coherence

      proof

        set SS = ( AllSymbolsOf S), A = ( AllTermsOf S);

        now

          let x be object;

          assume

           A1: x in A;

          then

          reconsider t = x as Element of A;

           not x in { {} } & x in (SS * ) by A1;

          hence x in ((SS * ) \ { {} }) by XBOOLE_0:def 5;

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    registration

      let S;

      cluster -> termal for Element of ( AllTermsOf S);

      coherence ;

    end

    definition

      let S;

      :: FOMODEL1:def39

      func S -subTerms -> Function of ( AllTermsOf S), (( AllTermsOf S) * ) means for t be Element of ( AllTermsOf S) holds (it . t) = ( SubTerms t);

      existence

      proof

        set SS = ( AllSymbolsOf S), A = ( AllTermsOf S);

        deffunc F( Element of A) = ( SubTerms $1);

        consider f be Function of A, (A * ) such that

         A1: for t be Element of A holds (f . t) = F(t) from FUNCT_2:sch 4;

        take f;

        thus thesis by A1;

      end;

      uniqueness

      proof

        set A = ( AllTermsOf S);

        let IT1,IT2 be Function of A, (A * );

        assume

         A2: for t be Element of A holds (IT1 . t) = ( SubTerms t);

        assume

         A3: for t be Element of A holds (IT2 . t) = ( SubTerms t);

        now

          let t be Element of A;

          

          thus (IT1 . t) = ( SubTerms t) by A2

          .= (IT2 . t) by A3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    theorem :: FOMODEL1:4

    ((S -termsOfMaxDepth ) . m) c= ((S -termsOfMaxDepth ) . (m + n)) by Lm5;

    theorem :: FOMODEL1:5

    x in ( AllTermsOf S) implies ex nn st x in ((S -termsOfMaxDepth ) . nn) by Lm6;

    theorem :: FOMODEL1:6

    ( AllTermsOf S) c= ((( AllSymbolsOf S) * ) \ { {} });

    theorem :: FOMODEL1:7

    ( AllTermsOf S) is S -prefix;

    theorem :: FOMODEL1:8

    x in ( AllTermsOf S) implies x is string of S;

    theorem :: FOMODEL1:9

    (( AtomicFormulaSymbolsOf S) \ ( OwnSymbolsOf S)) = {( TheEqSymbOf S)}

    proof

      set o = the OneF of S, z = the ZeroF of S, f = the adicity of S, R = ( RelSymbolsOf S), O = ( OwnSymbolsOf S), SS = ( AllSymbolsOf S), e = ( TheEqSymbOf S), n = ( TheNorSymbOf S), A = ( AtomicFormulaSymbolsOf S), D = (the carrier of S \ {o});

      

       A1: e in A by Lm3;

      (A \ O) = (A \ (A \ {z})) by XBOOLE_1: 41

      .= ((A \ A) \/ (A /\ {z})) by XBOOLE_1: 52

      .= {z} by ZFMISC_1: 46, A1;

      hence thesis;

    end;

    theorem :: FOMODEL1:10

    (( TermSymbolsOf S) \ ( LettersOf S)) = ( OpSymbolsOf S) by FUNCT_1: 69;

    theorem :: FOMODEL1:11

    

     Th11: (( AtomicFormulaSymbolsOf S) \ ( RelSymbolsOf S)) = ( TermSymbolsOf S)

    proof

      set R = ( RelSymbolsOf S), SSS = ( AtomicFormulaSymbolsOf S), f = the adicity of S;

      (f " INT ) = SSS by FUNCT_2: 40;

      

      hence (SSS \ R) = (f " ( INT \ ( INT \ NAT ))) by FUNCT_1: 69

      .= (f " (( INT \ INT ) \/ ( INT /\ NAT ))) by XBOOLE_1: 52

      .= ( TermSymbolsOf S) by XBOOLE_1: 7, XBOOLE_1: 28;

    end;

    registration

      let S;

      cluster non relational -> termal for ofAtomicFormula Element of S;

      coherence

      proof

        set R = ( RelSymbolsOf S), SSS = ( AtomicFormulaSymbolsOf S), T = ( TermSymbolsOf S);

        let s be ofAtomicFormula Element of S;

        assume s is non relational;

        then s in SSS & not s in R by Def20;

        then s in (SSS \ R) by XBOOLE_0:def 5;

        then s in T by Th11;

        hence thesis;

      end;

    end

    definition

      let S;

      :: original: OwnSymbolsOf

      redefine

      func OwnSymbolsOf S -> Subset of ( AllSymbolsOf S) ;

      coherence ;

    end

    registration

      let S;

      cluster non literal -> operational for termal Element of S;

      coherence

      proof

        set L = ( LettersOf S), P = ( OpSymbolsOf S), T = ( TermSymbolsOf S), f = the adicity of S;

        let s be termal Element of S;

        

         A1: s in T by Def18;

        assume not s is literal;

        then not s in L;

        then s in (T \ L) & (T \ L) = P by FUNCT_1: 69, A1, XBOOLE_0:def 5;

        hence thesis;

      end;

    end

    theorem :: FOMODEL1:12

    

     Th12: x is string of S iff x is non empty Element of (( AllSymbolsOf S) * )

    proof

      set SS = ( AllSymbolsOf S);

      x is string of S iff (x in (SS * ) & not x in { {} }) by XBOOLE_0:def 5;

      hence thesis;

    end;

    theorem :: FOMODEL1:13

    x is string of S iff x is non empty FinSequence of ( AllSymbolsOf S) by Th12;

    theorem :: FOMODEL1:14

    (S -termsOfMaxDepth ) is sequence of ( bool (( AllSymbolsOf S) * ));

    registration

      let S;

      cluster -> literal for Element of ( LettersOf S);

      coherence ;

    end

    registration

      let S;

      cluster ( TheNorSymbOf S) -> non low-compounding;

      coherence

      proof

        set N = ( TheNorSymbOf S), f = the adicity of S, Low = ( LowerCompoundersOf S), SS = ( AllSymbolsOf S);

        

         A1: ( dom f) = (SS \ {N}) & N in {N} by FUNCT_2:def 1, TARSKI:def 1;

         not N in Low by XBOOLE_0:def 5, A1;

        hence thesis;

      end;

    end

    registration

      let S;

      cluster ( TheNorSymbOf S) -> non own;

      coherence

      proof

        set N = ( TheNorSymbOf S), f = the adicity of S, O = ( OwnSymbolsOf S), SS = ( AllSymbolsOf S);

        N in {the ZeroF of S, N} by TARSKI:def 2;

        then not N in O by XBOOLE_0:def 5;

        hence thesis;

      end;

    end

    theorem :: FOMODEL1:15

    s <> ( TheNorSymbOf S) & s <> ( TheEqSymbOf S) implies s in ( OwnSymbolsOf S)

    proof

      set O = ( OwnSymbolsOf S), R = ( RelSymbolsOf S), E = ( TheEqSymbOf S), X = (R \ O), N = ( TheNorSymbOf S), SS = ( AllSymbolsOf S);

      assume s <> N & s <> E;

      then not s in {N} & not s in {E} by TARSKI:def 1;

      then not s in ( {N} \/ {E}) by XBOOLE_0:def 3;

      hence thesis by XBOOLE_0:def 5;

    end;

    reserve l,l1,l2 for literal Element of S,

a for ofAtomicFormula Element of S,

r for relational Element of S,

w,w1,w2 for string of S,

t,t1,t2 for termal string of S,

tt,tt1,tt2 for Element of ( AllTermsOf S);

    definition

      let S, t;

      :: FOMODEL1:def40

      func Depth t -> Nat means

      : Def40: t is it -termal & for n st t is n -termal holds it <= n;

      existence

      proof

        defpred P[ Nat] means t is $1 -termal;

        set TT = ( AllTermsOf S), T = (S -termsOfMaxDepth );

        reconsider TF = T as Function;

        t in TT by Def32;

        then

        consider mm such that

         A1: t in (TF . mm) by Lm6;

        t is mm -termal by A1;

        then

         A2: ex n be Nat st P[n];

        consider IT be Nat such that

         A3: P[IT] & for n st P[n] holds IT <= n from NAT_1:sch 5( A2);

        take IT;

        thus thesis by A3;

      end;

      uniqueness

      proof

        let IT1,IT2 be Nat;

        set phi = t;

        assume

         A4: phi is IT1 -termal & for n st phi is n -termal holds IT1 <= n;

        assume

         A5: phi is IT2 -termal & for n st phi is n -termal holds IT2 <= n;

        

         A6: IT2 <= IT1 by A5, A4;

        IT1 <= IT2 by A4, A5;

        hence thesis by A6, XXREAL_0: 1;

      end;

    end

    registration

      let S;

      let m0 be zero number;

      let t be m0 -termal string of S;

      cluster ( Depth t) -> zero;

      coherence by Def40;

    end

    registration

      let S;

      let s be low-compounding Element of S;

      cluster ( ar s) -> non zero;

      coherence

      proof

        set f = the adicity of S, SS = ( AllSymbolsOf S), N = ( TheNorSymbOf S);

        s in ( LowerCompoundersOf S) by Def15;

        then s in ( dom f) & (f . s) in ( INT \ { 0 }) by FUNCT_1:def 7;

        then not (f . s) in { 0 };

        hence thesis by TARSKI:def 1;

      end;

    end

    registration

      let S;

      let s be termal Element of S;

      cluster ( ar s) -> non negative;

      coherence

      proof

        set f = the adicity of S, T = ( TermSymbolsOf S);

        s in T by Def18;

        then

        reconsider nn = ( ar s) as Element of NAT by FUNCT_1:def 7;

        nn is non negative;

        hence thesis;

      end;

    end

    registration

      let S;

      let s be relational Element of S;

      cluster ( ar s) -> negative ext-real;

      coherence

      proof

        set f = the adicity of S, R = ( RelSymbolsOf S);

        s in R by Def17;

        then s in ( dom f) & (f . s) in ( INT \ NAT ) by FUNCT_1:def 7;

        then

         A1: ( ar s) in INT & not ( ar s) in NAT by XBOOLE_0:def 5;

        reconsider IT = ( ar s) as Element of INT ;

        thus thesis by A1, INT_1: 3;

      end;

    end

    theorem :: FOMODEL1:16

    

     Th16: t is non 0 -termal implies ((S -firstChar ) . t) is operational & ( SubTerms t) <> {}

    proof

      set T = (S -termsOfMaxDepth ), m = ( Depth t), ST = ( SubTerms t), TT = ( AllTermsOf S);

      assume t is non 0 -termal;

      then m <> 0 by Def40;

      then

      consider n such that

       A1: m = (n + 1) by NAT_1: 6;

      set F = (S -firstChar ), C = (S -multiCat ), Fam = { ( Compound (s,(T . n))) where s be ofAtomicFormula Element of S : s is operational };

      n < m by A1, NAT_1: 16;

      then not t is n -termal & t is m -termal by Def40;

      then not t in (T . n) & t in (T . (n + 1)) by A1;

      then (t in (( union Fam) \/ (T . n))) & not t in (T . n) by Def30;

      then t in ( union Fam) by XBOOLE_0:def 3;

      then

      consider x be set such that

       A2: t in x & x in Fam by TARSKI:def 4;

      consider s be ofAtomicFormula Element of S such that

       A3: x = ( Compound (s,(T . n))) & s is operational by A2;

      set k = |.( ar s).|;

      consider StringTuple be Element of ((( AllSymbolsOf S) * ) * ) such that

       A4: t = ( <*s*> ^ (C . StringTuple)) & ( rng StringTuple) c= (T . n) & StringTuple is |.( ar s).| -element by A2, A3;

      

       A5: (F . t) = (( <*s*> ^ (C . StringTuple)) . 1) by FOMODEL0: 6, A4

      .= ( <*s*> . 1) by FOMODEL0: 28

      .= s by FINSEQ_1: 40;

      hence (F . t) is operational by A3;

      reconsider k1 = k as non zero Nat by A3;

      reconsider STT = ST as (k1 + 0 ) -element Element of (TT * ) by A5;

      STT <> {} ;

      hence thesis;

    end;

    registration

      let S;

      cluster (S -multiCat ) -> FinSequence-yielding;

      coherence ;

    end

    registration

      let S;

      let W be non empty((( AllSymbolsOf S) * ) \ { {} }) -valued FinSequence;

      cluster ((S -multiCat ) . W) -> non empty;

      coherence

      proof

        set C = (S -multiCat ), SS = ( AllSymbolsOf S), g = (SS -concatenation ), G = ( MultPlace g);

        consider m such that

         A1: (m + 1) = ( len W) by NAT_1: 6;

        reconsider WW = W as ((m + 1) + 0 ) -element FinSequence by A1, CARD_1:def 7;

        

         A2: ( {(WW . (m + 1))} \ ((SS * ) \ { {} })) = {} ;

        then

         A3: (WW . (m + 1)) in ((SS * ) \ { {} }) by ZFMISC_1: 60;

        reconsider last = (WW . (m + 1)) as string of S by A2, ZFMISC_1: 60;

        reconsider lastt = (WW . (m + 1)) as Element of (SS * ) by A3;

        set VV = (WW | ( Seg m));

        reconsider VVV = VV as (SS * ) -valued FinSequence;

        ((VV ^ <*(WW . (m + 1))*>) \+\ WW) = {} ;

        then

         A4: (G . W) = (G . (VVV ^ <*lastt*>)) by FOMODEL0: 29;

        per cases ;

          suppose VVV is empty;

          

          then (G . W) = (G . <*lastt*>) by A4, FINSEQ_1: 34

          .= last by FOMODEL0: 31;

          hence thesis by FOMODEL0: 32;

        end;

          suppose

           A5: VVV is non empty;

          then

          reconsider VVVV = VVV as Element of (((SS * ) * ) \ { {} }) by FOMODEL0: 30;

          (G . W) = (g . ((G . VVV),lastt)) by A5, A4, FOMODEL0: 31

          .= ((G . VVVV) ^ last) by FOMODEL0: 4;

          hence thesis by FOMODEL0: 32;

        end;

      end;

    end

    registration

      let S, l;

      cluster <*l*> -> 0 -termal;

      coherence

      proof

        set w = <*l*>, L = ( LettersOf S), AT = ( AtomicTermsOf S), T = (S -termsOfMaxDepth );

        reconsider ll = l as Element of L by Def14;

        w = <*ll*>;

        then w in AT by FINSEQ_2: 98;

        then w in (T . 0 ) by Def30;

        hence thesis;

      end;

    end

    registration

      let S, m, n;

      cluster (m + ( 0 * n)) -termal -> (m + n) -termal for string of S;

      coherence

      proof

        set T = (S -termsOfMaxDepth );

        let t be string of S;

        assume t is (m + ( 0 * n)) -termal;

        then t in (T . m) & (T . m) c= (T . (m + n)) by Lm5;

        hence thesis;

      end;

    end

    registration

      let S;

      cluster non low-compounding -> literal for own Element of S;

      coherence

      proof

        set L = ( LettersOf S), P = ( OpSymbolsOf S), O = ( OwnSymbolsOf S), T = ( TermSymbolsOf S);

        

         A1: (T \ L) = P by FUNCT_1: 69;

        let s be own Element of S;

        reconsider ss = s as ofAtomicFormula Element of S;

        assume

         A2: s is non low-compounding;

        then not ss is relational;

        then

        reconsider sss = ss as termal ofAtomicFormula Element of S;

        assume not s is literal;

        then sss in T & not s in L by Def18;

        then s in (T \ L) by XBOOLE_0:def 5;

        then s is operational & not s is operational by A2, A1;

        hence contradiction;

      end;

    end

    registration

      let S, t;

      cluster ( SubTerms t) -> (( rng t) * ) -valued;

      coherence

      proof

        set SS = ( AllSymbolsOf S), C = (S -multiCat ), F = (S -firstChar ), ST = ( SubTerms t), T = (S -termsOfMaxDepth ), TT = ( AllTermsOf S);

        reconsider TTT = TT as Subset of (SS * ) by XBOOLE_1: 1;

        t = ( <*(F . t)*> ^ (C . ST)) by Def37;

        then ( rng (C . ST)) c= ( rng t) by FINSEQ_1: 30;

        then (C . ST) is ( rng t) -valued by RELAT_1:def 19;

        hence thesis by FOMODEL0: 42;

      end;

    end

    registration

      let S;

      let phi0 be 0wff string of S;

      cluster ( SubTerms phi0) -> (( rng phi0) * ) -valued;

      coherence

      proof

        set SS = ( AllSymbolsOf S), C = (S -multiCat ), F = (S -firstChar ), ST = ( SubTerms phi0), T = (S -termsOfMaxDepth ), TT = ( AllTermsOf S);

        reconsider TTT = TT as non empty Subset of (SS * ) by XBOOLE_1: 1;

        phi0 = ( <*(F . phi0)*> ^ (C . ST)) by Def38;

        then ( rng (C . ST)) c= ( rng phi0) by FINSEQ_1: 30;

        then (C . ST) is ( rng phi0) -valued by RELAT_1:def 19;

        hence thesis by FOMODEL0: 42;

      end;

    end

    definition

      let S;

      :: original: -termsOfMaxDepth

      redefine

      func S -termsOfMaxDepth -> sequence of ( bool ((( AllSymbolsOf S) * ) \ { {} })) ;

      coherence

      proof

        set T = (S -termsOfMaxDepth ), SS = ( AllSymbolsOf S);

        now

          let y be object;

          assume y in ( rng T);

          then

          consider x be object such that

           A1: x in ( dom T) & (T . x) = y by FUNCT_1:def 3;

          reconsider mm = x as Element of NAT by A1;

          (T . mm) misses { {} }

          proof

            assume (T . mm) meets { {} };

            then ((T . mm) /\ { {} }) <> {} ;

            then

            consider z be object such that

             A2: z in ((T . mm) /\ { {} }) by XBOOLE_0:def 1;

            thus contradiction by A2;

          end;

          then (T . mm) c= ((SS * ) \ { {} }) by XBOOLE_1: 86;

          hence y in ( bool ((SS * ) \ { {} })) by A1;

        end;

        then ( rng T) c= ( bool ((SS * ) \ { {} })) by TARSKI:def 3;

        hence thesis by FUNCT_2: 6;

      end;

    end

    registration

      let S, mm;

      cluster ((S -termsOfMaxDepth ) . mm) -> with_non-empty_elements;

      coherence ;

    end

    

     Lm11: ((S -termsOfMaxDepth ) . m) c= (( TermSymbolsOf S) * )

    proof

      set TS = ( TermSymbolsOf S), F = (S -firstChar ), C = (S -multiCat ), P = ( OpSymbolsOf S), T = (S -termsOfMaxDepth ), SS = ( AllSymbolsOf S), CC = (TS -multiCat );

      defpred P[ Nat] means (T . $1) c= (TS * );

      

       A1: P[ 0 ]

      proof

        now

          let x be object;

          assume x in (T . 0 );

          then

          reconsider t = x as 0 -termal string of S by Def33;

          reconsider s = (F . t) as termal Element of S;

          set sub = ( SubTerms t);

          reconsider ss = s as Element of TS by Def18;

          t = ( <*s*> ^ (C . sub)) by Def37

          .= ( <*s*> ^ {} )

          .= <*ss*>;

          then t is FinSequence of TS;

          hence x in (TS * );

        end;

        hence thesis by TARSKI:def 3;

      end;

      

       A2: for n st P[n] holds P[(n + 1)]

      proof

        let n;

        reconsider nn = n, NN = (n + 1) as Element of NAT by ORDINAL1:def 12;

        assume P[n];

        then

        reconsider Tn = (T . nn) as non empty Subset of (TS * );

        now

          let x be object;

          assume x in (T . (n + 1));

          then x in (T . NN);

          then

          reconsider t = x as (n + 1) -termal string of S by Def33;

          set s = (F . t), m = |.( ar s).|;

          reconsider tt = t as (nn + 1) -termal string of S;

          per cases ;

            suppose

             A3: not t is 0 -termal;

            then

             A4: s is operational by Th16;

            s in P & P c= TS by Def16, Th1, Th16, A3;

            then

            reconsider ss = s as Element of TS;

            reconsider m1 = m as non zero Nat by A4;

            ( SubTerms tt) is (T . nn) -valued;

            then

            reconsider sub = ( SubTerms t) as (m1 + 0 ) -element FinSequence of Tn by FOMODEL0: 26;

            sub in (Tn * ) & (Tn * ) c= ((TS * ) * );

            then

            reconsider subb = sub as (m1 + 0 ) -element Element of ((TS * ) * );

            sub is Tn -valued & Tn c= (TS * ) & TS c= SS by XBOOLE_1: 1;

            

            then ( <*ss*> ^ (CC . subb)) = ( <*(F . t)*> ^ (C . ( SubTerms t))) by FOMODEL0: 53

            .= t by Def37;

            then

            reconsider tt = t as FinSequence of TS by FOMODEL0: 26;

            tt in (TS * );

            hence x in (TS * );

          end;

            suppose t is 0 -termal;

            then x in (T . 0 );

            hence x in (TS * ) by A1;

          end;

        end;

        hence thesis by TARSKI:def 3;

      end;

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

      hence thesis;

    end;

    registration

      let S, m;

      let t be termal string of S;

      cluster (t null m) -> (( Depth t) + m) -termal;

      coherence

      proof

        set d = ( Depth t);

        t is (d + ( 0 * m)) -termal by Def40;

        hence thesis;

      end;

    end

    registration

      let S;

      cluster termal -> ( TermSymbolsOf S) -valued for string of S;

      coherence

      proof

        set T = (S -termsOfMaxDepth ), TS = ( TermSymbolsOf S);

        let w;

        assume w is termal;

        then

        reconsider tt = w as termal string of S;

        set d = ( Depth tt);

        reconsider t = (tt null 0 ) as (d + 0 ) -termal string of S;

        t in (T . d) & (T . d) c= (TS * ) by Lm11, Def33;

        hence thesis;

      end;

    end

    registration

      let S;

      cluster (( AllTermsOf S) \ (( TermSymbolsOf S) * )) -> empty;

      coherence

      proof

        set TT = ( AllTermsOf S), TS = ( TermSymbolsOf S);

        now

          let x be object;

          assume x in TT;

          then

          reconsider t = x as termal string of S;

          t is FinSequence of TS by FOMODEL0: 26;

          hence x in (TS * );

        end;

        then TT c= (TS * ) by TARSKI:def 3;

        hence thesis;

      end;

    end

    registration

      let S;

      let phi0 be 0wff string of S;

      cluster ( SubTerms phi0) -> (( TermSymbolsOf S) * ) -valued;

      coherence

      proof

        set sub = ( SubTerms phi0), TS = ( TermSymbolsOf S), TT = ( AllTermsOf S);

        (TT \ (TS * )) = {} ;

        then

        reconsider TTT = TT as non empty Subset of (TS * ) by XBOOLE_1: 37;

        sub is TTT -valued;

        hence thesis;

      end;

    end

    registration

      let S;

      cluster 0wff -> ( AtomicFormulaSymbolsOf S) -valued for string of S;

      coherence

      proof

        set TS = ( TermSymbolsOf S), AS = ( AtomicFormulaSymbolsOf S), F = (S -firstChar ), C = (S -multiCat ), TT = ( AllTermsOf S), CC = (TS -multiCat ), SS = ( AllSymbolsOf S);

        let w;

        assume w is 0wff;

        then

        reconsider phi = w as 0wff string of S;

        reconsider r = (F . phi) as relational Element of S;

        set m = |.( ar r).|;

        reconsider rr = r as Element of AS by Def20;

        reconsider sub = ( SubTerms phi) as (m + 0 ) -element Element of (TT * );

        (TT \ (TS * )) = {} ;

        then TS c= SS & TT c= (TS * ) & sub is TT -valued by XBOOLE_1: 1, XBOOLE_1: 37;

        

        then ( <*rr*> ^ (CC . sub)) = ( <*r*> ^ (C . sub)) by FOMODEL0: 53

        .= phi by Def38;

        hence thesis;

      end;

    end

    registration

      let S;

      cluster ( OwnSymbolsOf S) -> non empty;

      coherence ;

    end

    reserve phi0 for 0wff string of S;

    theorem :: FOMODEL1:17

    ((S -firstChar ) . phi0) <> ( TheEqSymbOf S) implies phi0 is ( OwnSymbolsOf S) -valued

    proof

      set O = ( OwnSymbolsOf S), F = (S -firstChar ), r = (F . phi0), C = (S -multiCat ), sub = ( SubTerms phi0), E = ( TheEqSymbOf S), R = ( RelSymbolsOf S);

      reconsider TS = ( TermSymbolsOf S) as non empty Subset of O by Th1;

      assume r <> E;

      then not r in {E} by TARSKI:def 1;

      then not r in (R \ O) by Th1;

      then r in O or not r in R by XBOOLE_0:def 5;

      then

      reconsider rr = r as Element of O by Def17;

      (C . sub) is TS -valued by FOMODEL0: 54;

      then

      reconsider tail = (C . sub) as O -valued FinSequence;

      phi0 = ( <*rr*> ^ tail) by Def38;

      hence thesis;

    end;

    registration

      cluster strict non empty for Language-like;

      existence

      proof

        set a = the Function of ( NAT \ { 0 }), INT ;

        take IT = Language-like (# NAT , 0 , 0 , a #);

        thus thesis;

      end;

    end

    definition

      let S1,S2 be Language-like;

      :: FOMODEL1:def41

      attr S2 is S1 -extending means

      : Def41: the adicity of S1 c= the adicity of S2 & ( TheEqSymbOf S1) = ( TheEqSymbOf S2) & ( TheNorSymbOf S1) = ( TheNorSymbOf S2);

    end

    registration

      let S;

      cluster (S null ) -> S -extending;

      coherence ;

    end

    registration

      let S;

      cluster S -extending for Language;

      existence

      proof

        reconsider SS = (S null ) as Language;

        take SS;

        thus thesis;

      end;

    end

    registration

      let S1;

      let S2 be S1 -extending Language;

      cluster (( OwnSymbolsOf S1) \ ( OwnSymbolsOf S2)) -> empty;

      coherence

      proof

        set O1 = ( OwnSymbolsOf S1), O2 = ( OwnSymbolsOf S2), f1 = the adicity of S1, f2 = the adicity of S2, A1 = ( AtomicFormulaSymbolsOf S1), SS1 = ( AllSymbolsOf S1), SS2 = ( AllSymbolsOf S2), z1 = the ZeroF of S1, o1 = the OneF of S1, z2 = the ZeroF of S2, o2 = the OneF of S2, E1 = ( TheEqSymbOf S1), E2 = ( TheEqSymbOf S2), N1 = ( TheNorSymbOf S1), N2 = ( TheNorSymbOf S2);

        

         A1: ( dom f1) = (SS1 \ {o1}) & ( dom f2) = (SS2 \ {o2}) by FUNCT_2:def 1;

        f1 c= f2 by Def41;

        then ((SS1 \ {N1}) \ {E1}) c= ((SS2 \ {N2}) \ {E1}) by XBOOLE_1: 33, GRFUNC_1: 2, A1;

        then (SS1 \ {N1, E1}) c= ((SS2 \ {N2}) \ {E1}) by XBOOLE_1: 41;

        then (SS1 \ {N1, E1}) c= (SS2 \ ( {N2} \/ {E1})) by XBOOLE_1: 41;

        then (SS1 \ {N1, E1}) c= (SS2 \ ( {N2} \/ {E2})) by Def41;

        hence thesis;

      end;

    end

    definition

      let f be INT -valued Function;

      let L be non empty Language-like;

      set C = the carrier of L, z = the ZeroF of L, o = the OneF of L, a = the adicity of L, X = ( dom f), g = (f | (X \ {o})), a1 = (g +* a), C1 = (C \/ X);

      :: FOMODEL1:def42

      func L extendWith f -> strict non empty Language-like means

      : Def42: the adicity of it = ((f | (( dom f) \ {the OneF of L})) +* the adicity of L) & the ZeroF of it = the ZeroF of L & the OneF of it = the OneF of L;

      existence

      proof

        z is Element of (C null X);

        then

        reconsider z1 = z as Element of C1 by TARSKI:def 3;

        o is Element of (C null X);

        then

        reconsider o1 = o as Element of C1 by TARSKI:def 3;

        

         A1: ( dom a) = (C \ {o}) by FUNCT_2:def 1;

        ( dom a1) = ((X \ {o}) \/ (C \ {o})) by FUNCT_4:def 1, A1

        .= ((X \/ C) \ {o}) by XBOOLE_1: 42;

        then ( dom a1) = (C1 \ {o1}) & ( rng a1) c= INT ;

        then a1 is Element of ( Funcs ((C1 \ {o1}), INT )) by FUNCT_2:def 2;

        then

        reconsider a11 = a1 as Function of (C1 \ {o1}), INT ;

        set new = Language-like (# C1, z1, o1, a11 #);

        reconsider new as strict non empty Language-like;

        take new;

        thus thesis;

      end;

      uniqueness

      proof

        let IT1,IT2 be strict non empty Language-like;

        set c1 = the carrier of IT1, z1 = the ZeroF of IT1, o1 = the OneF of IT1, a1 = the adicity of IT1;

        set c2 = the carrier of IT2, z2 = the ZeroF of IT2, o2 = the OneF of IT2, a2 = the adicity of IT2;

        set ITT1 = Language-like (# c1, z1, o1, a1 #), ITT2 = Language-like (# c2, z2, o2, a2 #);

        reconsider ITT1, ITT2 as non empty Language-like;

        defpred P[ Language-like] means the adicity of $1 = ((f | (( dom f) \ {o})) +* a) & the ZeroF of $1 = z & the OneF of $1 = o;

        assume

         A2: P[IT1] & P[IT2];

        ( dom a1) = (c2 \ {o1}) by FUNCT_2:def 1, A2;

        

        then ((c1 \ {o1}) \/ ( {o1} null c1)) = ((c2 \ {o2}) \/ ( {o2} null c2)) by A2, FUNCT_2:def 1

        .= c2;

        hence thesis by A2;

      end;

    end

    registration

      let S be non empty Language-like;

      let f be INT -valued Function;

      cluster (S extendWith f) -> S -extending;

      coherence

      proof

        set S1 = S, S2 = (S1 extendWith f), a1 = the adicity of S1, a2 = the adicity of S2, o1 = the OneF of S1;

        

         A1: ( TheEqSymbOf S1) = ( TheEqSymbOf S2) & ( TheNorSymbOf S1) = ( TheNorSymbOf S2) by Def42;

        a2 = ((f | (( dom f) \ {o1})) +* a1) by Def42;

        hence thesis by A1, FUNCT_4: 25;

      end;

    end

    registration

      let S be non degenerated Language-like;

      cluster S -extending -> non degenerated for Language-like;

      coherence

      proof

        set S1 = S;

        let S2 be Language-like;

        assume S2 is S -extending;

        then ( TheEqSymbOf S1) = ( TheEqSymbOf S2) & ( TheNorSymbOf S1) = ( TheNorSymbOf S2);

        then ( 0. S1) = ( 0. S2) & ( 1. S1) = ( 1. S2);

        hence thesis;

      end;

    end

    registration

      let S be eligible Language-like;

      cluster S -extending -> eligible for Language-like;

      coherence

      proof

        set S1 = S;

        let S2 be Language-like;

        set L1 = ( LettersOf S1), L2 = ( LettersOf S2), AS1 = ( AtomicFormulaSymbolsOf S1), AS2 = ( AtomicFormulaSymbolsOf S2), a1 = the adicity of S1, a2 = the adicity of S2, E1 = ( TheEqSymbOf S1), E2 = ( TheEqSymbOf S2);

        assume

         A1: S2 is S1 -extending;

        then

         A2: ( dom a1) = AS1 & ( dom a2) = AS2 & E1 = E2 & a1 c= a2 by FUNCT_2:def 1;

        reconsider a11 = a1 as Subset of a2 by A1;

        (a11 " { 0 }) c= (a2 " { 0 }) by RELAT_1: 144;

        then

        reconsider L11 = L1 as Subset of L2;

        (L2 null L11) is infinite;

        hence L2 is infinite;

        (a1 . E1) = ( - 2) by Def23;

        then E1 in ( dom a1) by FUNCT_1:def 2;

        

        then (a1 . E1) = ((a2 +* a11) . E1) by FUNCT_4: 13

        .= (a2 . E2) by FUNCT_4: 98, A2;

        hence (a2 . E2) = ( - 2) by Def23;

      end;

    end

    registration

      let E be empty Relation;

      let X;

      cluster (X |` E) -> empty;

      coherence by RELAT_1: 107;

    end

    

     Lm12: for S1 be non empty Language-like, f be INT -valued Function holds (( LettersOf (S1 extendWith f)) = (((f | (( dom f) \ ( AllSymbolsOf S1))) " { 0 }) \/ ( LettersOf S1)) & (the adicity of (S1 extendWith f) | ( OwnSymbolsOf S1)) = (the adicity of S1 | ( OwnSymbolsOf S1)))

    proof

      let S1 be non empty Language-like;

      let f be INT -valued Function;

      set S2 = (S1 extendWith f), L1 = ( LettersOf S1), a1 = the adicity of S1, a2 = the adicity of S2, z1 = the ZeroF of S1, o1 = the OneF of S1, X = (( dom f) \ {o1}), C1 = the carrier of S1, O1 = ( OwnSymbolsOf S1), L2 = ( LettersOf S2), f1 = (f | (X \ ( dom a1))), SS1 = ( AllSymbolsOf S1);

      C1 = ((C1 \ {o1}) \/ ( {o1} null C1))

      .= (( dom a1) \/ {o1}) by FUNCT_2:def 1;

      then f1 = (f | (( dom f) \ C1)) by XBOOLE_1: 41;

      

      then

       A1: ((f | (( dom f) \ C1)) \/ a1) = ((f | X) +* a1) by FOMODEL0: 57

      .= a2 by Def42;

      hence L2 = (((f | (( dom f) \ SS1)) " { 0 }) \/ L1) by FOMODEL0: 23;

      reconsider Y = (O1 /\ ( dom f)) as Subset of C1 by XBOOLE_1: 1;

      

      thus (a2 | O1) = ((a1 | O1) \/ ((f | (( dom f) \ C1)) | O1)) by A1, FOMODEL0: 56

      .= ((a1 | O1) \/ (f | (O1 /\ (( dom f) \ C1)))) by RELAT_1: 71

      .= ((a1 | O1) \/ (f | (Y \ C1)))

      .= (a1 | O1);

    end;

    registration

      let X;

      let m be Integer;

      cluster (X --> m) -> INT -valued;

      coherence

      proof

        reconsider mm = m as Element of INT by INT_1:def 2;

        (X --> m) is {mm} -valued;

        hence thesis;

      end;

    end

    definition

      let S;

      let X be functional set;

      :: FOMODEL1:def43

      func S addLettersNotIn X -> S -extending Language equals (S extendWith (((( AllSymbolsOf S) \/ ( SymbolsOf X)) -freeCountableSet ) --> 0 ) qua INT -valued Function);

      coherence ;

    end

    registration

      let S1;

      let X be functional set;

      cluster (( LettersOf (S1 addLettersNotIn X)) \ ( SymbolsOf X)) -> infinite;

      coherence

      proof

        set L1 = ( LettersOf S1), S2 = (S1 addLettersNotIn X), no = ( SymbolsOf X), L2 = ( LettersOf S2), IT = (L2 \ no), a1 = the adicity of S1, a2 = the adicity of S2, SS1 = ( AllSymbolsOf S1), fresh = ((SS1 \/ no) -freeCountableSet );

        reconsider f = (fresh --> 0 ) as INT -valued Function;

        

         A1: 0 in { 0 } & ( dom (fresh --> 0 )) = fresh by TARSKI:def 1;

        (fresh /\ (SS1 \/ no)) = {} ;

        then fresh misses (SS1 null no) & fresh misses (no null SS1) by XBOOLE_1: 63, XBOOLE_0:def 7;

        then

         A2: (fresh \ SS1) = fresh & (fresh \ no) = fresh by XBOOLE_1: 83;

        L2 = (((f | (( dom f) \ SS1)) " { 0 }) \/ L1) by Lm12;

        

        then IT = (((((f null {} ) | ( {} \/ ( dom f))) " { 0 }) \ no) \/ (L1 \ no)) by XBOOLE_1: 42, A2

        .= (fresh \/ (L1 \ no)) by FUNCOP_1: 14, A1, A2;

        hence thesis;

      end;

    end

    registration

      cluster countable for Language;

      existence

      proof

        reconsider z = 0 , o = 1 as Element of NAT ;

        set D = ( NAT \ {o});

        z in NAT & not z in {o};

        then

        reconsider zz = z as Element of D by XBOOLE_0:def 5;

        reconsider f = (D --> 0 ), g = (zz .--> ( - 2)) as INT -valued Function;

        set a = (f +* g);

        

         A1: zz in {zz} & ( dom g) = {zz} & ( dom f) = D by TARSKI:def 1;

        ( dom a) = (D null {zz}) by FUNCT_4:def 1;

        then ( rng a) c= INT & ( dom a) = D;

        then a is Element of ( Funcs (D, INT )) by FUNCT_2:def 2;

        then

        reconsider aa = a as Function of D, INT ;

        set IT = Language-like (# NAT , z, o, aa #);

        

         A2: ( 0. IT) <> ( 1. IT);

        (aa . z) = (g . zz) by A1, FUNCT_4: 13

        .= ( - 2) by A1, FUNCOP_1: 7;

        then

         A3: (aa . ( TheEqSymbOf IT)) = ( - 2);

        now

          let x be object;

          assume x in (D \ {z});

          then

           A4: x in D & not x in {zz};

          then x in ( dom aa) & not x in ( dom g) by FUNCT_2:def 1;

          

          then (aa . x) = (f . x) by FUNCT_4: 11

          .= 0 ;

          then x in ( dom aa) & (aa . x) in { 0 } by TARSKI:def 1, A4, FUNCT_2:def 1;

          hence x in (aa " { 0 }) by FUNCT_1:def 7;

        end;

        then

        reconsider E = (D \ {z}) as Subset of (aa " { 0 }) by TARSKI:def 3;

        E is infinite & ((aa " { 0 }) \/ E) = ((aa " { 0 }) null E);

        then ( LettersOf IT) is infinite;

        then

        reconsider IT as Language by A2, STRUCT_0:def 8, A3, Def23;

        take IT;

        thus thesis by ORDERS_4:def 2;

      end;

    end

    registration

      let S be countable Language;

      cluster ( AllSymbolsOf S) -> countable;

      coherence by ORDERS_4:def 2;

    end

    registration

      let S be countable Language;

      cluster ((( AllSymbolsOf S) * ) \ { {} }) -> countable;

      coherence

      proof

        set SS = ( AllSymbolsOf S);

        reconsider C = (SS * ) as countable set by CARD_4: 13;

        reconsider IT = (C \ { {} }) as Subset of C;

        IT is countable;

        hence thesis;

      end;

    end

    registration

      let L be non empty Language-like;

      let f be INT -valued Function;

      cluster (( AllSymbolsOf (L extendWith f)) \+\ (( dom f) \/ ( AllSymbolsOf L))) -> empty;

      coherence

      proof

        set L1 = L, a1 = the adicity of L1, SS1 = ( AllSymbolsOf L1), L2 = (L extendWith f), SS2 = ( AllSymbolsOf L2), a2 = the adicity of L2, X = ( dom f), E1 = ( TheEqSymbOf L1), N1 = ( TheNorSymbOf L1), E2 = ( TheEqSymbOf L2), N2 = ( TheNorSymbOf L2);

        reconsider Y = (X \ {N1}) as Subset of X;

        a2 = ((f | (X \ {N1})) +* a1) by Def42;

        then ( dom a2) = (( dom (f | Y)) \/ ( dom a1)) by FUNCT_4:def 1;

        

        then

         A1: (SS2 \ {N2}) = (Y \/ ( dom a1)) by FUNCT_2:def 1

        .= (Y \/ (SS1 \ {N1})) by FUNCT_2:def 1;

        reconsider NN1 = {N1} as non empty Subset of SS1 by ZFMISC_1: 31;

        reconsider NN2 = {N2} as non empty Subset of SS2 by ZFMISC_1: 31;

        NN1 c= SS1 & (SS1 null X) c= (SS1 \/ X);

        then

        reconsider NN11 = NN1 as non empty Subset of (SS1 \/ X) by XBOOLE_1: 1;

        SS2 = (NN2 \/ (SS2 \ NN2)) & SS1 = (NN1 \/ (SS1 \ NN1)) by XBOOLE_1: 45;

        

        then SS2 = ((NN2 \/ (SS1 \ NN1)) \/ Y) by XBOOLE_1: 4, A1

        .= ((NN1 \/ (SS1 \ NN1)) \/ Y) by Def41

        .= (NN1 \/ ((SS1 \ NN1) \/ Y)) by XBOOLE_1: 4

        .= (NN11 \/ ((SS1 \/ X) \ NN11)) by XBOOLE_1: 42

        .= (SS1 \/ X) by XBOOLE_1: 45;

        hence thesis;

      end;

    end

    registration

      let S be countable Language;

      let X be functional set;

      cluster (S addLettersNotIn X) -> countable;

      coherence

      proof

        set S1 = S, SS1 = ( AllSymbolsOf S1), SX = ( SymbolsOf X), add = ((SS1 \/ SX) -freeCountableSet ), f = (add --> 0 ), S2 = (S1 extendWith f), SS2 = ( AllSymbolsOf S2);

        (SS2 \+\ (( dom f) \/ SS1)) = {} ;

        

        then SS2 = (( dom f) \/ SS1) by FOMODEL0: 29

        .= (add \/ SS1);

        hence thesis by ORDERS_4:def 2;

      end;

    end

    definition

      let S be ZeroOneStr;

      :: original: degenerated

      redefine

      :: FOMODEL1:def44

      attr S is degenerated means

      : Def44: the ZeroF of S = the OneF of S;

      compatibility ;

    end

    registration

      let S;

      cluster ( AtomicTermsOf S) -> infinite;

      coherence

      proof

        set L = ( LettersOf S);

        ( card (1 -tuples_on L)) = ( card L) by CARD_4: 8;

        hence thesis;

      end;

    end

    theorem :: FOMODEL1:18

    (X /\ ( LettersOf S2)) is infinite implies ex S1 st (( OwnSymbolsOf S1) = (X /\ ( OwnSymbolsOf S2)) & S2 is S1 -extending)

    proof

      set L2 = ( LettersOf S2), O2 = ( OwnSymbolsOf S2), a2 = the adicity of S2, E2 = ( TheEqSymbOf S2), N2 = ( TheNorSymbOf S2), SS2 = ( AllSymbolsOf S2);

      reconsider X1 = (SS2 /\ X) as Subset of SS2;

      reconsider N22 = N2, E22 = E2 as Element of SS2;

       {E22, N22} is Subset of SS2;

      then

      reconsider X2 = {E2, N2} as non empty Subset of SS2;

      set SS1 = (X1 \/ X2);

      assume (X /\ L2) is infinite;

      then

      reconsider L11 = (X /\ L2) as infinite set;

      L11 c= ((X /\ SS2) null {E2, N2}) by XBOOLE_1: 26;

      then

      reconsider SS11 = SS1 as infinite Subset of SS2;

      reconsider AS11 = (SS11 \ {N2}) as infinite Subset of SS11;

      E2 in (X2 null X1) & not E2 in {N2} by TARSKI:def 1, TARSKI:def 2;

      then

      reconsider E1 = E2 as Element of AS11 by XBOOLE_0:def 5;

      N2 in (X2 null X1) by TARSKI:def 2;

      then

      reconsider N1 = N2 as Element of SS11;

      reconsider D1 = (SS11 \ {N1}) as infinite Subset of (SS2 \ {N2}) by XBOOLE_1: 33;

      ( rng (a2 | D1)) c= INT & ( dom (a2 | D1)) = D1 by PARTFUN1:def 2;

      then

      reconsider a1 = (a2 | D1) as Function of (SS11 \ {N1}), INT by FUNCT_2: 2;

      reconsider a11 = (a2 | D1) as Subset of a2;

      set S1 = Language-like (# SS11, E1 qua Element of SS11, N1, a1 #), O1 = ( OwnSymbolsOf S1), L1 = ( LettersOf S1);

      reconsider IT = S1 as non degenerated Language-like by Def44;

      

       A1: L1 = ((a2 " { 0 }) /\ D1) by FUNCT_1: 70

      .= ((L2 /\ SS11) \ {N1}) by XBOOLE_1: 49

      .= (((L2 /\ (SS2 /\ X)) \/ (L2 /\ {E2, N2})) \ {N2}) by XBOOLE_1: 23

      .= ((((L2 null SS2) /\ X) \/ (L2 /\ {E2, N2})) \ {N2}) by XBOOLE_1: 16

      .= ((L11 \/ (L2 /\ {E2, N2})) \ {N2});

      ((a1 . E1) \+\ (a2 . E1)) = {} ;

      then (a1 . E1) = (a2 . E2) & (a2 . E2) = ( - 2) by Def23, FOMODEL0: 29;

      then (the adicity of IT . ( TheEqSymbOf IT)) = ( - 2) & ( LettersOf IT) is infinite by A1;

      then

      reconsider IT as Language by Def23;

      take IT;

      (SS1 \ X2) = ((X1 \ X2) \/ (X2 \ X2)) by XBOOLE_1: 42

      .= (O2 /\ X) by XBOOLE_1: 49;

      hence ( OwnSymbolsOf IT) = (X /\ O2);

      thus thesis;

    end;

    definition

      let S;

      let w1,w2 be string of S;

      :: original: ^

      redefine

      func w1 ^ w2 -> string of S ;

      coherence

      proof

        set SS = ( AllSymbolsOf S);

        reconsider w11 = w1, w22 = w2 as non empty FinSequence of SS by FOMODEL0: 5;

        (w11 ^ w22) is non empty FinSequence of SS;

        hence thesis by FOMODEL0: 5;

      end;

    end

    definition

      let S, s;

      :: original: <*

      redefine

      func <*s*> -> string of S ;

      coherence

      proof

        set SS = ( AllSymbolsOf S);

         <*s*> is non empty FinSequence of SS;

        hence thesis by FOMODEL0: 5;

      end;

    end

    

     Lm13: (( <*( TheEqSymbOf S)*> ^ t1) ^ t2) is 0wff string of S

    proof

      set E = ( TheEqSymbOf S), AT = ( AllTermsOf S), C = (S -multiCat ), SS = ( AllSymbolsOf S);

      reconsider tt1 = t1, tt2 = t2 as Element of AT by Def32;

      reconsider T = ( <*tt1*> ^ <*tt2*>) as 2 -element Element of (AT * );

      reconsider ATT = AT as Subset of (SS * ) by XBOOLE_1: 1;

      reconsider TT = T as Element of (ATT * );

      reconsider TTT = TT as Element of ((SS * ) * );

      reconsider EE = E as ofAtomicFormula Element of S;

      

       A1: |.( - 2).| = ( - ( - 2)) by ABSVALUE:def 1

      .= 2;

      

       A2: |.( ar EE).| = 2 by A1, Def23;

      (C . TT) is Element of (SS * );

      then

      reconsider tailer = (C . T) as FinSequence of SS;

      reconsider SSS = SS as non empty set;

      reconsider EEE = EE as Element of SSS;

      reconsider header = <*EEE*> as FinSequence of SS;

      reconsider IT = (header ^ tailer) as non empty FinSequence of SS;

      reconsider phi = IT as string of S by Th12;

      tailer = ((SS -multiCat ) . <*tt1, tt2*>)

      .= (tt1 ^ tt2) by FOMODEL0: 15;

      then phi = (( <*E*> ^ tt1) ^ tt2) & phi is 0wff string of S by A2, Def35, FINSEQ_1: 32;

      hence thesis;

    end;

    registration

      let S;

      let t1,t2 be termal string of S;

      cluster (( <*( TheEqSymbOf S)*> ^ t1) ^ t2) -> 0wff;

      coherence by Lm13;

    end