fomodel2.miz



    begin

    reserve k,m,n for Nat,

kk,mm,nn for Element of NAT ,

A,B,X,Y,Z,x,y,z for set,

S,S1,S2 for Language,

s for Element of S,

w,w1,w2 for string of S,

U,U1,U2 for non empty set,

f,g for Function,

p,p1,p2 for FinSequence;

    definition

      let S;

      :: original: TheNorSymbOf

      redefine

      func TheNorSymbOf S -> Element of S ;

      coherence ;

    end

    definition

      let U be non empty set;

      :: FOMODEL2:def1

      func U -deltaInterpreter -> Function of (2 -tuples_on U), BOOLEAN equals ( chi (((U -concatenation ) .: ( id (1 -tuples_on U))),(2 -tuples_on U)));

      coherence ;

    end

    definition

      let X be set;

      :: original: id

      redefine

      func id X -> Equivalence_Relation of X ;

      coherence by EQREL_1: 3;

    end

    definition

      let S be Language;

      let U be non empty set;

      let s be ofAtomicFormula Element of S;

      :: FOMODEL2:def2

      mode Interpreter of s,U -> set means

      : Def2: it is Function of ( |.( ar s).| -tuples_on U), BOOLEAN if s is relational

      otherwise it is Function of ( |.( ar s).| -tuples_on U), U;

      existence

      proof

        thus s is relational implies ex IT be set st IT is Function of ( |.( ar s).| -tuples_on U), BOOLEAN

        proof

          assume s is relational;

          take the Function of ( |.( ar s).| -tuples_on U), BOOLEAN ;

          thus thesis;

        end;

        assume not s is relational;

        take the Function of ( |.( ar s).| -tuples_on U), U;

        thus thesis;

      end;

      consistency ;

    end

    definition

      let S, U;

      let s be ofAtomicFormula Element of S;

      :: original: Interpreter

      redefine

      mode Interpreter of s,U -> Function of ( |.( ar s).| -tuples_on U), (U \/ BOOLEAN ) ;

      coherence

      proof

        let f be Interpreter of s, U;

        set n = |.( ar s).|, D = (n -tuples_on U), C = (U \/ BOOLEAN );

        D c= (D \/ {} );

        then

        reconsider DD = D as Subset of D;

        reconsider C1 = BOOLEAN , C2 = U as Subset of C by XBOOLE_1: 7;

        per cases ;

          suppose s is relational;

          then

          reconsider ff = f as Function of DD, C1 by Def2;

           [:DD, C1:] c= [:D, C:];

          then

          reconsider fff = ff as Relation of D, C by XBOOLE_1: 1;

          fff is Function of D, C;

          hence thesis;

        end;

          suppose not s is relational;

          then

          reconsider ff = f as Function of DD, C2 by Def2;

           [:DD, C2:] c= [:D, C:];

          then

          reconsider fff = ff as Relation of D, C by XBOOLE_1: 1;

          fff is Function of D, C;

          hence thesis;

        end;

      end;

    end

    registration

      let S, U;

      let s be termal Element of S;

      cluster -> U -valued for Interpreter of s, U;

      coherence by Def2;

    end

    registration

      let S be Language;

      cluster literal -> own for Element of S;

      coherence ;

    end

    definition

      let S, U;

      :: FOMODEL2:def3

      mode Interpreter of S,U -> Function means

      : Def3: for s be own Element of S holds (it . s) is Interpreter of s, U;

      existence

      proof

        set O = ( OwnSymbolsOf S);

        defpred P[ object, object] means ex s be own Element of S st $1 = s & $2 is Interpreter of s, U;

        

         A1: for x be object st x in O holds ex y be object st P[x, y]

        proof

          let x be object;

          assume x in O;

          then

          reconsider s = x as own Element of S by FOMODEL1:def 19;

          take y = the Interpreter of s, U;

          take s;

          thus x = s & y is Interpreter of s, U;

        end;

        consider f be Function such that

         A2: ( dom f) = O & for s be object st s in O holds P[s, (f . s)] from CLASSES1:sch 1( A1);

        take f;

        thus for s be own Element of S holds (f . s) is Interpreter of s, U

        proof

          let s be own Element of S;

          consider s1 be own Element of S such that

           A3: s = s1 & (f . s) is Interpreter of s1, U by A2, FOMODEL1:def 19;

          thus (f . s) is Interpreter of s, U by A3;

        end;

      end;

    end

    definition

      let S, U, f;

      :: FOMODEL2:def4

      attr f is S,U -interpreter-like means

      : Def4: f is Interpreter of S, U & f is Function-yielding;

    end

    registration

      let S;

      let U be non empty set;

      cluster S, U -interpreter-like -> Function-yielding for Function;

      coherence ;

    end

    registration

      let S, U;

      let s be own Element of S;

      cluster -> non empty for Interpreter of s, U;

      coherence ;

    end

    

     Lm1: for f be Interpreter of S, U holds ( OwnSymbolsOf S) c= ( dom f)

    proof

      set SS = ( AllSymbolsOf S), A = ( AtomicFormulaSymbolsOf S), O = ( OwnSymbolsOf S);

      let f be Interpreter of S, U;

      let x be object;

      assume x in O;

      then

      reconsider s = x as own Element of S by FOMODEL1:def 19;

      (f . s) is non empty by Def3;

      hence x in ( dom f) by FUNCT_1:def 2;

    end;

    

     Lm2: f is S, U -interpreter-like implies ( OwnSymbolsOf S) c= ( dom f) by Lm1;

    registration

      let S be Language;

      let U be non empty set;

      cluster S, U -interpreter-like for Function;

      existence

      proof

        set O = ( OwnSymbolsOf S), SS = ( AllSymbolsOf S);

        set I = the Interpreter of S, U;

        reconsider f = (I | O) as Function;

        

         A1: ( dom f) = (O /\ ( dom I)) by RELAT_1: 61

        .= O by XBOOLE_1: 28, Lm1;

        take f;

        

         A2: for s be own Element of S holds (f . s) is Interpreter of s, U & (f . s) is Function

        proof

          let s be own Element of S;

          

           A3: (f . s) = (I . s) by FUNCT_1: 47, A1, FOMODEL1:def 19;

          hence (f . s) is Interpreter of s, U by Def3;

          thus (f . s) is Function by A3, Def3;

        end;

        then

        reconsider ff = f as Interpreter of S, U by Def3;

        now

          let x be object;

          assume x in ( dom f);

          then

          reconsider s = x as own Element of S by A1, FOMODEL1:def 19;

          (ff . s) is Function by A2;

          hence (ff . x) is Function;

        end;

        hence thesis by FUNCOP_1:def 6;

      end;

    end

    definition

      let S, U;

      let I be S, U -interpreter-like Function;

      let s be own Element of S;

      :: original: .

      redefine

      func I . s -> Interpreter of s, U ;

      coherence

      proof

        reconsider I as Interpreter of S, U by Def4;

        (I . s) is Interpreter of s, U by Def3;

        hence thesis;

      end;

    end

    registration

      let S be Language, U be non empty set;

      let I be S, U -interpreter-like Function;

      let x be own Element of S, f be Interpreter of x, U;

      cluster (I +* (x .--> f)) -> S, U -interpreter-like;

      coherence

      proof

        set g = (x .--> f), O = ( OwnSymbolsOf S), h = (I +* g);

        O c= ( dom I) & ( dom I) c= (( dom I) \/ ( dom g)) by Lm2, XBOOLE_1: 7;

        then

         A1: O c= (( dom I) \/ ( dom g));

        reconsider I as Interpreter of S, U by Def4;

        now

          let s be own Element of S;

          

           A2: s in O by FOMODEL1:def 19;

          per cases ;

            suppose

             A3: s in ( dom g);

            

            then

             A4: (h . s) = (g . s) by FUNCT_4:def 1, A2, A1

            .= f by FUNCOP_1: 7, A3;

            thus (h . s) is Interpreter of s, U by A4, A3, TARSKI:def 1;

          end;

            suppose not s in ( dom g);

            then (h . s) = (I . s) by FUNCT_4:def 1, A1, A2;

            hence (h . s) is Interpreter of s, U by Def3;

          end;

        end;

        then h is Interpreter of S, U & h is Function-yielding by Def3;

        hence thesis;

      end;

    end

    definition

      let f, x, y;

      :: FOMODEL2:def5

      func (x,y) ReassignIn f -> Function equals (f +* (x .--> ( {} .--> y)));

      coherence ;

    end

    registration

      let S be Language, U be non empty set, I be S, U -interpreter-like Function;

      let x be literal Element of S, u be Element of U;

      cluster ((x,u) ReassignIn I) -> S, U -interpreter-like;

      coherence

      proof

        set h = ((x,u) ReassignIn I), n = |.( ar x).|;

        n = 0 & { {} } = ( 0 -tuples_on U) by FOMODEL0: 10;

        then

        reconsider f = ( { {} } --> u) as Function of (n -tuples_on U), U;

        reconsider ff = f as Interpreter of x, U by Def2;

        h = (I +* (x .--> ff));

        hence thesis;

      end;

    end

    registration

      let S be Language;

      cluster ( AllSymbolsOf S) -> non empty;

      coherence ;

    end

    registration

      let Y be set;

      let X,Z be non empty set;

      cluster -> Function-yielding for Function of X, ( Funcs (Y,Z));

      coherence ;

    end

    registration

      let X,Y,Z be non empty set;

      cluster Function-yielding for Function of X, ( Funcs (Y,Z));

      existence

      proof

        take the Function of X, ( Funcs (Y,Z));

        thus thesis;

      end;

    end

    definition

      let f be Function-yielding Function, g be Function;

      :: FOMODEL2:def6

      func ^^^g,f__ -> Function means

      : Def6: ( dom it ) = ( dom f) & for x st x in ( dom f) holds (it . x) = (g * (f . x));

      existence

      proof

        deffunc F( object) = (g * (f . $1));

        consider h be Function such that

         A1: ( dom h) = ( dom f) & for x be object st x in ( dom f) holds (h . x) = F(x) from FUNCT_1:sch 3;

        take h;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let IT1,IT2 be Function;

        assume

         A2: ( dom IT1) = ( dom f) & for x st x in ( dom f) holds (IT1 . x) = (g * (f . x));

        assume

         A3: ( dom IT2) = ( dom f) & for x st x in ( dom f) holds (IT2 . x) = (g * (f . x));

        now

          let x be object;

          assume x in ( dom IT1);

          then (IT1 . x) = (g * (f . x)) & (IT2 . x) = (g * (f . x)) by A2, A3;

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

        end;

        hence thesis by A2, A3, FUNCT_1: 2;

      end;

    end

    registration

      let f be empty Function, g be Function;

      cluster ^^^g, f__ -> empty;

      coherence

      proof

        ( dom ^^^g, f__) = ( dom f) by Def6

        .= {} ;

        hence thesis;

      end;

    end

    definition

      ::$Canceled

    end

    registration

      let f be Function-yielding Function, g be empty Function;

      cluster ^^^f, g__ -> empty;

      coherence ;

    end

    registration

      let E,D be non empty set, p be D -valued FinSequence, h be Function of D, E;

      cluster (h * p) -> ( len p) -element;

      coherence

      proof

        reconsider pp = p as FinSequence of D by FOMODEL0: 26;

        ( len (h * pp)) = ( len pp) by FINSEQ_2: 33;

        hence thesis by CARD_1:def 7;

      end;

    end

    registration

      let X,Y be non empty set;

      let f be Function of X, Y;

      let p be X -valued FinSequence;

      cluster (f * p) -> FinSequence-like;

      coherence ;

    end

    registration

      let E,D be non empty set, n be Nat, p be n -elementD -valued FinSequence, h be Function of D, E;

      cluster (h * p) -> n -element;

      coherence ;

    end

    

     Lm3: for U be non empty set, S be Language, I be S, U -interpreter-like Function, t be termal string of S holds ( |.( ar t).| -tuples_on U) = ( dom (I . ((S -firstChar ) . t))) by FUNCT_2:def 1;

    theorem :: FOMODEL2:1

    for t0 be 0 -termal string of S holds t0 = <*((S -firstChar ) . t0)*>

    proof

      let t0 be 0 -termal string of S;

      reconsider e = ((S -multiCat ) . ( SubTerms t0)) as empty set;

      t0 = ( <*((S -firstChar ) . t0)*> ^ e) by FOMODEL1:def 37

      .= <*((S -firstChar ) . t0)*>;

      hence thesis;

    end;

    

     Lm4: for I be S, U -interpreter-like Function, xx be Function of ( AllTermsOf S), U holds ( ^^^(I * (S -firstChar )), ^^^xx, (S -subTerms )____ is Element of ( Funcs (( AllTermsOf S),U)) & ( AllTermsOf S) c= ( dom (I * (S -firstChar ))))

    proof

      let I be S, U -interpreter-like Function;

      set A = ( AllTermsOf S), F = (S -firstChar ), ST = (S -subTerms ), SS = ( AllSymbolsOf S), Z = ( AtomicTermsOf S), T = (S -termsOfMaxDepth );

      

       A1: ( dom F) = ((SS * ) \ { {} }) by FUNCT_2:def 1;

      let xx be Function of A, U;

      set f = ^^^xx, ST__, g = ^^^(I * F), f__;

      

       A2: ( dom f) = ( dom ST) by Def6

      .= A by FUNCT_2:def 1;

      

       A3: for a be set st a in A holds (a in ( dom (I * F)) & (a in ( dom g) implies (g . a) in U))

      proof

        let a be set;

        assume

         A4: a in A;

        then

        reconsider t = a as termal string of S;

        set n = |.( ar t).|;

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

        reconsider s = ss as own Element of S;

        reconsider t1 = s as Element of ( OwnSymbolsOf S) by FOMODEL1:def 19;

        t1 in ( OwnSymbolsOf S) & ( OwnSymbolsOf S) c= ( dom I) by Lm2;

        hence

         A5: a in ( dom (I * F)) by FUNCT_1: 11, A1;

        reconsider tt = a as Element of A by A4;

        reconsider i = (I . s) as Interpreter of s, U;

        (ST . tt) = ( SubTerms t) by FOMODEL1:def 39;

        then

        reconsider y = (ST . tt) as n -element FinSequence of A by FINSEQ_1:def 11;

        reconsider z = (xx * y) as n -element FinSequence of U;

        ( len z) = n by CARD_1:def 7;

        then

        reconsider zz = z as Element of (n -tuples_on U) by FINSEQ_2: 133;

        (n -tuples_on U) c= ( dom (I . t1)) by Lm3;

        then

         A6: zz in ( dom i);

        tt in A;

        then

         A7: tt in ( dom ST) by FUNCT_2:def 1;

        assume a in ( dom g);

        

        then (g . t) = (((I * F) . t) . (f . t)) by FOMODEL0:def 4

        .= ((I . s) . (f . t)) by A5, FUNCT_1: 12

        .= (i . zz) by Def6, A7;

        hence (g . a) in U by A6, FUNCT_1: 102;

      end;

      then

       A8: for a be object st a in A holds a in ( dom (I * F));

      

       A9: ( dom g) = (( dom (I * F)) /\ A) by A2, FOMODEL0:def 4

      .= A by A8, TARSKI:def 3, XBOOLE_1: 28;

      then for a be object st a in A holds (g . a) in U by A3;

      then g is Function of A, U by FUNCT_2: 3, A9;

      hence g is Element of ( Funcs (A,U)) by FUNCT_2: 8;

      thus thesis by A8;

    end;

    definition

      let S;

      let U be non empty set, u be Element of U;

      let I be S, U -interpreter-like Function;

      :: FOMODEL2:def8

      func (I,u) -TermEval -> sequence of ( Funcs (( AllTermsOf S),U)) means

      : Def7: (it . 0 ) = (( AllTermsOf S) --> u) & for mm holds (it . (mm + 1)) = ^^^(I * (S -firstChar )), ^^^(it . mm) qua Function, (S -subTerms )____;

      existence

      proof

        set A = ( AllTermsOf S), F = (S -firstChar ), ST = (S -subTerms ), SS = ( AllSymbolsOf S), Z = ( AtomicTermsOf S), T = (S -termsOfMaxDepth ), fz = (A --> u);

        defpred P[ set, Element of ( Funcs (A,U)), set] means $3 = ^^^(I * F), ^^^$2, ST____;

        reconsider fzz = fz as Function of A, U;

        reconsider fzzz = fzz as Element of ( Funcs (A,U)) by FUNCT_2: 8;

        

         A1: for mm be Nat holds for x be Element of ( Funcs (A,U)) holds ex y be Element of ( Funcs (A,U)) st P[mm, x, y]

        proof

          let mm be Nat;

          let x be Element of ( Funcs (A,U));

          reconsider xx = x as Function of A, U;

          reconsider yy = ^^^(I * F), ^^^xx, ST____ as Function of A, U by Lm4;

          reconsider yyy = yy as Element of ( Funcs (A,U)) by FUNCT_2: 8;

          take yyy;

          thus thesis;

        end;

        consider f be sequence of ( Funcs (A,U)) such that

         A2: ((f . 0 ) = fzzz & for mm be Nat holds P[mm, (f . mm) qua Element of ( Funcs (A,U)), (f . (mm + 1))]) from RECDEF_1:sch 2( A1);

        take f;

        thus thesis by A2;

      end;

      uniqueness

      proof

        set A = ( AllTermsOf S), F = (S -firstChar ), ST = (S -subTerms ), SS = ( AllSymbolsOf S), Z = ( AtomicTermsOf S), T = (S -termsOfMaxDepth ), fz = (A --> u);

        reconsider fzz = fz as Element of ( Funcs (A,U)) by FUNCT_2: 8;

        defpred P[ set, set, set] means for f be Element of ( Funcs (A,U)) st $2 = f holds $3 = ^^^(I * F), ^^^f, ST____;

        let IT1,IT2 be sequence of ( Funcs (A,U));

        assume

         A3: (IT1 . 0 ) = fz & for mm holds (IT1 . (mm + 1)) = ^^^(I * F), ^^^(IT1 . mm), ST____;

        assume

         A4: (IT2 . 0 ) = fz & for mm holds (IT2 . (mm + 1)) = ^^^(I * F), ^^^(IT2 . mm), ST____;

        

         A5: (IT1 . 0 ) = fzz by A3;

        

         A6: for m holds P[m, (IT1 . m), (IT1 . (m + 1))]

        proof

          let m;

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

          let f be Element of ( Funcs (A,U));

          assume (IT1 . m) = f;

          then (IT1 . mm) = f;

          hence thesis by A3;

        end;

        

         A7: (IT2 . 0 ) = fzz by A4;

        

         A8: for m holds P[m, (IT2 . m), (IT2 . (m + 1))]

        proof

          let m;

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

          let f be Element of ( Funcs (A,U));

          assume (IT2 . m) = f;

          then (IT2 . mm) = f;

          hence thesis by A4;

        end;

        

         A9: for m be Nat, x,y1,y2 be Element of ( Funcs (A,U)) st P[m, x, y1] & P[m, x, y2] holds y1 = y2

        proof

          let m;

          let x,y1,y2 be Element of ( Funcs (A,U));

          assume for f be Element of ( Funcs (A,U)) st x = f holds y1 = ^^^(I * F), ^^^f, ST____;

          then

           A10: y1 = ^^^(I * F), ^^^x, ST____;

          assume for f be Element of ( Funcs (A,U)) st x = f holds y2 = ^^^(I * F), ^^^f, ST____;

          hence y1 = y2 by A10;

        end;

        IT1 = IT2 from NAT_1:sch 14( A5, A6, A7, A8, A9);

        hence thesis;

      end;

    end

    

     Lm5: for u be Element of U, I be S, U -interpreter-like Function, t be termal string of S, mm be Element of NAT holds ((((I,u) -TermEval ) . (mm + 1)) . t) = ((I . ((S -firstChar ) . t)) . ((((I,u) -TermEval ) . mm) * ( SubTerms t))) & (t is 0 -termal implies ((((I,u) -TermEval ) . (mm + 1)) . t) = ((I . ((S -firstChar ) . t)) . {} ))

    proof

      let u be Element of U;

      let I be S, U -interpreter-like Function;

      let t be termal string of S;

      let mm;

      set TE = ((I,u) -TermEval ), F = (S -firstChar ), ST = (S -subTerms ), A = ( AllTermsOf S);

      

       A1: t in A & A c= ( dom (I * F)) by FOMODEL1:def 32, Lm4;

      reconsider tt = t as Element of A by FOMODEL1:def 32;

      set G = ^^^(I * F), ^^^(TE . mm), ST____;

      

       A2: ( dom ST) = A by FUNCT_2:def 1;

      G is Function of A, U by Lm4;

      then

       A3: ( dom G) = A by FUNCT_2:def 1;

      

       A4: ((TE . (mm + 1)) . t) = (G . t) by Def7

      .= (((I * F) . t) . ( ^^^(TE . mm), ST__ . t)) by A3, A1, FOMODEL0:def 4

      .= (((I * F) . t) . ((TE . mm) * (ST . tt))) by Def6, A2

      .= (((I * F) . t) . ((TE . mm) * ( SubTerms t))) by FOMODEL1:def 39

      .= ((I . (F . t)) . ((TE . mm) * ( SubTerms t))) by A1, FUNCT_1: 12;

      hence ((TE . (mm + 1)) . t) = ((I . (F . t)) . ((TE . mm) * ( SubTerms t)));

      assume t is 0 -termal;

      then

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

      reconsider s = (F . tt) as literal Element of S;

      reconsider v = (I . s) as Interpreter of s, U;

      ((TE . (mm + 1)) . t) = (v . {} ) by A4;

      hence thesis;

    end;

    

     Lm6: for I be S, U -interpreter-like Function, u1,u2 be Element of U holds for m be Nat holds for t be m -termal string of S, n be Nat holds ((((I,u1) -TermEval ) . (m + 1)) . t) = ((((I,u2) -TermEval ) . ((m + 1) + n)) . t)

    proof

      let I be S, U -interpreter-like Function, u1,u2 be Element of U;

      set F = (S -firstChar ), ST = (S -subTerms ), A = ( AllTermsOf S), T = (S -termsOfMaxDepth );

      set U1 = ((I,u1) -TermEval ), U2 = ((I,u2) -TermEval ), SS = ( AllSymbolsOf S);

      defpred P[ Nat] means for t be $1 -termal string of S, n be Nat holds ((U1 . ($1 + 1)) . t) = ((U2 . (($1 + 1) + n)) . t);

      

       A1: P[ 0 ]

      proof

        let t be 0 -termal string of S, n be Nat;

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

        ((U1 . ( 0 + 1)) . t) = ((I . ((S -firstChar ) . t)) . {} ) by Lm5

        .= ((U2 . (( 0 + 1) + nn)) . t) by Lm5;

        hence thesis;

      end;

      

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

      proof

        let k be Nat;

        assume

         A3: P[k];

        reconsider K = (k + 1) as Element of NAT ;

        let t be (k + 1) -termal string of S, n be Nat;

        reconsider KK = (K + n) as Element of NAT by ORDINAL1:def 12;

        reconsider tt = t as termal string of S;

        

         A4: ((U1 . K) * ( SubTerms t)) = ((U2 . (K + n)) * ( SubTerms t))

        proof

          set V = ( SubTerms t), l = |.( ar t).|;

          reconsider VV = V as l -element FinSequence of A by FINSEQ_1:def 11;

          reconsider kk = k as Element of NAT by ORDINAL1:def 12;

          reconsider tx = t as (kk + 1) -termal string of S;

          ( SubTerms tx) is (T . kk) -valued Function;

          then

          reconsider VVV = V as (T . k) -valued Function;

          ( len VV) = l by CARD_1:def 7;

          then

           A5: ( dom VVV) = ( Seg l) by FINSEQ_1:def 3;

          reconsider U1K = (U1 . K), U2K = (U2 . KK) as Function of A, U;

          reconsider p = (U1K * VV), q = (U2K * VV) as l -element FinSequence of U;

          ( len p) = l & ( len q) = l by CARD_1:def 7;

          then

           A6: ( dom p) = ( Seg l) & ( dom q) = ( Seg l) by FINSEQ_1:def 3;

          for i be object st i in ( Seg l) holds (p . i) = (q . i)

          proof

            let i be object;

            assume

             A7: i in ( Seg l);

            then

            reconsider t1 = (VVV . i) as k -termal string of S by FOMODEL1:def 33, A5, FUNCT_1: 102;

            (p . i) = ((U1 . K) . t1) by A7, A6, FUNCT_1: 12

            .= (U2K . (VVV . i)) by A3

            .= (q . i) by A7, A6, FUNCT_1: 12;

            hence thesis;

          end;

          hence thesis by A6, FUNCT_1: 2;

        end;

        ((U1 . (K + 1)) . tt) = ((I . (F . tt)) . ((U2 . KK) * ( SubTerms t))) by Lm5, A4

        .= ((U2 . (KK + 1)) . tt) by Lm5;

        hence thesis;

      end;

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

      hence thesis;

    end;

    definition

      let S, U;

      let I be S, U -interpreter-like Function;

      let t be Element of ( AllTermsOf S);

      :: FOMODEL2:def9

      func I -TermEval (t) -> Element of U means

      : Def8: for u1 be Element of U, mm st t in ((S -termsOfMaxDepth ) . mm) holds it = ((((I,u1) -TermEval ) . (mm + 1)) . t);

      existence

      proof

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

        consider mm such that

         A1: t in (T . mm) by FOMODEL1: 5;

        set u1 = the Element of U;

        reconsider t0 = t as string of S;

        reconsider t1 = t0 as mm -termal string of S by A1, FOMODEL1:def 33;

        reconsider mmm = (mm + 1) as Element of NAT ;

        reconsider f1 = (((I,u1) -TermEval ) . mmm) as Function of A, U;

        reconsider IT = (f1 . t) as Element of U;

        take IT;

        let u2 be Element of U, nn;

        assume t in (T . nn);

        then

        reconsider t2 = t0 as nn -termal string of S by FOMODEL1:def 33;

        IT = ((((I,u2) -TermEval ) . ((mm + 1) + nn)) . t1) by Lm6

        .= ((((I,u2) -TermEval ) . ((nn + 1) + mm)) . t2)

        .= ((((I,u2) -TermEval ) . (nn + 1)) . t2) by Lm6;

        hence thesis;

      end;

      uniqueness

      proof

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

        let IT1,IT2 be Element of U;

        assume

         A2: for u1 be Element of U, mm st t in (T . mm) holds IT1 = ((((I,u1) -TermEval ) . (mm + 1)) . t);

        assume

         A3: for u2 be Element of U, nn st t in (T . nn) holds IT2 = ((((I,u2) -TermEval ) . (nn + 1)) . t);

        consider mm such that

         A4: t in (T . mm) by FOMODEL1: 5;

        set u = the Element of U;

        IT1 = ((((I,u) -TermEval ) . (mm + 1)) . t) by A2, A4

        .= IT2 by A3, A4;

        hence thesis;

      end;

    end

    definition

      let S, U;

      let I be S, U -interpreter-like Function;

      :: FOMODEL2:def10

      func I -TermEval -> Function of ( AllTermsOf S), U means

      : Def9: for t be Element of ( AllTermsOf S) holds (it . t) = (I -TermEval t);

      existence

      proof

        set A = ( AllTermsOf S);

        deffunc F( Element of A) = (I -TermEval $1);

        consider f be Function of A, U 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, U;

        assume

         A2: for t be Element of ( AllTermsOf S) holds (IT1 . t) = (I -TermEval t);

        assume

         A3: for t be Element of ( AllTermsOf S) holds (IT2 . t) = (I -TermEval t);

        now

          let t be Element of A;

          

          thus (IT1 . t) = (I -TermEval t) by A2

          .= (IT2 . t) by A3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    definition

      let S, U;

      let I be S, U -interpreter-like Function;

      :: FOMODEL2:def11

      func I === -> Function equals (I +* (( TheEqSymbOf S) .--> (U -deltaInterpreter )));

      coherence ;

    end

    definition

      let S, U;

      let I be S, U -interpreter-like Function;

      let x be set;

      :: FOMODEL2:def12

      attr x is I -extension means

      : Def11: x = (I === );

    end

    registration

      let S, U;

      let I be S, U -interpreter-like Function;

      cluster (I === ) -> I -extension;

      coherence ;

      cluster I -extension -> Function-like for set;

      coherence ;

    end

    registration

      let S, U;

      let I be S, U -interpreter-like Function;

      cluster I -extension for Function;

      existence

      proof

        take f = (I === );

        thus thesis;

      end;

    end

    registration

      let S, U;

      let I be S, U -interpreter-like Function;

      cluster (I === ) -> S, U -interpreter-like;

      coherence

      proof

        set EQ = ( TheEqSymbOf S), g = (EQ .--> (U -deltaInterpreter )), O = ( OwnSymbolsOf S), A = ( AtomicFormulaSymbolsOf S);

        now

          let s be own Element of S;

          s in O by FOMODEL1:def 19;

          then not s in (A \ O) by XBOOLE_0:def 5;

          then not s in {EQ} by FOMODEL1: 9;

          then not s in ( dom g);

          then ((I === ) . s) = (I . s) by FUNCT_4: 11;

          hence ((I === ) . s) is Interpreter of s, U;

        end;

        hence (I === ) is Interpreter of S, U by Def3;

        thus thesis;

      end;

    end

    definition

      let S, U;

      let I be S, U -interpreter-like Function;

      let f be I -extension Function, s be ofAtomicFormula Element of S;

      :: original: .

      redefine

      func f . s -> Interpreter of s, U ;

      coherence

      proof

        set a = the adicity of S, EQ = ( TheEqSymbOf S), d = (U -deltaInterpreter ), g = (EQ .--> d), n = ( ar s), A = ( AtomicFormulaSymbolsOf S), O = ( OwnSymbolsOf S);

        reconsider sss = s as Element of A by FOMODEL1:def 20;

        reconsider EQQ = EQ as ofAtomicFormula Element of S;

        ( ar EQQ) = ( - 2) by FOMODEL1:def 23;

        

        then

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

        .= 2;

        

         A2: f = (I === ) by Def11;

        per cases ;

          suppose s is own;

          then

          reconsider ss = s as own Element of S;

          ((I === ) . ss) is Interpreter of s, U;

          hence thesis by Def11;

        end;

          suppose not s is own;

          then not sss in O;

          then sss in (A \ O) by XBOOLE_0:def 5;

          then sss in {EQ} by FOMODEL1: 9;

          then s = EQ by TARSKI:def 1;

          then (f . s) is Function of ( |.n.| -tuples_on U), BOOLEAN & s is relational by A1, A2, FUNCT_7: 94;

          hence thesis by Def2;

        end;

      end;

    end

    definition

      let S, U;

      let I be S, U -interpreter-like Function;

      let phi be 0wff string of S;

      :: FOMODEL2:def13

      func I -AtomicEval (phi) -> set equals (((I === ) . ((S -firstChar ) . phi)) . ((I -TermEval ) * ( SubTerms phi)));

      coherence ;

    end

    definition

      let S, U;

      let I be S, U -interpreter-like Function;

      let phi be 0wff string of S;

      :: original: -AtomicEval

      redefine

      func I -AtomicEval (phi) -> Element of BOOLEAN ;

      coherence

      proof

        set F = (S -firstChar ), i = (I -TermEval ), A = ( AllTermsOf S);

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

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

        reconsider f = ((I === ) . s) as Interpreter of s, U;

        reconsider ff = f as Function of (n -tuples_on U), BOOLEAN by Def2;

        reconsider V = ( SubTerms phi) as n -element FinSequence of A by FINSEQ_1:def 11;

        reconsider iV = (i * V) as n -element FinSequence of U;

        ( len iV) = n by CARD_1:def 7;

        then

        reconsider iVV = iV as Element of (n -tuples_on U) by FINSEQ_2: 133;

        (ff . iVV) is Element of BOOLEAN ;

        hence thesis;

      end;

    end

    registration

      let S, U;

      let I be S, U -interpreter-like Function;

      cluster (I | ( OwnSymbolsOf S)) -> ( PFuncs ((U * ),(U \/ BOOLEAN ))) -valued;

      coherence

      proof

        set O = ( OwnSymbolsOf S), f = (I | O), D = ( dom f), C = (U \/ BOOLEAN );

        now

          let y be object;

          assume y in ( rng f);

          then y in (f .: D);

          then

          consider x be object such that

           A1: x in D & x in D & y = (f . x) by FUNCT_1:def 6;

          x in O by A1;

          then

          reconsider s = x as own Element of S by FOMODEL1:def 19;

          reconsider n = |.( ar s).| as Element of NAT ;

          reconsider DD = (n -tuples_on U) as Subset of (U * ) by FINSEQ_2: 134;

          C c= C;

          then

          reconsider CC = C as Subset of C;

          (f . x) = (I . s) by FUNCT_1: 49, A1;

          then

          reconsider g = (f . x) as Function of DD, CC;

           [:DD, CC:] c= [:(U * ), C:];

          then

          reconsider gg = g as Relation of (U * ), C by XBOOLE_1: 1;

          gg is PartFunc of (U * ), C;

          hence y in ( PFuncs ((U * ),C)) by PARTFUN1: 45, A1;

        end;

        hence thesis by RELAT_1:def 19, TARSKI:def 3;

      end;

      cluster (I | ( OwnSymbolsOf S)) -> S, U -interpreter-like;

      coherence

      proof

        set O = ( OwnSymbolsOf S), f = (I | O), D = ( dom f), C = (U \/ BOOLEAN );

        now

          let s be own Element of S;

          (f . s) = (I . s) by FOMODEL1:def 19, FUNCT_1: 49;

          hence (f . s) is Interpreter of s, U;

        end;

        then f is Interpreter of S, U by Def3;

        hence thesis;

      end;

    end

    registration

      let S, U;

      let I be S, U -interpreter-like Function;

      cluster (I | ( OwnSymbolsOf S)) -> total;

      coherence

      proof

        set O = ( OwnSymbolsOf S), f = (I | O), D = ( dom f), C = (U \/ BOOLEAN );

        O c= ( dom f) & ( dom f) c= O by Lm2;

        hence thesis by PARTFUN1:def 2, XBOOLE_0:def 10;

      end;

    end

    definition

      let S, U;

      :: FOMODEL2:def14

      func U -InterpretersOf S -> set equals { f where f be Element of ( Funcs (( OwnSymbolsOf S),( PFuncs ((U * ),(U \/ BOOLEAN ))))) : f is S, U -interpreter-like };

      coherence ;

    end

    definition

      let S, U;

      :: original: -InterpretersOf

      redefine

      func U -InterpretersOf S -> Subset of ( Funcs (( OwnSymbolsOf S),( PFuncs ((U * ),(U \/ BOOLEAN ))))) ;

      coherence

      proof

        set I = (U -InterpretersOf S), O = ( OwnSymbolsOf S), C = ( PFuncs ((U * ),(U \/ BOOLEAN )));

        defpred P[ Element of ( Funcs (O,C))] means $1 is S, U -interpreter-like;

        { f where f be Element of ( Funcs (O,C)) : P[f] } is Subset of ( Funcs (O,C)) from DOMAIN_1:sch 7;

        hence thesis;

      end;

    end

    registration

      let S, U;

      cluster (U -InterpretersOf S) -> non empty;

      coherence

      proof

        set I = the S, U -interpreter-like Function;

        set O = ( OwnSymbolsOf S), f = (I | O), C = ( PFuncs ((U * ),(U \/ BOOLEAN )));

        ( dom f) c= O & ( rng f) c= C;

        then

        reconsider ff = f as Relation of O, C by RELSET_1: 4;

        reconsider fff = ff as Element of ( Funcs (O,C)) by FUNCT_2: 8;

        ex g be Element of ( Funcs (O,C)) st f = g & g is S, U -interpreter-like

        proof

          take fff;

          thus thesis;

        end;

        then f in (U -InterpretersOf S);

        hence thesis;

      end;

    end

    registration

      let S, U;

      cluster -> S, U -interpreter-like for Element of (U -InterpretersOf S);

      coherence

      proof

        set SUI = (U -InterpretersOf S), O = ( OwnSymbolsOf S), C = ( PFuncs ((U * ),(U \/ BOOLEAN )));

        let x be Element of SUI;

        x in SUI;

        then

        consider f be Element of ( Funcs (O,C)) such that

         A1: x = f & f is S, U -interpreter-like;

        thus thesis by A1;

      end;

    end

    definition

      let S, U;

      :: FOMODEL2:def15

      func S -TruthEval (U) -> Function of [:(U -InterpretersOf S), ( AtomicFormulasOf S):], BOOLEAN means

      : Def14: for I be Element of (U -InterpretersOf S), phi be Element of ( AtomicFormulasOf S) holds (it . (I,phi)) = (I -AtomicEval phi);

      existence

      proof

        set II = (U -InterpretersOf S), AF = ( AtomicFormulasOf S);

        deffunc F( Element of II, Element of AF) = ($1 -AtomicEval $2) qua Element of BOOLEAN ;

        consider f be Function of [:II, AF:], BOOLEAN such that

         A1: for I be Element of II, phi be Element of AF holds (f . (I,phi)) = F(I,phi) from BINOP_1:sch 4;

        take f;

        thus for I be Element of II, phi be Element of AF holds (f . (I,phi)) = (I -AtomicEval phi) by A1;

      end;

      uniqueness

      proof

        set II = (U -InterpretersOf S), AF = ( AtomicFormulasOf S), B = BOOLEAN ;

        let IT1,IT2 be Function of [:II, AF:], B;

        deffunc F( Element of II, Element of AF) = ($1 -AtomicEval $2);

        assume that

         A2: for I be Element of II, phi be Element of AF holds (IT1 . (I,phi)) = F(I,phi) and

         A3: for I be Element of II, phi be Element of AF holds (IT2 . (I,phi)) = F(I,phi);

        now

          let a be Element of II, b be Element of AF;

          

          thus (IT1 . (a,b)) = F(a,b) by A2

          .= (IT2 . (a,b)) by A3;

        end;

        hence IT1 = IT2;

      end;

    end

    definition

      let S, U;

      let I be Element of (U -InterpretersOf S);

      let f be PartFunc of [:(U -InterpretersOf S), ((( AllSymbolsOf S) * ) \ { {} }):], BOOLEAN ;

      let phi be Element of ((( AllSymbolsOf S) * ) \ { {} });

      :: FOMODEL2:def16

      func f -ExFunctor (I,phi) -> Element of BOOLEAN equals

      : Def15: TRUE if ex u be Element of U, v be literal Element of S st ((phi . 1) = v & (f . (((v,u) ReassignIn I),(phi /^ 1))) = TRUE )

      otherwise FALSE ;

      coherence ;

      consistency ;

    end

    definition

      let S, U;

      let g be Element of ( PFuncs ( [:(U -InterpretersOf S), ((( AllSymbolsOf S) * ) \ { {} }):], BOOLEAN ));

      :: FOMODEL2:def17

      func ExIterator (g) -> PartFunc of [:(U -InterpretersOf S), ((( AllSymbolsOf S) * ) \ { {} }):], BOOLEAN means

      : Def16: (for x be Element of (U -InterpretersOf S), y be Element of ((( AllSymbolsOf S) * ) \ { {} }) holds ( [x, y] in ( dom it ) iff (ex v be literal Element of S, w be string of S st [x, w] in ( dom g) & y = ( <*v*> ^ w)))) & (for x be Element of (U -InterpretersOf S), y be Element of ((( AllSymbolsOf S) * ) \ { {} }) st [x, y] in ( dom it ) holds (it . (x,y)) = (g -ExFunctor (x,y)));

      existence

      proof

        set SS = ( AllSymbolsOf S), II = (U -InterpretersOf S), Strings = ((SS * ) \ { {} });

        deffunc F( Element of II, Element of Strings) = (g -ExFunctor ($1,$2));

        defpred P[ Element of II, Element of Strings] means ex v be literal Element of S, w be string of S st [$1, w] in ( dom g) & $2 = ( <*v*> ^ w);

        

         A1: for x be Element of II, y be Element of Strings st P[x, y] holds F(x,y) in BOOLEAN ;

        consider f be PartFunc of [:II, Strings:], BOOLEAN such that

         A2: (for x be Element of II, y be Element of Strings holds ( [x, y] in ( dom f) iff P[x, y])) & (for x be Element of II, y be Element of Strings st [x, y] in ( dom f) holds (f . (x,y)) = F(x,y)) from BINOP_1:sch 8( A1);

        take f;

        thus thesis by A2;

      end;

      uniqueness

      proof

        set SS = ( AllSymbolsOf S), II = (U -InterpretersOf S), Strings = ((SS * ) \ { {} }), D = [:II, Strings:];

        let IT1,IT2 be PartFunc of D, BOOLEAN ;

        defpred P[ Element of II, Element of Strings] means ex v be literal Element of S, w be string of S st [$1, w] in ( dom g) & $2 = ( <*v*> ^ w);

        assume that

         A3: (for x be Element of II, y be Element of Strings holds ( [x, y] in ( dom IT1) iff P[x, y])) and

         A4: (for x be Element of II, y be Element of Strings st [x, y] in ( dom IT1) holds (IT1 . (x,y)) = (g -ExFunctor (x,y)));

        assume that

         A5: (for x be Element of II, y be Element of Strings holds ( [x, y] in ( dom IT2) iff P[x, y])) and

         A6: (for x be Element of II, y be Element of Strings st [x, y] in ( dom IT2) holds (IT2 . (x,y)) = (g -ExFunctor (x,y)));

         A7:

        now

          let x be object;

          assume

           A8: x in ( dom IT1);

          then

          reconsider xx = x as Element of D;

          consider x1,x2 be object such that

           A9: x1 in II & x2 in Strings & xx = [x1, x2] by ZFMISC_1:def 2;

          reconsider I = x1 as Element of II by A9;

          reconsider phi = x2 as Element of Strings by A9;

           P[I, phi] by A3, A8, A9;

          hence x in ( dom IT2) by A5, A9;

        end;

        then

         A10: ( dom IT1) c= ( dom IT2);

        now

          let x be object;

          assume

           A11: x in ( dom IT2);

          then

          reconsider xx = x as Element of D;

          consider x1,x2 be object such that

           A12: x1 in II & x2 in Strings & xx = [x1, x2] by ZFMISC_1:def 2;

          reconsider I = x1 as Element of II by A12;

          reconsider phi = x2 as Element of Strings by A12;

           P[I, phi] by A5, A11, A12;

          hence x in ( dom IT1) by A3, A12;

        end;

        then

         A13: ( dom IT2) c= ( dom IT1);

        now

          let x be object;

          assume

           A14: x in ( dom IT1);

          then

          reconsider xx = x as Element of D;

          consider x1,x2 be object such that

           A15: x1 in II & x2 in Strings & xx = [x1, x2] by ZFMISC_1:def 2;

          reconsider I = x1 as Element of II by A15;

          reconsider phi = x2 as Element of Strings by A15;

          (IT1 . x) = (IT1 . (I,phi)) by A15

          .= (g -ExFunctor (I,phi)) by A4, A15, A14

          .= (IT2 . (I,phi)) by A6, A15, A14, A7

          .= (IT2 . x) by A15;

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

        end;

        hence thesis by FUNCT_1: 2, A13, A10, XBOOLE_0:def 10;

      end;

    end

    definition

      let S, U;

      let f be PartFunc of [:(U -InterpretersOf S), ((( AllSymbolsOf S) * ) \ { {} }):], BOOLEAN ;

      let I be Element of (U -InterpretersOf S);

      let phi be Element of ((( AllSymbolsOf S) * ) \ { {} });

      :: FOMODEL2:def18

      func f -NorFunctor (I,phi) -> Element of BOOLEAN equals

      : Def17: TRUE if ex w1,w2 be Element of ((( AllSymbolsOf S) * ) \ { {} }) st ( [I, w1] in ( dom f) & (f . (I,w1)) = FALSE & (f . (I,w2)) = FALSE & phi = (( <*( TheNorSymbOf S)*> ^ w1) ^ w2))

      otherwise FALSE ;

      coherence ;

      consistency ;

    end

    definition

      let S, U;

      let g be Element of ( PFuncs ( [:(U -InterpretersOf S), ((( AllSymbolsOf S) * ) \ { {} }):], BOOLEAN ));

      :: FOMODEL2:def19

      func NorIterator (g) -> PartFunc of [:(U -InterpretersOf S), ((( AllSymbolsOf S) * ) \ { {} }):], BOOLEAN means

      : Def18: (for x be Element of (U -InterpretersOf S), y be Element of ((( AllSymbolsOf S) * ) \ { {} }) holds ( [x, y] in ( dom it ) iff (ex phi1,phi2 be Element of ((( AllSymbolsOf S) * ) \ { {} }) st (y = (( <*( TheNorSymbOf S)*> ^ phi1) ^ phi2) & [x, phi1] in ( dom g) & [x, phi2] in ( dom g))))) & (for x be Element of (U -InterpretersOf S), y be Element of ((( AllSymbolsOf S) * ) \ { {} }) st [x, y] in ( dom it ) holds (it . (x,y)) = (g -NorFunctor (x,y)));

      existence

      proof

        set SS = ( AllSymbolsOf S), II = (U -InterpretersOf S), Strings = ((SS * ) \ { {} });

        reconsider g as PartFunc of [:II, Strings:], BOOLEAN ;

        deffunc F( Element of II, Element of Strings) = (g -NorFunctor ($1,$2));

        defpred P[ Element of II, Element of Strings] means ex phi1,phi2 be Element of ((( AllSymbolsOf S) * ) \ { {} }) st ($2 = (( <*( TheNorSymbOf S)*> ^ phi1) ^ phi2) & [$1, phi1] in ( dom g) & [$1, phi2] in ( dom g));

        

         A1: for x be Element of II, y be Element of Strings st P[x, y] holds F(x,y) in BOOLEAN ;

        consider f be PartFunc of [:II, Strings:], BOOLEAN such that

         A2: (for x be Element of II, y be Element of Strings holds ( [x, y] in ( dom f) iff P[x, y])) & (for x be Element of II, y be Element of Strings st [x, y] in ( dom f) holds (f . (x,y)) = F(x,y)) from BINOP_1:sch 8( A1);

        take f;

        thus thesis by A2;

      end;

      uniqueness

      proof

        set SS = ( AllSymbolsOf S), II = (U -InterpretersOf S), Strings = ((SS * ) \ { {} }), D = [:II, Strings:];

        deffunc F( Element of II, Element of Strings) = (g -NorFunctor ($1,$2));

        defpred P[ Element of II, Element of Strings] means ex phi1,phi2 be Element of ((( AllSymbolsOf S) * ) \ { {} }) st ($2 = (( <*( TheNorSymbOf S)*> ^ phi1) ^ phi2) & [$1, phi1] in ( dom g) & [$1, phi2] in ( dom g));

        let IT1,IT2 be PartFunc of D, BOOLEAN ;

        assume that

         A3: (for x be Element of II, y be Element of Strings holds ( [x, y] in ( dom IT1) iff P[x, y])) and

         A4: (for x be Element of II, y be Element of Strings st [x, y] in ( dom IT1) holds (IT1 . (x,y)) = F(x,y));

        assume that

         A5: (for x be Element of II, y be Element of Strings holds ( [x, y] in ( dom IT2) iff P[x, y])) and

         A6: (for x be Element of II, y be Element of Strings st [x, y] in ( dom IT2) holds (IT2 . (x,y)) = F(x,y));

         A7:

        now

          let x be object;

          assume

           A8: x in ( dom IT1);

          then

          reconsider xx = x as Element of D;

          consider x1,x2 be object such that

           A9: x1 in II & x2 in Strings & xx = [x1, x2] by ZFMISC_1:def 2;

          reconsider I = x1 as Element of II by A9;

          reconsider phi = x2 as Element of Strings by A9;

           P[I, phi] by A3, A8, A9;

          hence x in ( dom IT2) by A5, A9;

        end;

        then

         A10: ( dom IT1) c= ( dom IT2);

        now

          let x be object;

          assume

           A11: x in ( dom IT2);

          then

          reconsider xx = x as Element of D;

          consider x1,x2 be object such that

           A12: x1 in II & x2 in Strings & xx = [x1, x2] by ZFMISC_1:def 2;

          reconsider I = x1 as Element of II by A12;

          reconsider phi = x2 as Element of Strings by A12;

           P[I, phi] by A5, A11, A12;

          hence x in ( dom IT1) by A3, A12;

        end;

        then

         A13: ( dom IT2) c= ( dom IT1);

        now

          let x be object;

          assume

           A14: x in ( dom IT1);

          then

          reconsider xx = x as Element of D;

          consider x1,x2 be object such that

           A15: x1 in II & x2 in Strings & xx = [x1, x2] by ZFMISC_1:def 2;

          reconsider I = x1 as Element of II by A15;

          reconsider phi = x2 as Element of Strings by A15;

          (IT1 . x) = (IT1 . (I,phi)) by A15

          .= F(I,phi) by A4, A15, A14

          .= (IT2 . (I,phi)) by A6, A15, A14, A7

          .= (IT2 . x) by A15;

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

        end;

        hence thesis by FUNCT_1: 2, A10, XBOOLE_0:def 10, A13;

      end;

    end

    definition

      let S, U;

      :: FOMODEL2:def20

      func (S,U) -TruthEval -> sequence of ( PFuncs ( [:(U -InterpretersOf S), ((( AllSymbolsOf S) * ) \ { {} }):], BOOLEAN )) means

      : Def19: (it . 0 ) = (S -TruthEval U) & for mm holds (it . (mm + 1)) = ((( ExIterator (it . mm)) +* ( NorIterator (it . mm))) +* (it . mm));

      existence

      proof

        set SS = ( AllSymbolsOf S), II = (U -InterpretersOf S), AF = ( AtomicFormulasOf S), Strings = ((SS * ) \ { {} }), D = [:II, Strings:];

        reconsider ii = II as Subset of II by XBOOLE_0:def 10;

        reconsider subboolean = BOOLEAN as Subset of BOOLEAN by XBOOLE_0:def 10;

        reconsider sub = [:ii, AF:] as Subset of D;

         [:sub, subboolean:] c= [:D, BOOLEAN :];

        then (S -TruthEval U) is PartFunc of D, BOOLEAN by XBOOLE_1: 1;

        then

        reconsider Z = (S -TruthEval U) as Element of ( PFuncs (D, BOOLEAN )) by PARTFUN1: 45;

        deffunc F( Element of ( PFuncs (D, BOOLEAN ))) = ((( ExIterator $1) +* ( NorIterator $1)) +* $1);

        defpred P[ set, Element of ( PFuncs (D, BOOLEAN )), set] means $3 = F($2);

        

         A1: for n be Nat holds for x be Element of ( PFuncs (D, BOOLEAN )) holds ex y be Element of ( PFuncs (D, BOOLEAN )) st P[n, x, y]

        proof

          let n be Nat, x be Element of ( PFuncs (D, BOOLEAN ));

          reconsider yy = F(x) as Element of ( PFuncs (D, BOOLEAN )) by PARTFUN1: 45;

          take y = yy;

          thus thesis;

        end;

        consider f be sequence of ( PFuncs (D, BOOLEAN )) such that

         A2: (f . 0 ) = Z & for n be Nat holds P[n, (f . n) qua Element of ( PFuncs (D, BOOLEAN )), (f . (n + 1))] from RECDEF_1:sch 2( A1);

        take f;

        thus (f . 0 ) = (S -TruthEval U) by A2;

        thus for mm holds (f . (mm + 1)) = ((( ExIterator (f . mm)) +* ( NorIterator (f . mm))) +* (f . mm)) by A2;

      end;

      uniqueness

      proof

        set SS = ( AllSymbolsOf S), II = (U -InterpretersOf S), AF = ( AtomicFormulasOf S), Strings = ((SS * ) \ { {} }), D = [:II, Strings:], Z = (S -TruthEval U);

         [:II, AF:] c= D & BOOLEAN c= BOOLEAN by ZFMISC_1: 96;

        then ( dom Z) c= D & ( rng Z) c= BOOLEAN ;

        then Z is Relation of D, BOOLEAN by RELSET_1: 4;

        then

        reconsider ZZ = Z as Element of ( PFuncs (D, BOOLEAN )) by PARTFUN1: 45;

        deffunc RecFun( set, Element of ( PFuncs (D, BOOLEAN ))) = ((( ExIterator $2) +* ( NorIterator $2)) +* $2);

        defpred P[ set, set, set] means for f be Element of ( PFuncs (D, BOOLEAN )) st $2 = f holds $3 = RecFun($1,f);

        let IT1,IT2 be sequence of ( PFuncs (D, BOOLEAN ));

        assume

         A3: (IT1 . 0 ) = Z & for mm holds (IT1 . (mm + 1)) = ((( ExIterator (IT1 . mm)) +* ( NorIterator (IT1 . mm))) +* (IT1 . mm));

        assume

         A4: (IT2 . 0 ) = Z & for mm holds (IT2 . (mm + 1)) = ((( ExIterator (IT2 . mm)) +* ( NorIterator (IT2 . mm))) +* (IT2 . mm));

        

         A5: (IT1 . 0 ) = ZZ by A3;

        

         A6: for m holds P[m, (IT1 . m), (IT1 . (m + 1))]

        proof

          let m;

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

          let f be Element of ( PFuncs (D, BOOLEAN ));

          assume f = (IT1 . m);

          then (IT1 . (mm + 1)) = RecFun(m,f) by A3;

          hence thesis;

        end;

        

         A7: (IT2 . 0 ) = ZZ by A4;

        

         A8: for m holds P[m, (IT2 . m), (IT2 . (m + 1))]

        proof

          let m;

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

          let f be Element of ( PFuncs (D, BOOLEAN ));

          assume f = (IT2 . m);

          then (IT2 . (mm + 1)) = RecFun(m,f) by A4;

          hence thesis;

        end;

        

         A9: for n be Nat, x,y1,y2 be Element of ( PFuncs (D, BOOLEAN )) st P[n, x, y1] & P[n, x, y2] holds y1 = y2

        proof

          let n be Nat, x,y1,y2 be Element of ( PFuncs (D, BOOLEAN ));

          assume that

           A10: P[n, x, y1] and

           A11: P[n, x, y2];

          

           A12: y2 = RecFun(n,x) by A11;

          thus thesis by A10, A12;

        end;

        thus thesis from NAT_1:sch 14( A5, A6, A7, A8, A9);

      end;

    end

    theorem :: FOMODEL2:2

    

     Th2: for I be S, U -interpreter-like Function holds (I | ( OwnSymbolsOf S)) in (U -InterpretersOf S)

    proof

      let I be S, U -interpreter-like Function;

      set O = ( OwnSymbolsOf S), C = ( PFuncs ((U * ),(U \/ BOOLEAN )));

      ( dom (I | O)) c= O & ( rng (I | O)) c= C;

      then (I | O) is Function of O, C by RELSET_1: 4;

      then (I | O) is S, U -interpreter-like & (I | O) is Element of ( Funcs (O,C)) by FUNCT_2: 8;

      hence thesis;

    end;

    definition

      let S be Language, m be Nat, U be non empty set;

      :: FOMODEL2:def21

      func (S,U) -TruthEval m -> Element of ( PFuncs ( [:(U -InterpretersOf S), ((( AllSymbolsOf S) * ) \ { {} }):], BOOLEAN )) means

      : Def20: for mm st m = mm holds it = (((S,U) -TruthEval ) . mm);

      existence

      proof

        set f = ((S,U) -TruthEval );

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

        take (f . nn);

        let mm;

        assume m = mm;

        hence (f . nn) = (f . mm);

      end;

      uniqueness

      proof

        set II = (U -InterpretersOf S), SS = ( AllSymbolsOf S), f = ((S,U) -TruthEval );

        let IT1,IT2 be Element of ( PFuncs ( [:II, ((SS * ) \ { {} }):], BOOLEAN ));

        assume that

         A1: for mm st m = mm holds IT1 = (((S,U) -TruthEval ) . mm) and

         A2: for mm st m = mm holds IT2 = (((S,U) -TruthEval ) . mm);

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

        

        thus IT1 = (f . mm) by A1

        .= IT2 by A2;

      end;

    end

    

     Lm7: for n holds x in ( dom ((S,U) -TruthEval m)) implies (x in ( dom ((S,U) -TruthEval (m + n))) & (((S,U) -TruthEval m) . x) = (((S,U) -TruthEval (m + n)) . x))

    proof

      set f = ((S,U) -TruthEval );

      defpred P[ Nat] means x in ( dom ((S,U) -TruthEval m)) implies (x in ( dom ((S,U) -TruthEval (m + $1))) & (((S,U) -TruthEval m) . x) = (((S,U) -TruthEval (m + $1)) . x));

      

       A1: P[ 0 ];

      

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

      proof

        let n;

        reconsider k = (m + n), K = ((m + n) + 1) as Element of NAT by ORDINAL1:def 12;

        assume

         A3: P[n];

        set g = ((S,U) -TruthEval m), g0 = ((S,U) -TruthEval (m + n)), g1 = ((S,U) -TruthEval ((m + n) + 1));

        

         A4: (f . k) = g0 & (f . K) = g1 by Def20;

        

         A5: (f . K) = ((( ExIterator (f . k)) +* ( NorIterator (f . k))) +* (f . k)) by Def19;

        then ( dom (f . K)) = (( dom (( ExIterator (f . k)) +* ( NorIterator (f . k)))) \/ ( dom (f . k))) by FUNCT_4:def 1;

        then

         A6: ( dom (f . k)) c= ( dom (f . K)) by XBOOLE_1: 7;

        assume

         A7: x in ( dom g);

        then x in ( dom (f . k)) by A3, Def20;

        then

         A8: x in ( dom (f . K)) by A6;

        thus x in ( dom ((S,U) -TruthEval (m + (n + 1)))) by A4, A7, A3, A6;

        x in (( dom (( ExIterator (f . k)) +* ( NorIterator (f . k)))) \/ ( dom (f . k))) by FUNCT_4:def 1, A8, A5;

        hence thesis by A3, A4, A7, A5, FUNCT_4:def 1;

      end;

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

    end;

    

     Lm8: x in ((X \/ Y) \/ Z) iff x in X or x in Y or x in Z

    proof

      set W = ((X \/ Y) \/ Z);

      x in W iff (x in (X \/ Y)) or x in Z by XBOOLE_0:def 3;

      hence thesis by XBOOLE_0:def 3;

    end;

    

     Lm9: for m holds for I1 be Element of (U1 -InterpretersOf S), I2 be Element of (U2 -InterpretersOf S), w be string of S holds ( [I1, w] in ( dom ((S,U1) -TruthEval m)) implies [I2, w] in ( dom ((S,U2) -TruthEval m)))

    proof

      set SS = ( AllSymbolsOf S), N = ( TheNorSymbOf S), II1 = (U1 -InterpretersOf S), II2 = (U2 -InterpretersOf S), AF = ( AtomicFormulasOf S);

      defpred P[ Nat] means for I1 be Element of II1, I2 be Element of II2, w be string of S holds ( [I1, w] in ( dom ((S,U1) -TruthEval $1)) implies [I2, w] in ( dom ((S,U2) -TruthEval $1)));

      

       A1: P[ 0 ]

      proof

        set f1 = ((S,U1) -TruthEval 0 ), f2 = ((S,U2) -TruthEval 0 );

        reconsider Z = 0 as Element of NAT ;

        reconsider g1 = (((S,U1) -TruthEval ) . Z) as Element of ( PFuncs ( [:II1, ((SS * ) \ { {} }):], BOOLEAN ));

        reconsider g2 = (((S,U2) -TruthEval ) . Z) as Element of ( PFuncs ( [:II2, ((SS * ) \ { {} }):], BOOLEAN ));

        

         A2: f1 = g1 & f2 = g2 by Def20;

        

         A3: g1 = (S -TruthEval U1) & g2 = (S -TruthEval U2) by Def19;

        

         A4: ( dom f1) = [:II1, AF:] by A2, FUNCT_2:def 1, A3;

        

         A5: ( dom f2) = [:II2, AF:] by A2, FUNCT_2:def 1, A3;

        let I1 be Element of II1, I2 be Element of II2;

        let w;

        assume [I1, w] in ( dom f1);

        then I1 in II1 & w in AF by ZFMISC_1: 87, A4;

        hence [I2, w] in ( dom f2) by A5, ZFMISC_1: 87;

      end;

      

       A6: 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

         A7: P[n];

        let I1 be Element of II1, I2 be Element of II2;

        set f1n = ((S,U1) -TruthEval n), f1N = ((S,U1) -TruthEval (n + 1)), f2n = ((S,U2) -TruthEval n), f2N = ((S,U2) -TruthEval (n + 1));

        

         A8: ( dom f1N) = ((( dom ( ExIterator f1n)) \/ ( dom ( NorIterator f1n))) \/ ( dom f1n))

        proof

          reconsider g1N = (((S,U1) -TruthEval ) . NN) as Element of ( PFuncs ( [:II1, ((SS * ) \ { {} }):], BOOLEAN ));

          reconsider g1n = (((S,U1) -TruthEval ) . nn) as Element of ( PFuncs ( [:II1, ((SS * ) \ { {} }):], BOOLEAN ));

          

           A9: f1n = g1n & f1N = g1N by Def20;

          then f1N = ((( ExIterator g1n) +* ( NorIterator g1n)) +* g1n) by Def19;

          

          then ( dom f1N) = (( dom (( ExIterator g1n) +* ( NorIterator g1n))) \/ ( dom g1n)) by FUNCT_4:def 1

          .= ((( dom ( ExIterator g1n)) \/ ( dom ( NorIterator g1n))) \/ ( dom g1n)) by FUNCT_4:def 1;

          hence thesis by A9;

        end;

        

         A10: ( dom f2N) = ((( dom ( ExIterator f2n)) \/ ( dom ( NorIterator f2n))) \/ ( dom f2n))

        proof

          reconsider g2N = (((S,U2) -TruthEval ) . NN) as Element of ( PFuncs ( [:II2, ((SS * ) \ { {} }):], BOOLEAN ));

          reconsider g2n = (((S,U2) -TruthEval ) . nn) as Element of ( PFuncs ( [:II2, ((SS * ) \ { {} }):], BOOLEAN ));

          

           A11: f2n = g2n & f2N = g2N by Def20;

          then f2N = ((( ExIterator g2n) +* ( NorIterator g2n)) +* g2n) by Def19;

          

          then ( dom f2N) = (( dom (( ExIterator g2n) +* ( NorIterator g2n))) \/ ( dom g2n)) by FUNCT_4:def 1

          .= ((( dom ( ExIterator g2n)) \/ ( dom ( NorIterator g2n))) \/ ( dom g2n)) by FUNCT_4:def 1;

          hence thesis by A11;

        end;

        let w;

        set x = [I1, w];

        assume

         A12: x in ( dom f1N);

        per cases by A12, Lm8, A8;

          suppose x in ( dom ( ExIterator f1n));

          then

          consider v be literal Element of S, ww be string of S such that

           A13: [I1, ww] in ( dom f1n) & w = ( <*v*> ^ ww) by Def16;

           [I2, ww] in ( dom f2n) & w = ( <*v*> ^ ww) by A13, A7;

          then [I2, w] in ( dom ( ExIterator f2n)) by Def16;

          hence [I2, w] in ( dom f2N) by Lm8, A10;

        end;

          suppose x in ( dom ( NorIterator f1n));

          then

          consider phi1,phi2 be string of S such that

           A14: (w = (( <*( TheNorSymbOf S)*> ^ phi1) ^ phi2) & [I1, phi1] in ( dom f1n) & [I1, phi2] in ( dom f1n)) by Def18;

          w = (( <*N*> ^ phi1) ^ phi2) & [I2, phi1] in ( dom f2n) & [I2, phi2] in ( dom f2n) by A14, A7;

          then [I2, w] in ( dom ( NorIterator f2n)) by Def18;

          hence thesis by Lm8, A10;

        end;

          suppose x in ( dom f1n);

          then [I2, w] in ( dom f2n) by A7;

          hence thesis by Lm8, A10;

        end;

      end;

      thus for m holds P[m] from NAT_1:sch 2( A1, A6);

    end;

    

     Lm10: ( curry (((S,U) -TruthEval ) . mm)) is Function of (U -InterpretersOf S), ( PFuncs (((( AllSymbolsOf S) * ) \ { {} }), BOOLEAN ))

    proof

      set II = (U -InterpretersOf S), AF = ( AtomicFormulasOf S), f = (((S,U) -TruthEval ) . mm), SS = ( AllSymbolsOf S), F = ((S,U) -TruthEval );

      reconsider g = ( curry f) as Element of ( PFuncs (II,( PFuncs (((SS * ) \ { {} }), BOOLEAN )))) by FUNCT_6: 14;

      set y = the Element of AF;

      reconsider Z = 0 as Element of NAT ;

      ( dom (S -TruthEval U)) = [:II, AF:] by FUNCT_2:def 1;

      then

       A1: ( dom (F . 0 )) = [:II, AF:] by Def19;

      now

        let x be object;

        assume x in II;

        then [x, y] in ( dom (F . 0 )) by A1, ZFMISC_1: 87;

        then [x, y] in ( dom ((S,U) -TruthEval 0 )) by Def20;

        then [x, y] in ( dom ((S,U) -TruthEval ( 0 + mm))) by Lm7;

        then [x, y] in ( dom f) by Def20;

        hence x in ( dom g) by FUNCT_5: 19;

      end;

      then II c= ( dom g) & ( dom g) c= II;

      then

      reconsider gg = g as total PartFunc of II, ( PFuncs (((SS * ) \ { {} }), BOOLEAN )) by XBOOLE_0:def 10, PARTFUN1:def 2;

      ( curry f) = gg;

      hence thesis;

    end;

    

     Lm11: ( curry ((S,U) -TruthEval m)) is Function of (U -InterpretersOf S), ( PFuncs (((( AllSymbolsOf S) * ) \ { {} }), BOOLEAN ))

    proof

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

      set f = ((S,U) -TruthEval mm), g = (((S,U) -TruthEval ) . mm);

      ( curry f) = ( curry g) by Def20;

      hence thesis by Lm10;

    end;

    definition

      let S, U, m;

      let I be Element of (U -InterpretersOf S);

      :: FOMODEL2:def22

      func (I,m) -TruthEval -> Element of ( PFuncs (((( AllSymbolsOf S) * ) \ { {} }), BOOLEAN )) equals (( curry ((S,U) -TruthEval m)) . I);

      coherence

      proof

        set II = (U -InterpretersOf S), SS = ( AllSymbolsOf S);

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

        ( curry ((S,U) -TruthEval mm)) = ( curry (((S,U) -TruthEval ) . mm)) by Def20;

        then

        reconsider f = ( curry ((S,U) -TruthEval mm)) as Function of II, ( PFuncs (((SS * ) \ { {} }), BOOLEAN )) by Lm10;

        (f . I) is Element of ( PFuncs (((SS * ) \ { {} }), BOOLEAN ));

        hence thesis;

      end;

    end

    

     Lm12: for I be Element of (U -InterpretersOf S) holds ((I,m) -TruthEval ) c= ((I,(m + n)) -TruthEval )

    proof

      set UI = (U -InterpretersOf S), SS = ( AllSymbolsOf S);

      let I be Element of UI;

      set IT1 = ((I,m) -TruthEval ), IT2 = ((I,(m + n)) -TruthEval ), f = ((S,U) -TruthEval m), g = ((S,U) -TruthEval (m + n));

      reconsider F = ( curry f), G = ( curry g) as Function of UI, ( PFuncs (((SS * ) \ { {} }), BOOLEAN )) by Lm11;

      

       A1: IT1 = (F . I) & IT2 = (G . I) & ( dom F) = UI by FUNCT_2:def 1;

      

       A2: for x st x in ( dom IT1) holds (x in ( dom IT2) & (IT1 . x) = (IT2 . x))

      proof

        let x;

        assume

         A3: x in ( dom IT1);

        then

         A4: [I, x] in ( dom f) by A1, FUNCT_5: 31;

        then

         A5: [I, x] in ( dom g) & (g . [I, x]) = (f . [I, x]) by Lm7;

        then x in ( dom IT2) & (IT2 . x) = (g . (I,x)) by FUNCT_5: 20;

        

        then (IT2 . x) = (f . (I,x)) by A4, Lm7

        .= (IT1 . x) by A3, FUNCT_5: 31, A1;

        hence x in ( dom IT2) & (IT1 . x) = (IT2 . x) by A5, FUNCT_5: 20;

      end;

      (for x be object st x in ( dom IT1) holds x in ( dom IT2)) & for x be object st x in ( dom IT1) holds (IT1 . x) = (IT2 . x) by A2;

      hence thesis by GRFUNC_1: 2, TARSKI:def 3;

    end;

    

     Lm13: for I1 be Element of (U1 -InterpretersOf S), I2 be Element of (U2 -InterpretersOf S) holds ( dom ((I1,m) -TruthEval )) c= ( dom ((I2,m) -TruthEval ))

    proof

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

      set II1 = (U1 -InterpretersOf S), II2 = (U2 -InterpretersOf S), f = (((S,U1) -TruthEval ) . mm), SS = ( AllSymbolsOf S), ff1 = ((S,U1) -TruthEval mm), ff2 = ((S,U2) -TruthEval mm), g = (((S,U2) -TruthEval ) . mm);

      let I1 be Element of II1, I2 be Element of II2;

      

       A1: f = ff1 & g = ff2 by Def20;

      set F1 = ((I1,m) -TruthEval ), F2 = ((I2,m) -TruthEval );

      

       A2: (( curry f) . I1) = F1 & (( curry g) . I2) = F2 by Def20;

      then

      reconsider f1 = (( curry (((S,U1) -TruthEval ) . mm)) . I1), f2 = (( curry (((S,U2) -TruthEval ) . mm)) . I2) as Element of ( PFuncs (((SS * ) \ { {} }), BOOLEAN ));

      reconsider F = ( curry f) as Function of II1, ( PFuncs (((SS * ) \ { {} }), BOOLEAN )) by Lm10;

      

       A3: I1 in II1;

      f is Element of ( PFuncs ( [:II1, ((SS * ) \ { {} }):], BOOLEAN ));

      then ( dom f) c= [:II1, ((SS * ) \ { {} }):] by RELAT_1:def 18;

      then

       A4: ( uncurry F) = f by FUNCT_5: 50;

      now

        let ww be object;

        assume

         A5: ww in ( dom f1);

        then

        reconsider w = ww as Element of ((SS * ) \ { {} });

        I1 in ( dom F) & f1 = (F . I1) & ww in ( dom f1) by A3, FUNCT_2:def 1, A5;

        then [I1, w] in ( dom ff1) by A1, A4, FUNCT_5: 38;

        then [I2, ww] in ( dom g) by A1, Lm9;

        hence ww in ( dom f2) by FUNCT_5: 20;

      end;

      hence thesis by A2;

    end;

    

     Lm14: for I1 be Element of (U1 -InterpretersOf S), I2 be Element of (U2 -InterpretersOf S) holds ( dom ((I1,mm) -TruthEval )) = ( dom ((I2,mm) -TruthEval )) by Lm13;

    definition

      let S;

      let m be natural Number;

      :: FOMODEL2:def23

      func S -formulasOfMaxDepth m -> Subset of ((( AllSymbolsOf S) * ) \ { {} }) means

      : Def22: for U be non empty set, I be Element of (U -InterpretersOf S), mm be Element of NAT st m = mm holds it = ( dom ((I,mm) -TruthEval ));

      existence

      proof

        set SS = ( AllSymbolsOf S);

        set UU = the non empty set, II = the Element of (UU -InterpretersOf S);

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

        reconsider IT = ( dom ((II,nn) -TruthEval )) as Subset of ((SS * ) \ { {} });

        take IT;

        let U;

        set III = (U -InterpretersOf S);

        let I be Element of III;

        let mm;

        assume m = mm;

        hence IT = ( dom ((I,mm) -TruthEval )) by Lm14;

      end;

      uniqueness

      proof

        set SS = ( AllSymbolsOf S);

        let IT1,IT2 be Subset of ((SS * ) \ { {} });

        assume that

         A1: for U be non empty set, I be Element of (U -InterpretersOf S), mm be Element of NAT st m = mm holds IT1 = ( dom ((I,mm) -TruthEval )) and

         A2: for U be non empty set, I be Element of (U -InterpretersOf S), mm be Element of NAT st m = mm holds IT2 = ( dom ((I,mm) -TruthEval ));

        set U = the non empty set, I = the Element of (U -InterpretersOf S);

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

        

        thus IT1 = ( dom ((I,nn) -TruthEval )) by A1

        .= IT2 by A2;

      end;

    end

    

     Lm15: (S -formulasOfMaxDepth m) c= (S -formulasOfMaxDepth (m + n))

    proof

      set U = the non empty set;

      set X = (S -formulasOfMaxDepth m), Y = (S -formulasOfMaxDepth (m + n)), II = (U -InterpretersOf S);

      set I = the Element of II;

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

      set f = ((I,mm) -TruthEval ), g = ((I,NN) -TruthEval );

      

       A1: X = ( dom f) & Y = ( dom g) by Def22;

      f c= g by Lm12;

      hence thesis by GRFUNC_1: 2, A1;

    end;

    

     Lm16: (S -formulasOfMaxDepth 0 ) = ( AtomicFormulasOf S)

    proof

      set U = the non empty set, AF = ( AtomicFormulasOf S), II = (U -InterpretersOf S), I = the Element of II;

      reconsider z = 0 as Element of NAT ;

      

       A1: [:II, AF:] = ( dom (S -TruthEval U)) by FUNCT_2:def 1

      .= ( dom (((S,U) -TruthEval ) . z)) by Def19

      .= ( dom ((S,U) -TruthEval 0 )) by Def20;

      now

        let x be object;

        assume x in AF;

        then [I, x] in ( dom ((S,U) -TruthEval 0 )) by A1, ZFMISC_1:def 2;

        then x in ( dom ((I,z) -TruthEval )) by FUNCT_5: 20;

        hence x in (S -formulasOfMaxDepth 0 ) by Def22;

      end;

      then

       A2: AF c= (S -formulasOfMaxDepth 0 );

      now

        let x be object;

        assume x in (S -formulasOfMaxDepth 0 );

        then

         A3: x in ( dom ((I,z) -TruthEval )) by Def22;

        set f = ((S,U) -TruthEval z), g = ((I,z) -TruthEval );

        f = (((S,U) -TruthEval ) . z) by Def20;

        then

        reconsider gg = ( curry f) as Function of II, ( PFuncs (((( AllSymbolsOf S) * ) \ { {} }), BOOLEAN )) by Lm10;

        ( dom gg) = II by FUNCT_2:def 1;

        then [I, x] in [:II, AF:] by A1, A3, FUNCT_5: 31;

        then ( [I, x] `2 ) in AF by MCART_1: 10;

        hence x in AF;

      end;

      then (S -formulasOfMaxDepth 0 ) c= AF;

      hence thesis by A2;

    end;

    definition

      let S;

      let m be natural Number;

      let w;

      :: FOMODEL2:def24

      attr w is m -wff means

      : Def23: w in (S -formulasOfMaxDepth m);

    end

    definition

      let S, w;

      :: FOMODEL2:def25

      attr w is wff means

      : Def24: ex m st w is m -wff;

    end

    registration

      let S;

      cluster 0 -wff -> 0wff for string of S;

      coherence

      proof

        set AF = ( AtomicFormulasOf S), Z = (S -formulasOfMaxDepth 0 );

        let w be string of S;

        assume w is 0 -wff;

        then w in Z;

        then w in AF by Lm16;

        hence thesis;

      end;

      cluster 0wff -> 0 -wff for string of S;

      coherence

      proof

        set AF = ( AtomicFormulasOf S);

        let w be string of S;

        assume w is 0wff;

        then w in AF;

        then w in (S -formulasOfMaxDepth 0 ) by Lm16;

        hence thesis;

      end;

      let m;

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

      coherence ;

      let n;

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

      coherence

      proof

        set X = (S -formulasOfMaxDepth m), Y = (S -formulasOfMaxDepth (m + n));

        

         A1: X c= Y by Lm15;

        let w;

        assume w is (m + ( 0 * n)) -wff;

        then w in X;

        hence thesis by A1;

      end;

    end

    registration

      let S;

      let m be natural Number;

      cluster m -wff for string of S;

      existence

      proof

        reconsider m as Nat by TARSKI: 1;

        set w = the 0wff string of S;

        w is ( 0 + ( 0 * m)) -wff;

        then w is ( 0 + m) -wff;

        hence thesis;

      end;

    end

    registration

      let S;

      let m be natural Number;

      cluster (S -formulasOfMaxDepth m) -> non empty;

      coherence

      proof

        set X = (S -formulasOfMaxDepth m), phi = the m -wff string of S;

        phi in X by Def23;

        hence thesis;

      end;

    end

    registration

      let S;

      cluster wff for string of S;

      existence

      proof

        take the 0 -wff string of S;

        thus thesis;

      end;

    end

    definition

      let S, U;

      let I be Element of (U -InterpretersOf S), w be wff string of S;

      :: FOMODEL2:def26

      func I -TruthEval w -> Element of BOOLEAN means

      : Def25: for m be Nat st w is m -wff holds it = (((I,m) -TruthEval ) . w);

      existence

      proof

        set IU = (U -InterpretersOf S), SS = ( AllSymbolsOf S), III = I, II = I;

        consider n such that

         A1: w is n -wff by Def24;

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

        set fn = ((III,n) -TruthEval );

        reconsider ww = w as n -wff string of S by A1;

        

         A2: (S -formulasOfMaxDepth nn) = ( dom ((III,nn) -TruthEval )) by Def22;

        (fn . ww) = (fn /. ww) by A2, Def23, PARTFUN1:def 6;

        then

        reconsider IT = (fn . ww) as Element of BOOLEAN ;

        take IT;

        let m;

        set fm = ((II,m) -TruthEval ), f = ((II,(m + n)) -TruthEval ), g = ((III,(n + m)) -TruthEval );

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

        

         A3: (S -formulasOfMaxDepth m) = ( dom ((II,mm) -TruthEval )) & (S -formulasOfMaxDepth nn) = ( dom ((III,nn) -TruthEval )) by Def22;

        

         A4: fm c= f & fn c= g & f = g by Lm12;

        assume w is m -wff;

        then (fm . w) = (f . w) by A4, A3, GRFUNC_1: 2;

        hence IT = (fm . w) by A2, Def23, A4, GRFUNC_1: 2;

      end;

      uniqueness

      proof

        let IT1,IT2 be Element of BOOLEAN ;

        assume

         A5: for m be Nat st w is m -wff holds IT1 = (((I,m) -TruthEval ) . w);

        assume

         A6: for m be Nat st w is m -wff holds IT2 = (((I,m) -TruthEval ) . w);

        consider m be Nat such that

         A7: w is m -wff by Def24;

        

        thus IT1 = (((I,m) -TruthEval ) . w) by A5, A7

        .= IT2 by A6, A7;

      end;

    end

    definition

      let S;

      :: FOMODEL2:def27

      func AllFormulasOf S -> set equals { w where w be string of S : ex m st w is m -wff };

      coherence ;

    end

    registration

      let S;

      cluster ( AllFormulasOf S) -> non empty;

      coherence

      proof

        set w = the 0 -wff string of S;

        w in ( AllFormulasOf S);

        hence thesis;

      end;

    end

    reserve u,u1,u2 for Element of U,

t for termal string of S,

I for S, U -interpreter-like Function,

l,l1,l2 for literal Element of S,

m1,n1 for non zero Nat,

phi0 for 0wff string of S,

psi,phi,phi1,phi2 for wff string of S;

    theorem :: FOMODEL2:3

    

     Th3: ((((I,u) -TermEval ) . (m + 1)) . t) = ((I . ((S -firstChar ) . t)) . ((((I,u) -TermEval ) . m) * ( SubTerms t))) & (t is 0 -termal implies ((((I,u) -TermEval ) . (m + 1)) . t) = ((I . ((S -firstChar ) . t)) . {} ))

    proof

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

      ((((I,u) -TermEval ) . (mm + 1)) . t) = ((I . ((S -firstChar ) . t)) . ((((I,u) -TermEval ) . mm) * ( SubTerms t))) & (t is 0 -termal implies ((((I,u) -TermEval ) . (mm + 1)) . t) = ((I . ((S -firstChar ) . t)) . {} )) by Lm5;

      hence thesis;

    end;

    theorem :: FOMODEL2:4

    for t be m -termal string of S holds ((((I,u1) -TermEval ) . (m + 1)) . t) = ((((I,u2) -TermEval ) . ((m + 1) + n)) . t) by Lm6;

    theorem :: FOMODEL2:5

    ( curry ((S,U) -TruthEval m)) is Function of (U -InterpretersOf S), ( PFuncs (((( AllSymbolsOf S) * ) \ { {} }), BOOLEAN )) by Lm11;

    theorem :: FOMODEL2:6

    x in ((X \/ Y) \/ Z) iff x in X or x in Y or x in Z by Lm8;

    theorem :: FOMODEL2:7

    (S -formulasOfMaxDepth 0 ) = ( AtomicFormulasOf S) by Lm16;

    definition

      let S, m;

      :: original: -formulasOfMaxDepth

      redefine

      :: FOMODEL2:def28

      func S -formulasOfMaxDepth m means

      : Def27: for U be non empty set, I be Element of (U -InterpretersOf S) holds it = ( dom ((I,m) -TruthEval ));

      compatibility

      proof

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

        set SS = ( AllSymbolsOf S), Phim = (S -formulasOfMaxDepth m);

        defpred P[ set] means for U be non empty set, I be Element of (U -InterpretersOf S) holds $1 = ( dom ((I,m) -TruthEval ));

        let x be Subset of ((SS * ) \ { {} });

        thus x = Phim implies P[x]

        proof

          assume

           A1: x = Phim;

          thus for U be non empty set, I be Element of (U -InterpretersOf S) holds x = ( dom ((I,m) -TruthEval ))

          proof

            let U;

            set II = (U -InterpretersOf S);

            let I be Element of II;

            Phim = ( dom ((I,mm) -TruthEval )) by Def22;

            hence x = ( dom ((I,m) -TruthEval )) by A1;

          end;

        end;

        assume

         A2: P[x];

        for U be non empty set, I be Element of (U -InterpretersOf S), nn be Element of NAT st m = nn holds x = ( dom ((I,nn) -TruthEval )) by A2;

        hence x = Phim by Def22;

      end;

    end

    

     Lm17: ( curry ((S,U) -TruthEval m)) is Function of (U -InterpretersOf S), ( Funcs ((S -formulasOfMaxDepth m), BOOLEAN ))

    proof

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

      set Fm = ((S,U) -TruthEval m), II = (U -InterpretersOf S), SS = ( AllSymbolsOf S), Phim = (S -formulasOfMaxDepth m);

      reconsider f = ( curry Fm) as Function of II, ( PFuncs (((SS * ) \ { {} }), BOOLEAN )) by Lm11;

      

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

      now

        let x be object;

        assume x in II;

        then

        reconsider Ix = x as Element of II;

        reconsider g = (f . Ix) as Element of ( PFuncs (((SS * ) \ { {} }), BOOLEAN ));

        g is BOOLEAN -valued & g = ((Ix,m) -TruthEval );

        then g = g & ( dom g) = Phim & ( rng g) c= BOOLEAN by Def27;

        hence (f . x) in ( Funcs (Phim, BOOLEAN )) by FUNCT_2:def 2;

      end;

      hence thesis by FUNCT_2: 3, A1;

    end;

    theorem :: FOMODEL2:8

    

     Th8: ((S,U) -TruthEval m) in ( Funcs ( [:(U -InterpretersOf S), (S -formulasOfMaxDepth m):], BOOLEAN )) & (((S,U) -TruthEval ) . m) in ( Funcs ( [:(U -InterpretersOf S), (S -formulasOfMaxDepth m):], BOOLEAN ))

    proof

      set Fm = ((S,U) -TruthEval m), II = (U -InterpretersOf S), Phim = (S -formulasOfMaxDepth m), SS = ( AllSymbolsOf S);

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

      reconsider Fmm = Fm as PartFunc of [:II, ((SS * ) \ { {} }):], BOOLEAN ;

      ( dom Fm) c= [:II, ((SS * ) \ { {} }):];

      then

       A1: ( uncurry ( curry Fm)) = Fm by FUNCT_5: 50;

      reconsider f = ( curry Fm) as Function of II, ( Funcs (Phim, BOOLEAN )) by Lm17;

      ( rng f) c= ( Funcs (Phim, BOOLEAN )) & ( dom f) = II by FUNCT_2:def 1;

      then Fm = Fm & ( dom Fm) = [:II, Phim:] & ( rng Fm) c= BOOLEAN by A1, FUNCT_5: 26;

      hence Fm in ( Funcs ( [:II, Phim:], BOOLEAN )) by FUNCT_2:def 2;

      then (((S,U) -TruthEval ) . mm) in ( Funcs ( [:II, Phim:], BOOLEAN )) by Def20;

      hence thesis;

    end;

    definition

      let S, m;

      :: FOMODEL2:def29

      func m -ExFormulasOf S -> set equals the set of all ( <*v*> ^ phi) where v be Element of ( LettersOf S), phi be Element of (S -formulasOfMaxDepth m);

      coherence ;

      :: FOMODEL2:def30

      func m -NorFormulasOf S -> set equals the set of all (( <*( TheNorSymbOf S)*> ^ phi1) ^ phi2) where phi1 be Element of (S -formulasOfMaxDepth m), phi2 be Element of (S -formulasOfMaxDepth m);

      coherence ;

    end

    

     Lm18: ( dom ( NorIterator ((S,U) -TruthEval m))) = [:(U -InterpretersOf S), (m -NorFormulasOf S):]

    proof

      set mm = m, II = (U -InterpretersOf S), SS = ( AllSymbolsOf S), N = ( TheNorSymbOf S), Fm = ((S,U) -TruthEval mm), Phim = (S -formulasOfMaxDepth mm), IT = ( NorIterator Fm);

      deffunc F( FinSequence, FinSequence) = (( <*N*> ^ $1) ^ $2);

      defpred P[] means not contradiction;

      set A = { F(phi1,phi2) where phi1,phi2 be Element of Phim : P[] }, LH = ( dom IT), RH = [:II, A:];

      Fm is Element of ( Funcs ( [:II, Phim:], BOOLEAN )) by Th8;

      then

      reconsider Fmm = Fm as Function of [:II, Phim:], BOOLEAN ;

      

       A1: ( dom Fmm) = [:II, Phim:] by FUNCT_2:def 1;

      reconsider ITT = IT as PartFunc of [:II, ((SS * ) \ { {} }):], BOOLEAN ;

      

       A2: [:II, ((SS * ) \ { {} }):] = the set of all [x, y] where x be Element of II, y be Element of ((SS * ) \ { {} }) by DOMAIN_1: 19;

      now

        let z be object;

        assume

         A3: z in LH;

        then z in [:II, ((SS * ) \ { {} }):];

        then

        consider x be Element of II, y be Element of ((SS * ) \ { {} }) such that

         A4: z = [x, y] by A2;

        consider phi1,phi2 be Element of ((SS * ) \ { {} }) such that

         A5: y = (( <*N*> ^ phi1) ^ phi2) & [x, phi1] in ( dom Fm) & [x, phi2] in ( dom Fm) by Def18, A3, A4;

        reconsider phi11 = phi1, phi22 = phi2 as Element of Phim by ZFMISC_1: 87, A5, A1;

        set yy = F(phi11,phi22);

        x in II & yy in A & z = [x, yy] by A4, A5;

        hence z in RH by ZFMISC_1:def 2;

      end;

      then

       A6: LH c= RH;

      now

        let z be object;

        assume z in RH;

        then

        consider xx,yy be object such that

         A7: xx in II & yy in A & z = [xx, yy] by ZFMISC_1:def 2;

        reconsider x = xx as Element of II by A7;

        consider phi1,phi2 be Element of Phim such that

         A8: yy = F(phi1,phi2) by A7;

        reconsider phi11 = phi1, phi22 = phi2 as string of S;

        (( <*N*> ^ phi11) ^ phi22) is string of S;

        then

        reconsider y = yy as string of S by A8;

         [x, phi1] in ( dom Fmm) & [x, phi2] in ( dom Fmm) by A1;

        then [x, y] in LH by A8, Def18;

        hence z in LH by A7;

      end;

      then RH c= LH;

      hence thesis by A6;

    end;

    

     Lm19: ( dom ( ExIterator ((S,U) -TruthEval m))) = [:(U -InterpretersOf S), (m -ExFormulasOf S):]

    proof

      set mm = m, II = (U -InterpretersOf S), SS = ( AllSymbolsOf S), N = ( TheNorSymbOf S), Fm = ((S,U) -TruthEval mm), Phim = (S -formulasOfMaxDepth mm), IT = ( ExIterator Fm), L = ( LettersOf S);

      deffunc F( set, FinSequence) = ( <*$1*> ^ $2);

      defpred P[] means not contradiction;

      set A = { F(v,phi) where v be Element of L, phi be Element of Phim : P[] }, LH = ( dom IT), RH = [:II, A:];

      Fm is Element of ( Funcs ( [:II, Phim:], BOOLEAN )) by Th8;

      then

      reconsider Fmm = Fm as Function of [:II, Phim:], BOOLEAN ;

      

       A1: ( dom Fmm) = [:II, Phim:] by FUNCT_2:def 1;

      reconsider ITT = IT as PartFunc of [:II, ((SS * ) \ { {} }):], BOOLEAN ;

      

       A2: [:II, ((SS * ) \ { {} }):] = the set of all [x, y] where x be Element of II, y be Element of ((SS * ) \ { {} }) by DOMAIN_1: 19;

      now

        let z be object;

        assume

         A3: z in LH;

        then z in [:II, ((SS * ) \ { {} }):];

        then

        consider x be Element of II, y be Element of ((SS * ) \ { {} }) such that

         A4: z = [x, y] by A2;

        consider v be literal Element of S, w be string of S such that

         A5: [x, w] in ( dom Fm) & y = ( <*v*> ^ w) by Def16, A3, A4;

        reconsider phi = w as Element of Phim by A1, A5, ZFMISC_1: 87;

        reconsider vv = v as Element of L by FOMODEL1:def 14;

        y = ( <*vv*> ^ phi) by A5;

        then y in A;

        hence z in RH by ZFMISC_1:def 2, A4;

      end;

      then

       A6: LH c= RH;

      now

        let z be object;

        assume z in RH;

        then

        consider xx,yy be object such that

         A7: xx in II & yy in A & z = [xx, yy] by ZFMISC_1:def 2;

        reconsider x = xx as Element of II by A7;

        consider vv be Element of L, phi be Element of Phim such that

         A8: yy = F(vv,phi) by A7;

        reconsider v = vv as literal Element of S;

        reconsider w = phi as string of S;

         [x, phi] in ( dom Fm) & yy = ( <*v*> ^ w) by A8, A1;

        hence z in LH by A7, Def16;

      end;

      then RH c= LH;

      hence thesis by A6;

    end;

    theorem :: FOMODEL2:9

    

     Th9: (S -formulasOfMaxDepth (m + 1)) = (((m -ExFormulasOf S) \/ (m -NorFormulasOf S)) \/ (S -formulasOfMaxDepth m))

    proof

      set U = the non empty set, n = (m + 1), II = (U -InterpretersOf S), SS = ( AllSymbolsOf S), N = ( TheNorSymbOf S), I = the Element of II;

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

      set F = ((S,U) -TruthEval ), Fn = (F . nn), Fc = ( curry Fn), Dm = (S -formulasOfMaxDepth m), Dn = (S -formulasOfMaxDepth n);

      (F . mm) is Element of ( PFuncs ( [:II, ((SS * ) \ { {} }):], BOOLEAN ));

      then

      reconsider Fm = (F . mm) as PartFunc of [:II, ((SS * ) \ { {} }):], BOOLEAN ;

      

       A1: ((S,U) -TruthEval n) = Fn & ((S,U) -TruthEval m) = Fm by Def20;

      reconsider Fcc = Fc as Function of II, ( Funcs (Dn, BOOLEAN )) by Lm17, A1;

      reconsider fn = (Fcc . I) as Function of Dn, BOOLEAN ;

      Fm is Element of ( Funcs ( [:II, Dm:], BOOLEAN )) by Th8;

      then

      reconsider Fmm = Fm as Function of [:II, Dm:], BOOLEAN ;

      ( dom fn) = Dn & ( dom Fcc) = II by FUNCT_2:def 1;

      then

       A2: Dn = ( proj2 (( dom Fn) /\ [: {I}, ( proj2 ( dom Fn)):])) by FUNCT_5: 31;

      

       A3: Fn = ((( ExIterator (F . mm)) +* ( NorIterator (F . mm))) +* Fm) by Def19;

      reconsider Em = ( ExIterator (F . mm)) as PartFunc of [:II, ((SS * ) \ { {} }):], BOOLEAN ;

      reconsider dEm = ( dom Em) as Relation of II, ((SS * ) \ { {} });

      reconsider dNm = ( dom ( NorIterator (F . mm))), dFm = ( dom Fm) as Relation of II, ((SS * ) \ { {} });

      

       A4: dFm = ( dom Fmm)

      .= [:II, Dm:] by FUNCT_2:def 1;

      

       A5: ( dom Fn) = (( dom (( ExIterator (F . mm)) +* ( NorIterator (F . mm)))) \/ ( dom Fm)) by A3, FUNCT_4:def 1

      .= ((dEm \/ dNm) \/ dFm) by FUNCT_4:def 1;

      set RNNN = (m -NorFormulasOf S), REEE = (m -ExFormulasOf S);

      ((S,U) -TruthEval m) = Fm by Def20;

      then dNm = [:II, RNNN:] & dEm = [:II, REEE:] by Lm18, Lm19;

      

      then

       A6: ((dEm \/ dNm) \/ dFm) = ( [:II, (REEE \/ RNNN):] \/ [:II, Dm:]) by A4, ZFMISC_1: 97

      .= [:II, ((REEE \/ RNNN) \/ Dm):] by ZFMISC_1: 97;

      reconsider sub = [: {I}, ((REEE \/ RNNN) \/ Dm):] as Subset of [:II, ((REEE \/ RNNN) \/ Dm):] by ZFMISC_1: 96;

      Dn = ( rng ( [:II, ((REEE \/ RNNN) \/ Dm):] /\ sub)) by A6, A2, A5

      .= ((REEE \/ RNNN) \/ Dm);

      hence thesis;

    end;

    theorem :: FOMODEL2:10

    

     Th10: ( AtomicFormulasOf S) is S -prefix

    proof

      set AF = ( AtomicFormulasOf S), SS = ( AllSymbolsOf S), TT = ( AllTermsOf S), C = (S -multiCat );

      now

        let p1,q1,p2,q2 be SS -valued FinSequence;

        assume p1 in AF;

        then

        consider phi1 be string of S such that

         A1: p1 = phi1 & phi1 is 0wff;

        assume p2 in AF;

        then

        consider phi2 be string of S such that

         A2: p2 = phi2 & phi2 is 0wff;

        consider r1 be relational Element of S, T1 be |.( ar r1).| -element Element of (TT * ) such that

         A3: phi1 = ( <*r1*> ^ (C . T1)) by A1;

        consider r2 be relational Element of S, T2 be |.( ar r2).| -element Element of (TT * ) such that

         A4: phi2 = ( <*r2*> ^ (C . T2)) by A2;

        assume (p1 ^ q1) = (p2 ^ q2);

        

        then

         A5: ( <*r1*> ^ ((C . T1) ^ q1)) = (( <*r2*> ^ (C . T2)) ^ q2) by A1, A2, A3, A4, FINSEQ_1: 32

        .= ( <*r2*> ^ ((C . T2) ^ q2)) by FINSEQ_1: 32;

        

        then

         A6: r1 = (( <*r2*> ^ ((C . T2) ^ q2)) . 1) by FINSEQ_1: 41

        .= r2 by FINSEQ_1: 41;

        set n = |.( ar r1).|, nT = (n -tuples_on TT);

        reconsider T11 = T1, T22 = T2 as Element of nT by FOMODEL0: 16, A6;

        reconsider P = (C .: nT) as SS -prefix set;

        

         A7: (((SS * ) \ { {} }) * ) c= ((SS * ) * ) & (TT * ) c= (((SS * ) \ { {} }) * );

        then T1 in ((SS * ) * ) & T2 in ((SS * ) * ) & ( dom C) = ((SS * ) * ) by FUNCT_2:def 1;

        then

         A8: (C . T11) in P & (C . T22) in P by FUNCT_1:def 6;

        reconsider T111 = T1, T222 = T2 as Element of ((SS * ) * ) by A7;

        ((C . T111) ^ q1) = ((C . T222) ^ q2) by A6, FINSEQ_1: 33, A5;

        hence p1 = p2 & q1 = q2 by A1, A2, A8, FOMODEL0:def 19, A3, A4, A6;

      end;

      then AF is SS -prefix;

      hence thesis;

    end;

    registration

      let S;

      cluster ( AtomicFormulasOf S) -> S -prefix;

      coherence by Th10;

    end

    registration

      let S;

      cluster (S -formulasOfMaxDepth 0 ) -> S -prefix;

      coherence

      proof

        (S -formulasOfMaxDepth 0 ) = ( AtomicFormulasOf S) by Lm16;

        hence thesis;

      end;

    end

    definition

      let S, phi;

      :: FOMODEL2:def31

      func Depth phi -> Nat means

      : Def30: phi is it -wff & for n st phi is n -wff holds it <= n;

      existence

      proof

        defpred P[ Nat] means phi is $1 -wff;

        consider m such that

         A1: phi is m -wff by Def24;

        

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

        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;

        assume

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

        assume

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

        

         A6: IT2 <= IT1 by A5, A4;

        IT1 <= IT2 by A4, A5;

        hence thesis by A6, XXREAL_0: 1;

      end;

    end

    

     Lm20: phi in ((S -formulasOfMaxDepth m) \ (S -formulasOfMaxDepth 0 )) implies ex n st (phi is (n + 1) -wff & not phi is n -wff & (n + 1) <= m)

    proof

      set Phim = (S -formulasOfMaxDepth m), Phi0 = (S -formulasOfMaxDepth 0 );

      assume

       B1: phi in (Phim \ Phi0);

      then not phi in Phi0 by XBOOLE_0:def 5;

      then not phi is 0 -wff;

      then ( Depth phi) <> 0 by Def30;

      then

      consider n such that

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

      take n;

       not (n + 1) <= (n + 0 ) by XREAL_1: 8;

      hence phi is (n + 1) -wff & not phi is n -wff by Def30, A1;

      phi is m -wff by B1;

      hence (n + 1) <= m by A1, Def30;

    end;

    

     Lm21: (w is (m + 1) -wff & not w is m -wff) implies ((ex v be literal Element of S, phi be m -wff string of S st w = ( <*v*> ^ phi)) or (ex phi1,phi2 be m -wff string of S st w = (( <*( TheNorSymbOf S)*> ^ phi1) ^ phi2)))

    proof

      set Phim = (S -formulasOfMaxDepth m), PhiM = (S -formulasOfMaxDepth (m + 1)), L = ( LettersOf S), N = ( TheNorSymbOf S), EF = (m -ExFormulasOf S), NF = (m -NorFormulasOf S);

      assume w is (m + 1) -wff;

      then w in PhiM;

      then w in ((EF \/ NF) \/ Phim) by Th9;

      then

       A1: w in EF or w in NF or w in Phim by Lm8;

      assume

       A2: w is non m -wff;

      assume

       A3: not ex v be literal Element of S, phi be m -wff string of S st w = ( <*v*> ^ phi);

      w in EF implies ex v be literal Element of S, phi be m -wff string of S st w = ( <*v*> ^ phi)

      proof

        assume w in EF;

        then

        consider vv be Element of L, phi be Element of Phim such that

         A4: w = ( <*vv*> ^ phi);

        reconsider phii = phi as m -wff string of S by Def23;

        reconsider v = vv as literal Element of S;

        take v;

        take phii;

        thus thesis by A4;

      end;

      then

      consider phi1,phi2 be Element of Phim such that

       A5: w = (( <*N*> ^ phi1) ^ phi2) by A3, A2, A1;

      reconsider phi11 = phi1, phi22 = phi2 as m -wff string of S by Def23;

      take phi11, phi22;

      thus thesis by A5;

    end;

    registration

      let S, m;

      let phi1,phi2 be m -wff string of S;

      cluster (( <*( TheNorSymbOf S)*> ^ phi1) ^ phi2) -> (m + 1) -wff;

      coherence

      proof

        set N = ( TheNorSymbOf S), Phim = (S -formulasOfMaxDepth m), NF = (m -NorFormulasOf S), PhiM = (S -formulasOfMaxDepth (m + 1)), EF = (m -ExFormulasOf S), IT = (( <*N*> ^ phi1) ^ phi2);

        reconsider phi11 = phi1, phi22 = phi2 as Element of Phim by Def23;

        IT = (( <*N*> ^ phi11) ^ phi22);

        then IT in NF;

        then IT in ((EF \/ NF) \/ Phim) by Lm8;

        then

        reconsider ITT = IT as Element of PhiM by Th9;

        ITT is (m + 1) -wff;

        hence thesis;

      end;

    end

    registration

      let S, phi1, phi2;

      cluster (( <*( TheNorSymbOf S)*> ^ phi1) ^ phi2) -> wff;

      coherence

      proof

        set N = ( TheNorSymbOf S), IT = (( <*N*> ^ phi1) ^ phi2);

        consider m such that

         A1: phi1 is m -wff by Def24;

        consider n such that

         A2: phi2 is n -wff by Def24;

        reconsider phi11 = phi1 as (m + ( 0 * n)) -wff string of S by A1;

        reconsider phi22 = phi2 as (n + ( 0 * m)) -wff string of S by A2;

        reconsider phi111 = phi11 as (m + n) -wff string of S;

        reconsider phi222 = phi22 as (m + n) -wff string of S;

        (( <*N*> ^ phi111) ^ phi222) is ((m + n) + 1) -wff string of S;

        hence thesis;

      end;

    end

    registration

      let S, m;

      let phi be m -wff string of S, v be literal Element of S;

      cluster ( <*v*> ^ phi) -> (m + 1) -wff;

      coherence

      proof

        set L = ( LettersOf S), Phim = (S -formulasOfMaxDepth m), NF = (m -NorFormulasOf S), PhiM = (S -formulasOfMaxDepth (m + 1)), EF = (m -ExFormulasOf S), IT = ( <*v*> ^ phi);

        reconsider vv = v as Element of L by FOMODEL1:def 14;

        reconsider phii = phi as Element of Phim by Def23;

        IT = ( <*vv*> ^ phii);

        then IT in EF;

        then IT in ((EF \/ NF) \/ Phim) by Lm8;

        then

        reconsider ITT = IT as Element of PhiM by Th9;

        ITT is (m + 1) -wff;

        hence thesis;

      end;

    end

    registration

      let S, l, phi;

      cluster ( <*l*> ^ phi) -> wff;

      coherence

      proof

        consider m such that

         A1: phi is m -wff by Def24;

        reconsider phii = phi as m -wff string of S by A1;

        set IT = ( <*l*> ^ phii);

        IT is (m + 1) -wff;

        hence thesis;

      end;

    end

    registration

      let S, w;

      let s be non relational Element of S;

      cluster ( <*s*> ^ w) -> non 0wff;

      coherence

      proof

        set FC = (S -firstChar ), IT = ( <*s*> ^ w), SS = ( AllSymbolsOf S);

        (FC . IT) = (IT . 1) by FOMODEL0: 6

        .= s by FINSEQ_1: 41;

        hence thesis;

      end;

    end

    registration

      let S, w1, w2;

      let s be non relational Element of S;

      cluster (( <*s*> ^ w1) ^ w2) -> non 0wff;

      coherence

      proof

        (( <*s*> ^ w1) ^ w2) = ( <*s*> ^ (w1 ^ w2)) by FINSEQ_1: 32;

        hence thesis;

      end;

    end

    registration

      let S;

      cluster ( TheNorSymbOf S) -> non relational;

      coherence ;

    end

    registration

      let S, w;

      cluster ( <*( TheNorSymbOf S)*> ^ w) -> non 0wff;

      coherence ;

    end

    registration

      let S, l, w;

      cluster ( <*l*> ^ w) -> non 0wff;

      coherence ;

    end

    definition

      let S, w;

      :: FOMODEL2:def32

      attr w is exal means

      : Def31: ((S -firstChar ) . w) is literal;

    end

    registration

      let S, w, l;

      cluster ( <*l*> ^ w) -> exal;

      coherence

      proof

        set ww = ( <*l*> ^ w), F = (S -firstChar );

        (F . ww) = (ww . 1) by FOMODEL0: 6

        .= l by FINSEQ_1: 41;

        hence thesis;

      end;

    end

    registration

      let S, m1;

      cluster exal for m1 -wff string of S;

      existence

      proof

        consider m such that

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

        set phi = the m -wff string of S, l = the literal Element of S, psi = ( <*l*> ^ phi);

        reconsider psii = psi as m1 -wff string of S by A1;

        take psii;

        thus thesis;

      end;

    end

    registration

      let S;

      cluster exal -> non 0wff for string of S;

      coherence ;

    end

    registration

      let S, m1;

      cluster non 0wff for exalm1 -wff string of S;

      existence

      proof

        set l = the literal Element of S;

        consider m such that

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

        set phi = the m -wff string of S;

        reconsider psi = ( <*l*> ^ phi) as exalm1 -wff string of S by A1;

        take psi;

        thus thesis;

      end;

    end

    registration

      let S;

      cluster non 0wff for exal wff string of S;

      existence

      proof

        take the non 0wff exal the non zero Nat -wff string of S;

        thus thesis;

      end;

    end

    

     Lm22: phi is non 0wff implies ( Depth phi) <> 0

    proof

      assume phi is non 0wff;

      then not phi is 0 -wff;

      hence ( Depth phi) <> 0 by Def30;

    end;

    registration

      let S;

      let phi be non 0wff wff string of S;

      cluster ( Depth phi) -> non zero;

      coherence by Lm22;

    end

    

     Lm23: w is wff & w is non 0wff implies ((w . 1) in ( LettersOf S) or (w . 1) = ( TheNorSymbOf S))

    proof

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

      assume w is wff;

      then

      reconsider ww = w as wff string of S;

      set n = ( Depth ww);

      assume w is non 0wff;

      then

      consider m such that

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

      (m + 1) > (m + 0 ) by XREAL_1: 8;

      then ww is (m + 1) -wff & not ww is m -wff by Def30, A1;

      per cases by Lm21;

        suppose ex v be literal Element of S, phi be m -wff string of S st w = ( <*v*> ^ phi);

        then

        consider v be literal Element of S, phi be m -wff string of S such that

         A2: w = ( <*v*> ^ phi);

        v = (w . 1) by A2, FINSEQ_1: 41;

        hence thesis by FOMODEL1:def 14;

      end;

        suppose ex phi1,phi2 be m -wff string of S st w = (( <*N*> ^ phi1) ^ phi2);

        then

        consider phi1,phi2 be m -wff string of S such that

         A3: w = (( <*N*> ^ phi1) ^ phi2);

        (w . 1) = (( <*N*> ^ (phi1 ^ phi2)) . 1) by A3, FINSEQ_1: 32

        .= N by FINSEQ_1: 41;

        hence thesis;

      end;

    end;

    registration

      let S;

      let w be non 0wff wff string of S;

      cluster ((S -firstChar ) . w) -> non relational;

      coherence

      proof

        set F = (S -firstChar ), L = ( LettersOf S), N = ( TheNorSymbOf S), SS = ( AllSymbolsOf S);

        per cases by Lm23;

          suppose (w . 1) in L;

          then

          reconsider IT = (F . w) as Element of L by FOMODEL0: 6;

          IT is non relational;

          hence thesis;

        end;

          suppose (w . 1) = N;

          hence thesis by FOMODEL0: 6;

        end;

      end;

    end

    

     Lm24: (S -formulasOfMaxDepth m) is S -prefix

    proof

      set SS = ( AllSymbolsOf S), AF = ( AtomicFormulasOf S), Nor = ( TheNorSymbOf S), Phi0 = (S -formulasOfMaxDepth 0 ), F = (S -firstChar );

      defpred P[ Nat] means (S -formulasOfMaxDepth $1) is SS -prefix;

      

       A1: P[ 0 ];

      

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

      proof

        let n;

        assume

         A3: P[n];

        set N = (n + 1), PhiN = (S -formulasOfMaxDepth N), Phin = (S -formulasOfMaxDepth n);

        

         A4: (PhiN \ Phi0) is SS -prefix

        proof

          now

            let p1,q1,p2,q2 be SS -valued FinSequence;

            assume

             A5: p1 in (PhiN \ Phi0);

            then

            reconsider phi1 = p1 as N -wff string of S by Def23;

            consider m1 be Nat such that

             A6: phi1 is (m1 + 1) -wff & not phi1 is m1 -wff & (m1 + 1) <= N by Lm20, A5;

            assume

             A7: p2 in (PhiN \ Phi0);

            then

            reconsider phi2 = p2 as N -wff string of S by Def23;

            consider m2 be Nat such that

             A8: phi2 is (m2 + 1) -wff & not phi2 is m2 -wff & (m2 + 1) <= N by Lm20, A7;

            consider k1 be Nat such that

             A9: n = (m1 + k1) by A6, XREAL_1: 8, NAT_1: 10;

            consider k2 be Nat such that

             A10: n = (m2 + k2) by A8, XREAL_1: 8, NAT_1: 10;

            assume

             A11: (p1 ^ q1) = (p2 ^ q2);

            per cases by Lm21, A6;

              suppose (ex v1 be literal Element of S, phi11 be m1 -wff string of S st phi1 = ( <*v1*> ^ phi11));

              then

              consider v1 be literal Element of S, phi11 be m1 -wff string of S such that

               A12: phi1 = ( <*v1*> ^ phi11);

              per cases by Lm21, A8;

                suppose ex v2 be literal Element of S, phi22 be m2 -wff string of S st phi2 = ( <*v2*> ^ phi22);

                then

                consider v2 be literal Element of S, phi22 be m2 -wff string of S such that

                 A13: phi2 = ( <*v2*> ^ phi22);

                (( <*v2*> ^ phi22) ^ q2) = ( <*v1*> ^ (phi11 ^ q1)) by A13, A11, A12, FINSEQ_1: 32;

                then

                 A14: ( <*v2*> ^ (phi22 ^ q2)) = ( <*v1*> ^ (phi11 ^ q1)) by FINSEQ_1: 32;

                then

                 A15: (( <*v2*> ^ (phi22 ^ q2)) . 1) = v1 by FINSEQ_1: 41;

                then

                 A16: v2 = v1 by FINSEQ_1: 41;

                ( <*v1*> ^ (phi22 ^ q2)) = ( <*v1*> ^ (phi11 ^ q1)) by A14, A15, FINSEQ_1: 41;

                then

                 A17: (phi22 ^ q2) = (phi11 ^ q1) by FINSEQ_1: 33;

                phi11 is (m1 + ( 0 * k1)) -wff & phi22 is (m2 + ( 0 * k2)) -wff;

                then phi11 in Phin & phi22 in Phin by A9, A10, Def23;

                hence p1 = p2 & q1 = q2 by A12, A16, A13, A3, A17, FOMODEL0:def 19;

              end;

                suppose ex r2,s2 be m2 -wff string of S st phi2 = (( <*Nor*> ^ r2) ^ s2);

                then

                consider r2,s2 be m2 -wff string of S such that

                 A18: phi2 = (( <*Nor*> ^ r2) ^ s2);

                (phi1 . 1) = ((phi2 ^ q2) . 1) by FOMODEL0: 28, A11

                .= (phi2 . 1) by FOMODEL0: 28

                .= (( <*Nor*> ^ (r2 ^ s2)) . 1) by A18, FINSEQ_1: 32

                .= Nor by FINSEQ_1: 41;

                hence p1 = p2 & q1 = q2 by A12, FINSEQ_1: 41;

              end;

            end;

              suppose ex r1,s1 be m1 -wff string of S st phi1 = (( <*Nor*> ^ r1) ^ s1);

              then

              consider r1,s1 be m1 -wff string of S such that

               A19: phi1 = (( <*Nor*> ^ r1) ^ s1);

              

               A20: (phi1 . 1) = (( <*Nor*> ^ (r1 ^ s1)) . 1) by A19, FINSEQ_1: 32

              .= Nor by FINSEQ_1: 41;

              per cases by A8, Lm21;

                suppose ex v2 be literal Element of S, phi22 be m2 -wff string of S st phi2 = ( <*v2*> ^ phi22);

                then

                consider v2 be literal Element of S, phi22 be m2 -wff string of S such that

                 A21: phi2 = ( <*v2*> ^ phi22);

                (phi1 . 1) = ((phi2 ^ q2) . 1) by FOMODEL0: 28, A11

                .= (( <*v2*> ^ phi22) . 1) by FOMODEL0: 28, A21

                .= v2 by FINSEQ_1: 41;

                hence p1 = p2 & q1 = q2 by A20;

              end;

                suppose ex r2,s2 be m2 -wff string of S st phi2 = (( <*Nor*> ^ r2) ^ s2);

                then

                consider r2,s2 be m2 -wff string of S such that

                 A22: phi2 = (( <*Nor*> ^ r2) ^ s2);

                r1 is (m1 + ( 0 * k1)) -wff & r2 is (m2 + ( 0 * k2)) -wff;

                then

                 A23: r1 in Phin & r2 in Phin & s1 in Phin & s2 in Phin by A9, A10, Def23;

                ( <*Nor*> ^ ((r1 ^ s1) ^ q1)) = (( <*Nor*> ^ (r1 ^ s1)) ^ q1) by FINSEQ_1: 32

                .= ((( <*Nor*> ^ r2) ^ s2) ^ q2) by A19, A22, A11, FINSEQ_1: 32

                .= (( <*Nor*> ^ (r2 ^ s2)) ^ q2) by FINSEQ_1: 32

                .= ( <*Nor*> ^ ((r2 ^ s2) ^ q2)) by FINSEQ_1: 32;

                

                then ((r1 ^ s1) ^ q1) = ((r2 ^ s2) ^ q2) by FINSEQ_1: 33

                .= (r2 ^ (s2 ^ q2)) by FINSEQ_1: 32;

                then (r1 ^ (s1 ^ q1)) = (r2 ^ (s2 ^ q2)) by FINSEQ_1: 32;

                then r1 = r2 & (s1 ^ q1) = (s2 ^ q2) by A3, FOMODEL0:def 19, A23;

                hence p1 = p2 & q1 = q2 by A19, A22, A3, A23, FOMODEL0:def 19;

              end;

            end;

          end;

          hence thesis;

        end;

        now

          let p1,q1,p2,q2 be SS -valued FinSequence;

          assume

           A24: p1 in PhiN & p2 in PhiN & (p1 ^ q1) = (p2 ^ q2);

          then

          reconsider phi1 = p1, phi2 = p2 as N -wff string of S by Def23;

          per cases ;

            suppose

             A25: phi1 in Phi0;

            then phi1 is 0 -wff;

            then

            reconsider phi11 = phi1 as 0wff string of S;

            (F . phi11) is relational Element of S;

            then (phi1 . 1) is relational Element of S by FOMODEL0: 6;

            then ((phi2 ^ q2) . 1) is relational Element of S by A24, FOMODEL0: 28;

            then (phi2 . 1) is relational Element of S by FOMODEL0: 28;

            then (F . phi2) is relational by FOMODEL0: 6;

            then phi2 is 0wff;

            then phi2 is 0 -wff;

            then phi2 in Phi0 & phi1 in Phi0 by A25;

            hence p1 = p2 & q1 = q2 by A24, FOMODEL0:def 19;

          end;

            suppose

             A26: not phi1 in Phi0;

            then phi1 is non 0 -wff;

            then

            reconsider phi11 = phi1 as non 0wff wff string of S;

            (F . phi2) = (phi2 . 1) by FOMODEL0: 6

            .= ((phi1 ^ q1) . 1) by A24, FOMODEL0: 28

            .= (phi1 . 1) by FOMODEL0: 28

            .= (F . phi11) by FOMODEL0: 6;

            then phi2 is non 0 -wff;

            then not phi2 in Phi0;

            then phi1 in (PhiN \ Phi0) & phi2 in (PhiN \ Phi0) by A24, A26, XBOOLE_0:def 5;

            hence p1 = p2 & q1 = q2 by A24, A4;

          end;

        end;

        hence thesis by FOMODEL0:def 19;

      end;

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

      then (S -formulasOfMaxDepth m) is SS -prefix;

      hence thesis;

    end;

    registration

      let S, m;

      cluster (S -formulasOfMaxDepth m) -> S -prefix;

      coherence by Lm24;

    end

    definition

      let S;

      :: original: AllFormulasOf

      redefine

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

      coherence

      proof

        set FF = ( AllFormulasOf S), SS = ( AllSymbolsOf S), IT = ((SS * ) \ { {} });

        now

          let x be object;

          assume x in FF;

          then

          consider phi be string of S such that

           A1: x = phi & ex m st phi is m -wff;

          thus x in IT by A1;

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    registration

      let S;

      cluster -> wff for Element of ( AllFormulasOf S);

      coherence

      proof

        set FF = ( AllFormulasOf S);

        let x be Element of FF;

        x in FF;

        then

        consider phi be string of S such that

         A1: x = phi & ex m st phi is m -wff;

        thus thesis by A1;

      end;

    end

    

     Lm25: ( AllFormulasOf S) is S -prefix

    proof

      set FF = ( AllFormulasOf S), SS = ( AllSymbolsOf S);

      now

        let p1,q1,p2,q2 be SS -valued FinSequence;

        assume

         A1: p1 in FF & p2 in FF & (p1 ^ q1) = (p2 ^ q2);

        then

        reconsider phi1 = p1, phi2 = p2 as wff string of S;

        consider m1 be Nat such that

         A2: phi1 is m1 -wff by Def24;

        consider m2 be Nat such that

         A3: phi2 is m2 -wff by Def24;

        set N = (m1 + m2), PhiN = (S -formulasOfMaxDepth N);

        phi1 is (m1 + ( 0 * m2)) -wff & phi2 is (m2 + ( 0 * m1)) -wff by A2, A3;

        then

        reconsider phi11 = phi1, phi22 = phi2 as N -wff string of S;

        phi11 in PhiN & phi22 in PhiN by Def23;

        hence p1 = p2 & q1 = q2 by A1, FOMODEL0:def 19;

      end;

      then FF is SS -prefix;

      hence thesis;

    end;

    registration

      let S;

      cluster ( AllFormulasOf S) -> S -prefix;

      coherence by Lm25;

    end

    theorem :: FOMODEL2:11

    ( dom ( NorIterator ((S,U) -TruthEval m))) = [:(U -InterpretersOf S), (m -NorFormulasOf S):] by Lm18;

    theorem :: FOMODEL2:12

    ( dom ( ExIterator ((S,U) -TruthEval m))) = [:(U -InterpretersOf S), (m -ExFormulasOf S):] by Lm19;

    

     Lm26: ((U -deltaInterpreter ) " {1}) = ((U -concatenation ) .: ( id (1 -tuples_on U)))

    proof

      set d = (U -deltaInterpreter ), f = (U -concatenation ), U1 = (1 -tuples_on U), U2 = (2 -tuples_on U), A = (f .: ( id U1)), B = U2;

      

       A1: (d " {1}) = (A /\ ((1 + 1) -tuples_on U)) by FOMODEL0: 24

      .= ((f .: ( id U1)) /\ (f .: [:U1, U1:])) by FOMODEL0: 22;

      reconsider O = (f .: ( id U1)) as Subset of (f .: [:U1, U1:]) by RELAT_1: 123;

      (O /\ (f .: [:U1, U1:])) = (O null (f .: [:U1, U1:]))

      .= O;

      hence thesis by A1;

    end;

    theorem :: FOMODEL2:13

    

     Th13: ((U -deltaInterpreter ) " {1}) = the set of all <*u, u*> where u be Element of U

    proof

      set RH = the set of all <*u, u*> where u be Element of U;

      set LH = ((U -deltaInterpreter ) " {1}), X = ((U -concatenation ) .: ( id (1 -tuples_on U)));

      LH = X & X = RH by Lm26, FOMODEL0: 38;

      hence thesis;

    end;

    definition

      let S;

      :: original: TheEqSymbOf

      redefine

      func TheEqSymbOf S -> Element of S ;

      coherence ;

    end

    registration

      let S;

      cluster (( ar ( TheEqSymbOf S)) + 2) -> zero;

      coherence

      proof

        set E = ( TheEqSymbOf S);

        ( ar E) = ( - 2) by FOMODEL1:def 23;

        hence thesis;

      end;

      cluster ( |.( ar ( TheEqSymbOf S)).| - 2) -> zero;

      coherence

      proof

        set E = ( TheEqSymbOf S);

        

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

        .= 2;

         |.( ar E).| = 2 by A1, FOMODEL1:def 23;

        hence thesis;

      end;

    end

    theorem :: FOMODEL2:14

    

     Th14: for phi be 0wff string of S, I be S, U -interpreter-like Function holds (((S -firstChar ) . phi) <> ( TheEqSymbOf S) implies (I -AtomicEval phi) = ((I . ((S -firstChar ) . phi)) . ((I -TermEval ) * ( SubTerms phi)))) & (((S -firstChar ) . phi) = ( TheEqSymbOf S) implies (I -AtomicEval phi) = ((U -deltaInterpreter ) . ((I -TermEval ) * ( SubTerms phi))))

    proof

      let phi be 0wff string of S, I be S, U -interpreter-like Function;

      set TT = ( AllTermsOf S), E = ( TheEqSymbOf S), p = ( SubTerms phi), F = (S -firstChar ), r = (F . phi), n = |.( ar r).|, AF = ( AtomicFormulasOf S), d = (U -deltaInterpreter ), p = ( SubTerms phi), V = (I -AtomicEval phi), f = ((I === ) . r), UV = (I -TermEval ), G = (I . r);

      

       A1: ( |.( ar E).| - 2) = 0 ;

      thus r <> E implies V = ((I . (F . phi)) . (UV * p))

      proof

        assume r <> E;

        then not r in ( dom (E .--> d)) by TARSKI:def 1;

        hence V = (G . (UV * p)) by FUNCT_4: 11;

      end;

      assume r = E;

      then

       A2: r in {E} & n = 2 by TARSKI:def 1, A1;

      then r in ( dom (E .--> d));

      

      then f = ((E .--> d) . r) by FUNCT_4: 13

      .= d by A2, FUNCOP_1: 7;

      hence V = (d . (UV * p));

    end;

    theorem :: FOMODEL2:15

    for I be S, U -interpreter-like Function, phi be 0wff string of S st ((S -firstChar ) . phi) = ( TheEqSymbOf S) holds ((I -AtomicEval phi) = 1 iff (((I -TermEval ) . (( SubTerms phi) . 1)) = ((I -TermEval ) . (( SubTerms phi) . 2))))

    proof

      let I be S, U -interpreter-like Function, phi be 0wff string of S;

      set E = ( TheEqSymbOf S), p = ( SubTerms phi), F = (S -firstChar ), s = (F . phi), UV = (I -TermEval ), V = (I -AtomicEval phi), d = (U -deltaInterpreter ), U2 = (2 -tuples_on U), TT = ( AllTermsOf S), D = the set of all <*u, u*> where u be Element of U;

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

      

       A1: U2 = the set of all <*u1, u2*> where u1,u2 be Element of U by FINSEQ_2: 99;

      

       A2: ( |.( ar E).| - 2) = 0 ;

      reconsider r = s as relational Element of S;

      set f = ((I === ) . r);

      reconsider EE = E as relational Element of S;

      assume

       A3: s = E;

      then V = (d . (UV * p)) & n = 2 by Th14, A2;

      then V = 1 iff (UV * p) in (d " {1}) by FOMODEL0: 25;

      then

       A4: V = 1 iff (UV * p) in D by Th13;

      reconsider pp = p as 2 -element FinSequence of TT by FINSEQ_1:def 11, A3, A2;

      reconsider q = (UV * pp) as FinSequence of U;

      reconsider qq = q as Element of U2 by FOMODEL0: 16;

      qq in U2;

      then

      consider u1,u2 be Element of U such that

       A5: qq = <*u1, u2*> by A1;

      

       A6: (qq . 1) = u1 & (qq . 2) = u2 by A5, FINSEQ_1: 44;

      1 <= 2;

      then 1 <= 1 & 1 <= ( len q) & 1 <= 2 & 2 <= ( len q) by CARD_1:def 7;

      then 1 in ( Seg ( len q)) & 2 in ( Seg ( len q));

      then 1 in ( dom q) & 2 in ( dom q) by FINSEQ_1:def 3;

      then

       A7: (q . 1) = (UV . (p . 1)) & (q . 2) = (UV . (p . 2)) by FUNCT_1: 12;

      q in D implies (UV . (p . 1)) = (UV . (p . 2))

      proof

        assume q in D;

        then

        consider u be Element of U such that

         A8: <*u, u*> = q;

        (q . 1) = u & (q . 2) = u by A8, FINSEQ_1: 44;

        hence thesis by A7;

      end;

      hence thesis by A4, A7, A5, A6;

    end;

    registration

      let S, m;

      cluster (m -ExFormulasOf S) -> non empty;

      coherence

      proof

        set IT = (m -ExFormulasOf S), L = ( LettersOf S), Phim = (S -formulasOfMaxDepth m);

        set l = the Element of L, phi = the Element of Phim;

        set x = ( <*l*> ^ phi);

        x in IT;

        hence thesis;

      end;

    end

    registration

      let S, m;

      cluster (m -NorFormulasOf S) -> non empty;

      coherence

      proof

        set IT = (m -NorFormulasOf S), Phim = (S -formulasOfMaxDepth m), N = ( TheNorSymbOf S), phi1 = the Element of Phim, x = (( <*N*> ^ phi1) ^ phi1);

        x in IT;

        hence thesis;

      end;

    end

    definition

      let S, m;

      :: original: -NorFormulasOf

      redefine

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

      coherence

      proof

        set IT = (m -NorFormulasOf S), Phim = (S -formulasOfMaxDepth m), N = ( TheNorSymbOf S), SS = ( AllSymbolsOf S);

        now

          let x be object;

          assume x in IT;

          then ex phi1,phi2 be Element of Phim st x = (( <*N*> ^ phi1) ^ phi2);

          hence x in ((SS * ) \ { {} });

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    registration

      let S;

      let w be exal string of S;

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

      coherence by Def31;

    end

    registration

      let S, m;

      cluster -> non exal for Element of (m -NorFormulasOf S);

      coherence

      proof

        set IT = (m -NorFormulasOf S), Phim = (S -formulasOfMaxDepth m), F = (S -firstChar ), N = ( TheNorSymbOf S), SS = ( AllSymbolsOf S);

        let x be Element of IT;

        x in IT;

        then

        consider phi1,phi2 be Element of Phim such that

         A1: x = (( <*N*> ^ phi1) ^ phi2);

        reconsider phi = x as string of S;

        (F . phi) = (phi . 1) by FOMODEL0: 6

        .= (( <*N*> ^ (phi1 ^ phi2)) . 1) by FINSEQ_1: 32, A1

        .= N by FINSEQ_1: 41;

        hence thesis;

      end;

    end

    

     Lm27: ( Depth phi) = (m + 1) & phi is exal implies phi in (m -ExFormulasOf S)

    proof

      set p = ( Depth phi), Phim = (S -formulasOfMaxDepth m), E = (m -ExFormulasOf S), PhiM = (S -formulasOfMaxDepth (m + 1)), N = (m -NorFormulasOf S);

      

       Z0: (PhiM \ Phim) = (((E \/ N) \/ Phim) \ Phim) by Th9

      .= ((E \/ N) \ Phim) by XBOOLE_1: 40;

      

       B0: (m + 0 ) < (m + 1) by XREAL_1: 8;

      assume p = (m + 1);

      then phi is (m + 1) -wff & not phi is m -wff by B0, Def30;

      then phi in PhiM & not phi in Phim;

      then

       Z1: phi in (PhiM \ Phim) by XBOOLE_0:def 5;

      assume phi is exal;

      then not phi in N;

      hence phi in E by Z1, XBOOLE_0:def 3, Z0;

    end;

    

     Lm28: ( Depth ( <*l*> ^ phi1)) > ( Depth phi1)

    proof

      set nor = ( TheNorSymbOf S), phi = ( <*l*> ^ phi1), m = ( Depth phi1), M = ( Depth phi), L = ( LettersOf S);

      consider n such that

       B1: M = (n + 1) by NAT_1: 6;

      set Phin = (S -formulasOfMaxDepth n);

      phi in (n -ExFormulasOf S) by Lm27, B1;

      then

      consider v be Element of L, psi be Element of Phin such that

       B0: phi = ( <*v*> ^ psi) & not contradiction;

      v = (( <*v*> ^ psi) . 1) by FINSEQ_1: 41

      .= l by B0, FINSEQ_1: 41;

      then psi = phi1 by B0, FINSEQ_1: 33;

      then phi1 is n -wff;

      then m <= n by Def30;

      then (m + 0 ) < (n + 1) by XREAL_1: 8;

      hence thesis by B1;

    end;

    definition

      let S, m;

      :: original: -ExFormulasOf

      redefine

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

      coherence

      proof

        set IT = (m -ExFormulasOf S), SS = ( AllSymbolsOf S), Phim = (S -formulasOfMaxDepth m), L = ( LettersOf S);

        now

          let x be object;

          assume x in IT;

          then ex l be Element of L, phi be Element of Phim st x = ( <*l*> ^ phi);

          hence x in ((SS * ) \ { {} });

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    registration

      let S, m;

      cluster -> exal for Element of (m -ExFormulasOf S);

      coherence

      proof

        set E = (m -ExFormulasOf S), L = ( LettersOf S), Phim = (S -formulasOfMaxDepth m);

        let x be Element of E;

        x in E;

        then

        consider l be Element of L, phi be Element of Phim such that

         A1: x = ( <*l*> ^ phi);

        thus thesis by A1;

      end;

    end

    

     Lm29: (( Depth phi) = (m + 1) & not phi is exal) implies phi in (m -NorFormulasOf S)

    proof

      set p = ( Depth phi), Phim = (S -formulasOfMaxDepth m), E = (m -ExFormulasOf S), PhiM = (S -formulasOfMaxDepth (m + 1)), N = (m -NorFormulasOf S);

      

       Z0: (PhiM \ Phim) = (((E \/ N) \/ Phim) \ Phim) by Th9

      .= ((E \/ N) \ Phim) by XBOOLE_1: 40;

      

       B0: (m + 0 ) < (m + 1) by XREAL_1: 8;

      assume p = (m + 1);

      then phi is (m + 1) -wff & not phi is m -wff by B0, Def30;

      then phi in PhiM & not phi in Phim;

      then

       Z1: phi in (PhiM \ Phim) by XBOOLE_0:def 5;

      assume not phi is exal;

      then not phi in E;

      hence phi in N by Z0, Z1, XBOOLE_0:def 3;

    end;

    registration

      let S;

      cluster non literal for Element of S;

      existence

      proof

        take ( TheNorSymbOf S);

        thus thesis;

      end;

    end

    registration

      let S, w;

      let s be non literal Element of S;

      cluster ( <*s*> ^ w) -> non exal;

      coherence

      proof

        set IT = ( <*s*> ^ w), F = (S -firstChar ), SS = ( AllSymbolsOf S);

        (F . IT) = (IT . 1) by FOMODEL0: 6

        .= s by FINSEQ_1: 41;

        hence thesis;

      end;

    end

    registration

      let S, w1, w2;

      let s be non literal Element of S;

      cluster (( <*s*> ^ w1) ^ w2) -> non exal;

      coherence

      proof

        (( <*s*> ^ w1) ^ w2) = ( <*s*> ^ (w1 ^ w2)) by FINSEQ_1: 32;

        hence thesis;

      end;

    end

    registration

      let S;

      cluster ( TheNorSymbOf S) -> non literal;

      coherence ;

    end

    theorem :: FOMODEL2:16

    

     Th16: phi in ( AllFormulasOf S)

    proof

      set AF = ( AllFormulasOf S);

      consider m such that

       A1: phi is m -wff by Def24;

      thus thesis by A1;

    end;

    

     Lm30: ( Depth (( <*( TheNorSymbOf S)*> ^ phi1) ^ phi2)) > ( Depth phi1) & ( Depth (( <*( TheNorSymbOf S)*> ^ phi1) ^ phi2)) > ( Depth phi2)

    proof

      set nor = ( TheNorSymbOf S), phi = (( <*nor*> ^ phi1) ^ phi2), m1 = ( Depth phi1), m2 = ( Depth phi2), M = ( Depth phi), L = ( LettersOf S), FF = ( AllFormulasOf S), SS = ( AllSymbolsOf S);

      consider n such that

       B0: M = (n + 1) by NAT_1: 6;

      set Phin = (S -formulasOfMaxDepth n);

      phi in (n -NorFormulasOf S) by Lm29, B0;

      then

      consider phi11,phi22 be Element of Phin such that

       B1: phi = (( <*nor*> ^ phi11) ^ phi22) & not contradiction;

      reconsider phi111 = phi11, phi222 = phi22 as n -wff string of S by Def23;

      ( <*nor*> ^ (phi1 ^ phi2)) = phi by FINSEQ_1: 32

      .= ( <*nor*> ^ (phi11 ^ phi22)) by B1, FINSEQ_1: 32;

      then

       B2: (phi1 ^ phi2) = (phi111 ^ phi222) by FINSEQ_1: 33;

      phi111 in FF & phi1 in FF by Th16;

      then phi1 is n -wff & phi2 is n -wff by FOMODEL0:def 19, B2;

      then m1 <= n & m2 <= n by Def30;

      then (m1 + 0 ) < (n + 1) & (m2 + 0 ) < (n + 1) by XREAL_1: 8;

      hence thesis by B0;

    end;

    

     Lm31: ( Depth (( <*( TheNorSymbOf S)*> ^ phi1) ^ phi2)) = (( max (( Depth phi1),( Depth phi2))) + 1)

    proof

      set nor = ( TheNorSymbOf S), phi = (( <*nor*> ^ phi1) ^ phi2), m1 = ( Depth phi1), m2 = ( Depth phi2), m = ( max (m1,m2)), M = ( Depth phi);

      M <= M & M > m1 & M > m2 by Lm30;

      then M > m by XXREAL_0:def 10;

      then

       B1: (m + 1) <= M by NAT_1: 13;

      reconsider mm = m as Nat by XXREAL_0: 16;

      reconsider d1 = (m - m1), d2 = (m - m2) as Nat;

      phi1 is (m1 + ( 0 * d1)) -wff & phi2 is (m2 + ( 0 * d2)) -wff by Def30;

      then phi1 is (m1 + d1) -wff & phi2 is (m2 + d2) -wff;

      then

      reconsider phi11 = phi1, phi22 = phi2 as m -wff string of S;

       J1:

      now

        let n;

        assume phi is n -wff;

        then n >= M by Def30;

        hence n >= (m + 1) by B1, XXREAL_0: 2;

      end;

      set Phim = (S -formulasOfMaxDepth mm), NF = (mm -NorFormulasOf S), PhiM = (S -formulasOfMaxDepth (mm + 1)), EF = (mm -ExFormulasOf S);

      reconsider phi111 = phi11, phi222 = phi22 as Element of Phim by Def23;

      phi = (( <*nor*> ^ phi111) ^ phi222);

      then phi in NF;

      then phi in ((EF \/ NF) \/ Phim) by Lm8;

      then

      reconsider ITT = phi as Element of PhiM by Th9;

      ITT is (m + 1) -wff;

      then (( <*nor*> ^ phi11) ^ phi22) is (m + 1) -wff string of S;

      hence M = (m + 1) by Def30, J1;

    end;

    notation

      let S;

      let m be natural Number;

      let w;

      antonym w is m -nonwff for w is m -wff;

    end

    registration

      let m, S;

      cluster non m -wff -> m -nonwff for string of S;

      coherence ;

    end

    registration

      let S, phi1, phi2;

      cluster (( <*( TheNorSymbOf S)*> ^ phi1) ^ phi2) -> ( max (( Depth phi1),( Depth phi2))) -nonwff;

      coherence

      proof

        set nor = ( TheNorSymbOf S), phi = (( <*nor*> ^ phi1) ^ phi2), m1 = ( Depth phi1), m2 = ( Depth phi2), m = ( Depth phi), M = ( max (m1,m2));

        m = (M + 1) by Lm31;

        then m > (M + 0 ) by XREAL_1: 8;

        hence thesis by Def30;

      end;

    end

    registration

      let S, phi, l;

      cluster ( <*l*> ^ phi) -> ( Depth phi) -nonwff;

      coherence

      proof

        set m = ( Depth phi), psi = ( <*l*> ^ phi), M = ( Depth psi);

        m < M by Lm28;

        hence thesis by Def30;

      end;

    end

    registration

      let S, phi, l;

      cluster ( <*l*> ^ phi) -> (1 + ( Depth phi)) -wff;

      coherence

      proof

        set m = ( Depth phi), psi = ( <*l*> ^ phi), M = ( Depth psi);

        reconsider phii = phi as m -wff string of S by Def30;

        ( <*l*> ^ phii) is (m + 1) -wff;

        hence thesis;

      end;

    end

    

     Lm32: for I be Relation st I in (U -InterpretersOf S) holds ( dom I) = ( OwnSymbolsOf S)

    proof

      set O = ( OwnSymbolsOf S), II = (U -InterpretersOf S);

      let I be Relation;

      assume I in II;

      then

      consider f be Element of ( Funcs (O,( PFuncs ((U * ),(U \/ BOOLEAN ))))) such that

       A1: I = f & f is S, U -interpreter-like;

      reconsider ff = f as Function of O, ( PFuncs ((U * ),(U \/ BOOLEAN )));

      thus ( dom I) = O by A1, FUNCT_2:def 1;

    end;

    registration

      let S, U;

      cluster -> ( OwnSymbolsOf S) -defined for Element of (U -InterpretersOf S);

      coherence

      proof

        set O = ( OwnSymbolsOf S), II = (U -InterpretersOf S);

        let I be Element of II;

        ( dom I) c= O by Lm32;

        hence thesis by RELAT_1:def 18;

      end;

    end

    registration

      let S, U;

      cluster ( OwnSymbolsOf S) -defined for Element of (U -InterpretersOf S);

      existence

      proof

        set II = (U -InterpretersOf S);

        take the Element of II;

        thus thesis;

      end;

    end

    registration

      let S, U;

      cluster -> total for ( OwnSymbolsOf S) -defined Element of (U -InterpretersOf S);

      coherence

      proof

        set O = ( OwnSymbolsOf S), II = (U -InterpretersOf S);

        let I be O -defined Element of II;

        ( dom I) = O by Lm32;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    definition

      let S, U;

      let I be Element of (U -InterpretersOf S);

      let x be literal Element of S, u be Element of U;

      :: original: ReassignIn

      redefine

      func (x,u) ReassignIn I -> Element of (U -InterpretersOf S) ;

      coherence

      proof

        set II = (U -InterpretersOf S), IT = ((x,u) ReassignIn I), O = ( OwnSymbolsOf S), new = ( { {} } --> u), g = (x .--> new);

        reconsider xx = x as own Element of S;

         {x} c= O & ( dom g) = {x} by FOMODEL1:def 19, ZFMISC_1: 31;

        then

        reconsider G = ( dom g) as Subset of O;

        ( dom IT) = (( dom I) \/ G) by FUNCT_4:def 1

        .= (O \/ G) by PARTFUN1:def 2

        .= O;

        then

        reconsider ITT = IT as O -defined Function by RELAT_1:def 18;

        (ITT | O) = ITT;

        hence thesis by Th2;

      end;

    end

    

     Lm33: for I be Element of (U -InterpretersOf S) st w is m -wff holds (((I,m) -TruthEval ) . w) = (((S,U) -TruthEval m) . [I, w])

    proof

      set II = (U -InterpretersOf S);

      let I be Element of II;

      set g = ((I,m) -TruthEval ), f = ((S,U) -TruthEval m), Phim = (S -formulasOfMaxDepth m);

      f is Element of ( Funcs ( [:II, Phim:], BOOLEAN )) by Th8;

      then

      reconsider ff = f as Function of [:II, Phim:], BOOLEAN ;

      

       A1: ( dom ff) = [:II, Phim:] by FUNCT_2:def 1;

      assume w is m -wff;

      then w in Phim;

      then [I, w] in ( dom f) & g = (( curry f) . I) by A1, ZFMISC_1: 87;

      then w in ( dom g) & (g . w) = (f . (I,w)) by FUNCT_5: 20;

      hence thesis;

    end;

    reserve I for Element of (U -InterpretersOf S);

    

     Lm34: for f be PartFunc of [:(U -InterpretersOf S), ((( AllSymbolsOf S) * ) \ { {} }):], BOOLEAN st ( dom f) = [:(U -InterpretersOf S), (S -formulasOfMaxDepth m):] & phi1 is m -wff holds ((f -ExFunctor (I,( <*l*> ^ phi1))) = 1 iff ex u st (f . (((l,u) ReassignIn I),phi1)) = TRUE )

    proof

      set II = (U -InterpretersOf S), SS = ( AllSymbolsOf S), N = ( TheNorSymbOf S), psi = ( <*l*> ^ phi1), FF = ( AllFormulasOf S), Phim = (S -formulasOfMaxDepth m);

      let f be PartFunc of [:II, ((SS * ) \ { {} }):], BOOLEAN ;

      assume ( dom f) = [:II, Phim:] & phi1 is m -wff;

      set LH = (f -ExFunctor (I,psi));

      reconsider psii = psi, phi11 = phi1 as FinSequence of SS by FOMODEL0: 26;

      

       A1: (( <*l*> ^ phi11) /^ 1) = phi11 by FINSEQ_6: 45;

      hereby

        assume LH = 1;

        then

        consider u be Element of U, v be literal Element of S such that

         A2: ((psi . 1) = v & (f . (((v,u) ReassignIn I),(psi /^ 1))) = TRUE ) by Def15;

        take u;

        thus (f . (((l,u) ReassignIn I),phi1)) = TRUE by A2, A1, FINSEQ_1: 41;

      end;

      given u such that

       A3: (f . (((l,u) ReassignIn I),phi1)) = TRUE ;

      ex u1, l1 st (psii . 1) = l1 & (f . (((l1,u1) ReassignIn I),(psii /^ 1))) = TRUE by A1, FINSEQ_1: 41, A3;

      hence thesis by Def15;

    end;

    

     Lm35: (I -TruthEval ( <*l*> ^ phi)) = TRUE iff (ex u st (((l,u) ReassignIn I) -TruthEval phi) = 1)

    proof

      set Nor = ( TheNorSymbOf S), II = (U -InterpretersOf S), SS = ( AllSymbolsOf S), D = ( PFuncs ( [:II, ((SS * ) \ { {} }):], BOOLEAN )), m = ( Depth phi), M = (m + 1), L = ( LettersOf S);

      reconsider phii = phi as m -wff string of S by Def30;

      reconsider psi = ( <*l*> ^ phi) as M -wff string of S;

      deffunc E( Element of D) = ( ExIterator $1);

      deffunc N( Element of D) = ( NorIterator $1);

      set F = ((S,U) -TruthEval );

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

      set Phim = (S -formulasOfMaxDepth m), PhiM = (S -formulasOfMaxDepth M);

      reconsider phiii = phii as Element of Phim by Def23;

      reconsider ll = l as Element of L by FOMODEL1:def 14;

      set FM = ((S,U) -TruthEval M), Fm = ((S,U) -TruthEval m), mNF = (m -NorFormulasOf S), mEF = (m -ExFormulasOf S);

      psi = ( <*ll*> ^ phiii);

      then psi in mEF & not psi in mNF;

      then [I, psi] in [:II, mEF:] & not [I, psi] in [:II, mNF:] by ZFMISC_1: 87;

      then

       A1: [I, psi] in ( dom ( ExIterator Fm)) & not [I, psi] in ( dom ( NorIterator Fm)) by Lm18, Lm19;

      

       A2: (F . MM) = ((( ExIterator (F . mm)) +* ( NorIterator (F . mm))) +* (F . mm)) by Def19;

      Fm is Element of ( Funcs ( [:II, Phim:], BOOLEAN )) by Th8;

      then

      reconsider Fmm = Fm as Function of [:II, Phim:], BOOLEAN ;

      

       A3: not [I, psi] in ( dom (F . mm))

      proof

        

         A4: not psi in Phim by Def23;

        ( dom (F . mm)) = ( dom Fmm) by Def20

        .= [:II, Phim:] by FUNCT_2:def 1;

        hence thesis by A4, ZFMISC_1: 87;

      end;

      

       A5: ( dom Fmm) = [:II, Phim:] by FUNCT_2:def 1;

      

       A6: (I -TruthEval psi) = (((I,M) -TruthEval ) . psi) by Def25

      .= (FM . [I, psi]) by Lm33

      .= ((F . MM) . [I, psi]) by Def20

      .= ((( ExIterator (F . mm)) +* ( NorIterator (F . mm))) . [I, psi]) by A2, A3, FUNCT_4: 11

      .= ((( ExIterator (F . mm)) +* ( NorIterator Fm)) . [I, psi]) by Def20

      .= (( ExIterator (F . mm)) . [I, psi]) by FUNCT_4: 11, A1

      .= ( E(Fm) . (I,psi)) by Def20

      .= (Fm -ExFunctor (I,psi)) by A1, Def16;

      

       A7: (ex u st (Fm . (((l,u) ReassignIn I),phii)) = TRUE ) implies ex u st (((l,u) ReassignIn I) -TruthEval phii) = TRUE

      proof

        given u such that

         A8: (Fm . (((l,u) ReassignIn I),phii)) = TRUE ;

        take u;

        set J = ((l,u) ReassignIn I);

        (((J,m) -TruthEval ) . phii) = TRUE by A8, Lm33;

        hence thesis by Def25;

      end;

      (ex u st (((l,u) ReassignIn I) -TruthEval phii) = TRUE ) implies (ex u st (Fm . (((l,u) ReassignIn I),phii)) = TRUE )

      proof

        given u such that

         A9: (((l,u) ReassignIn I) -TruthEval phii) = TRUE ;

        take u;

        set J = ((l,u) ReassignIn I);

        (((J,m) -TruthEval ) . phii) = TRUE by A9, Def25;

        hence thesis by Lm33;

      end;

      hence thesis by A6, A5, Lm34, A7;

    end;

    

     Lm36: for f be PartFunc of [:(U -InterpretersOf S), ((( AllSymbolsOf S) * ) \ { {} }):], BOOLEAN st ( dom f) = [:(U -InterpretersOf S), (S -formulasOfMaxDepth m):] & phi1 is m -wff holds ((f -NorFunctor (I,(( <*( TheNorSymbOf S)*> ^ phi1) ^ w2))) = 1 iff (f . (I,phi1)) = 0 & (f . (I,w2)) = 0 )

    proof

      set II = (U -InterpretersOf S), SS = ( AllSymbolsOf S), N = ( TheNorSymbOf S), phi2 = w2, psi = (( <*N*> ^ phi1) ^ phi2), FF = ( AllFormulasOf S), Phim = (S -formulasOfMaxDepth m);

      let f be PartFunc of [:II, ((SS * ) \ { {} }):], BOOLEAN ;

      assume

       A1: ( dom f) = [:II, Phim:] & phi1 is m -wff;

      set LH = (f -NorFunctor (I,psi)), RH1 = (f . (I,phi1)), RH2 = (f . (I,phi2));

      hereby

        assume LH = 1;

        then

        consider w, w1 such that

         A2: [I, w] in ( dom f) & (f . (I,w)) = FALSE & (f . (I,w1)) = FALSE & psi = (( <*N*> ^ w) ^ w1) by Def17;

        

         A3: w in Phim & phi1 in Phim by A1, A2, ZFMISC_1: 87;

        ( <*N*> ^ (w ^ w1)) = psi by A2, FINSEQ_1: 32

        .= ( <*N*> ^ (phi1 ^ phi2)) by FINSEQ_1: 32;

        then (w ^ w1) = (phi1 ^ phi2) by FINSEQ_1: 33;

        hence RH1 = 0 & RH2 = 0 by A2, FOMODEL0:def 19, A3;

      end;

      assume RH1 = 0 & RH2 = 0 ;

      hence LH = 1 by A1, ZFMISC_1: 87, Def17;

    end;

    

     Lm37: (I -TruthEval (( <*( TheNorSymbOf S)*> ^ phi1) ^ phi2)) = TRUE iff ((I -TruthEval phi1) = FALSE & (I -TruthEval phi2) = FALSE )

    proof

      set Nor = ( TheNorSymbOf S), II = (U -InterpretersOf S), SS = ( AllSymbolsOf S), B = BOOLEAN , D = ( PFuncs ( [:II, ((SS * ) \ { {} }):], BOOLEAN )), m1 = ( Depth phi1), m2 = ( Depth phi2);

      deffunc E( Element of D) = ( ExIterator $1);

      deffunc N( Element of D) = ( NorIterator $1);

      set F = ((S,U) -TruthEval );

      reconsider m = ( max (m1,m2)) as Nat by TARSKI: 1;

      set M = (m + 1);

      reconsider d1 = (m - m1), d2 = (m - m2) as Nat;

      phi1 is (m1 + ( 0 * d1)) -wff & phi2 is (m2 + ( 0 * d2)) -wff by Def30;

      then phi1 is (m1 + d1) -wff & phi2 is (m2 + d2) -wff;

      then

      reconsider phi11 = phi1, phi22 = phi2 as m -wff string of S;

      reconsider phi = (( <*Nor*> ^ phi11) ^ phi22) as (m + 1) -wff string of S;

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

      set Phim = (S -formulasOfMaxDepth m), PhiM = (S -formulasOfMaxDepth M);

      set FM = ((S,U) -TruthEval M), Fm = ((S,U) -TruthEval m), mNF = (m -NorFormulasOf S);

      

       A1: (I -TruthEval phi1) = (((I,m) -TruthEval ) . phi11) by Def25

      .= (Fm . (I,phi1)) by Lm33;

      

       A2: (I -TruthEval phi22) = (((I,m) -TruthEval ) . phi22) by Def25

      .= (Fm . (I,phi2)) by Lm33;

      reconsider phi111 = phi11, phi222 = phi22 as Element of Phim by Def23;

      phi = (( <*Nor*> ^ phi111) ^ phi222);

      then phi in mNF;

      then [I, phi] in [:II, mNF:] by ZFMISC_1: 87;

      then

       A3: [I, phi] in ( dom ( NorIterator Fm)) by Lm18;

      

       A4: (F . MM) = ((( ExIterator (F . mm)) +* ( NorIterator (F . mm))) +* (F . mm)) by Def19;

      Fm is Element of ( Funcs ( [:II, Phim:], BOOLEAN )) by Th8;

      then

      reconsider Fmm = Fm as Function of [:II, Phim:], BOOLEAN ;

      

       A5: not [I, phi] in ( dom (F . mm))

      proof

        

         A6: not phi in Phim by Def23;

        ( dom (F . mm)) = ( dom Fmm) by Def20

        .= [:II, Phim:] by FUNCT_2:def 1;

        hence thesis by A6, ZFMISC_1: 87;

      end;

      

       A7: ( dom Fmm) = [:II, Phim:] by FUNCT_2:def 1;

      (I -TruthEval phi) = (((I,M) -TruthEval ) . phi) by Def25

      .= (FM . [I, phi]) by Lm33

      .= ((F . MM) . [I, phi]) by Def20

      .= ((( ExIterator (F . mm)) +* ( NorIterator (F . mm))) . [I, phi]) by A4, A5, FUNCT_4: 11

      .= ((( ExIterator (F . mm)) +* ( NorIterator Fm)) . [I, phi]) by Def20

      .= ( N(Fm) . (I,phi)) by FUNCT_4: 13, A3

      .= (Fm -NorFunctor (I,phi)) by A3, Def18;

      hence thesis by A7, Lm36, A2, A1;

    end;

    definition

      let S, w;

      :: FOMODEL2:def33

      func xnot w -> string of S equals (( <*( TheNorSymbOf S)*> ^ w) ^ w);

      coherence ;

    end

    registration

      let S, m;

      let phi be m -wff string of S;

      cluster ( xnot phi) -> (m + 1) -wff;

      coherence ;

    end

    registration

      let S, phi;

      cluster ( xnot phi) -> wff;

      coherence ;

    end

    registration

      let S;

      cluster ( TheEqSymbOf S) -> non own;

      coherence

      proof

        set E = ( TheEqSymbOf S), R = ( RelSymbolsOf S), O = ( OwnSymbolsOf S);

        E in {E} by TARSKI:def 1;

        then E in (R \ O) by FOMODEL1: 1;

        then not E in O by XBOOLE_0:def 5;

        hence thesis;

      end;

    end

    definition

      let S, X;

      :: FOMODEL2:def34

      attr X is S -mincover means for phi holds (phi in X iff not ( xnot phi) in X);

    end

    theorem :: FOMODEL2:17

    

     Th17: ( Depth (( <*( TheNorSymbOf S)*> ^ phi1) ^ phi2)) = (1 + ( max (( Depth phi1),( Depth phi2)))) & ( Depth ( <*l*> ^ phi1)) = (( Depth phi1) + 1)

    proof

      set N = ( TheNorSymbOf S), m1 = ( Depth phi1), m2 = ( Depth phi2), e = ( <*l*> ^ phi1), n = (( <*N*> ^ phi1) ^ phi2);

      thus ( Depth n) = (1 + ( max (m1,m2))) by Lm31;

      now

        let m;

        assume

         C0: e is m -wff;

        assume m < (m1 + 1);

        then m <= m1 by NAT_1: 13;

        then (m - m) <= (m1 - m) by XREAL_1: 13;

        then

        reconsider k = (m1 - m) as Nat;

        e is (m + ( 0 * k)) -wff by C0;

        then e is (m + k) -wff;

        hence contradiction;

      end;

      hence ( Depth e) = (m1 + 1) by Def30;

    end;

    theorem :: FOMODEL2:18

    (( Depth phi) = (m + 1)) implies ((phi is exal iff phi in (m -ExFormulasOf S)) & (phi is non exal iff phi in (m -NorFormulasOf S))) by Lm27, Lm29;

    theorem :: FOMODEL2:19

    ((I -TruthEval ( <*l*> ^ phi)) = TRUE iff (ex u st (((l,u) ReassignIn I) -TruthEval phi) = 1)) & ((I -TruthEval (( <*( TheNorSymbOf S)*> ^ phi1) ^ phi2)) = TRUE iff ((I -TruthEval phi1) = FALSE & (I -TruthEval phi2) = FALSE )) by Lm35, Lm37;

    reserve I for S, U -interpreter-like Function;

    theorem :: FOMODEL2:20

    

     Th20: ((((I,u) -TermEval ) . (m + 1)) | ((S -termsOfMaxDepth ) . m)) = ((I -TermEval ) | ((S -termsOfMaxDepth ) . m))

    proof

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

      set T = (S -termsOfMaxDepth ), TI = (I -TermEval ), TII = ((I,u) -TermEval ), TT = ( AllTermsOf S);

      reconsider IM = (TII . MM) as Function of TT, U;

      reconsider Tm = (T . mm), TM = (T . MM) as Subset of TT by FOMODEL1: 2;

      set LH = (IM | Tm), RH = (TI | Tm);

      

       A1: ( dom LH) = Tm & ( dom RH) = Tm by PARTFUN1:def 2;

      now

        let x be object;

        assume

         A2: x in ( dom LH);

        then x in (Tm null TT);

        then

        reconsider tt = x as Element of TT;

        reconsider ttt = x as Element of Tm by A2;

        ((LH . ttt) \+\ (IM . ttt)) = {} & ((RH . ttt) \+\ (TI . ttt)) = {} ;

        then

         A3: (LH . x) = (IM . tt) & (RH . x) = (TI . x) by FOMODEL0: 29;

        

        then (LH . x) = (I -TermEval tt) by A2, Def8

        .= (RH . x) by A3, Def9;

        hence (LH . x) = (RH . x);

      end;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: FOMODEL2:21

    

     Th21: ((I -TermEval ) . t) = ((I . ((S -firstChar ) . t)) . ((I -TermEval ) * ( SubTerms t)))

    proof

      set u = the Element of U, TI = (I -TermEval ), TII = ((I,u) -TermEval ), TT = ( AllTermsOf S), F = (S -firstChar ), s = (F . t), m = ( Depth t), T = (S -termsOfMaxDepth ), ST = ( SubTerms t);

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

      

       A1: t is (m + ( 0 * 1)) -termal by FOMODEL1:def 40;

      reconsider tm = t as m -termal string of S by FOMODEL1:def 40;

      reconsider tM = t as (mm + 1) -termal string of S by A1;

      reconsider Tm = (T . mm), TM = (T . MM) as Subset of TT by FOMODEL1: 2;

      reconsider ttt = tm as Element of (T . mm) by FOMODEL1:def 33;

      reconsider tt = t as Element of TT by FOMODEL1:def 32;

      set V = (I -TermEval tt);

      reconsider IM = (TII . MM) as Function of TT, U;

      ( SubTerms tM) is Tm -valued;

      then

       A2: ( dom (TI | Tm)) = Tm & ( dom (IM | Tm)) = Tm & ( rng ST) c= Tm by RELAT_1:def 19, PARTFUN1:def 2;

      (TI . t) = V by Def9

      .= ((TII . MM) . ttt) by Def8

      .= ((TII . ((m + 1) + 1)) . tm) by Lm6

      .= ((I . s) . ((TII . MM) * ST)) by Th3

      .= ((I . s) . (((TII . MM) | Tm) * ST)) by RELAT_1: 165, A2

      .= ((I . s) . ((TI | Tm) * ST)) by Th20

      .= ((I . s) . (TI * ST)) by A2, RELAT_1: 165;

      hence thesis;

    end;

    definition

      let S, phi;

      set F = (S -firstChar ), d = ( Depth phi), s = (F . phi), L = ( LettersOf S), N = ( TheNorSymbOf S), FF = ( AllFormulasOf S), SS = ( AllSymbolsOf S);

      defpred P[ set] means ex phi1, p st p is SS -valued & $1 = [phi1, p] & phi = (( <*((S -firstChar ) . phi)*> ^ phi1) ^ p);

      :: FOMODEL2:def35

      func SubWffsOf phi -> set means

      : Def34: ex phi1, p st p is ( AllSymbolsOf S) -valued & it = [phi1, p] & phi = (( <*((S -firstChar ) . phi)*> ^ phi1) ^ p) if phi is non 0wff

      otherwise it = [phi, {} ];

      existence

      proof

        thus phi is non 0wff implies ex IT be set st P[IT]

        proof

          assume phi is non 0wff;

          then

          consider m such that

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

          per cases ;

            suppose phi is exal;

            then phi in (m -ExFormulasOf S) by A1, Lm27;

            then

            consider ll be Element of L, phi0 be Element of (S -formulasOfMaxDepth m) such that

             A2: phi = ( <*ll*> ^ phi0);

            

             A3: ll = (phi . 1) by A2, FINSEQ_1: 41

            .= s by FOMODEL0: 6;

            reconsider l = ll as literal Element of S;

            reconsider phi1 = phi0 as m -wff string of S by Def23;

            reconsider IT = [phi1, {} ] as set;

            take IT;

            take phi1;

            take p = ( {} null SS);

            thus p is SS -valued;

            thus IT = [phi1, p];

            thus thesis by A2, A3;

          end;

            suppose not phi is exal;

            then phi in (m -NorFormulasOf S) by A1, Lm29;

            then

            consider phi0,psi0 be Element of (S -formulasOfMaxDepth m) such that

             A4: phi = (( <*N*> ^ phi0) ^ psi0);

            

             A5: s = (phi . 1) by FOMODEL0: 6

            .= (( <*N*> ^ (phi0 ^ psi0)) . 1) by A4, FINSEQ_1: 32

            .= N by FINSEQ_1: 41;

            reconsider phi1 = phi0, psi1 = psi0 as m -wff string of S by Def23;

            take IT = [phi1, psi0];

            take phi1;

            take p = psi1;

            thus p is SS -valued;

            thus IT = [phi1, p];

            thus phi = (( <*s*> ^ phi1) ^ p) by A4, A5;

          end;

        end;

        assume phi is 0wff;

        take IT = [phi, {} ];

        thus thesis;

      end;

      uniqueness

      proof

        let IT1,IT2 be set;

        thus phi is non 0wff & P[IT1] & P[IT2] implies IT1 = IT2

        proof

          assume phi is non 0wff;

          then

          reconsider phi as non 0wff string of S;

          assume

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

          consider phi1, p1 such that

           A7: p1 is SS -valued & IT1 = [phi1, p1] & phi = (( <*s*> ^ phi1) ^ p1) by A6;

          consider phi2, p2 such that

           A8: p2 is SS -valued & IT2 = [phi2, p2] & phi = (( <*s*> ^ phi2) ^ p2) by A6;

          reconsider q1 = p1, q2 = p2 as SS -valued FinSequence by A7, A8;

          ( <*s*> ^ (phi1 ^ p1)) = phi by A7, FINSEQ_1: 32

          .= ( <*s*> ^ (phi2 ^ p2)) by FINSEQ_1: 32, A8;

          then (phi1 ^ q1) = (phi2 ^ q2) & phi1 in FF & phi2 in FF by Th16, FINSEQ_1: 33;

          then phi1 = phi2 & q1 = q2 by FOMODEL0:def 19;

          hence thesis by A7, A8;

        end;

        thus phi is 0wff & IT1 = [phi, {} ] & IT2 = [phi, {} ] implies IT1 = IT2;

      end;

      consistency ;

    end

    definition

      let S, phi;

      set IT = ( SubWffsOf phi), SS = ( AllSymbolsOf S), F = (S -firstChar );

      :: FOMODEL2:def36

      func head phi -> wff string of S equals (( SubWffsOf phi) `1 );

      coherence

      proof

        per cases ;

          suppose phi is non 0wff;

          then

          consider phi1, p such that

           A1: p is SS -valued & IT = [phi1, p] & phi = (( <*(F . phi)*> ^ phi1) ^ p) by Def34;

          ((IT `1 ) \+\ phi1) = {} by A1;

          hence thesis by FOMODEL0: 29;

        end;

          suppose phi is 0wff;

          then IT = [phi, {} ] by Def34;

          then ((IT `1 ) \+\ phi) = {} ;

          hence thesis by FOMODEL0: 29;

        end;

      end;

      :: FOMODEL2:def37

      func tail phi -> Element of (( AllSymbolsOf S) * ) equals (( SubWffsOf phi) `2 );

      coherence

      proof

        per cases ;

          suppose phi is non 0wff;

          then

          consider phi1, p such that

           A2: p is SS -valued & IT = [phi1, p] & phi = (( <*(F . phi)*> ^ phi1) ^ p) by Def34;

          (IT `2 ) = p & p is FinSequence of SS by A2, FOMODEL0: 26;

          hence thesis;

        end;

          suppose phi is 0wff;

          then IT = [phi, {} ] by Def34;

          then ((IT `2 ) \+\ {} ) = ( {} null SS);

          then

          reconsider ITT = (IT `2 ) as SS -valued FinSequence;

          ITT is FinSequence of SS by FOMODEL0: 26;

          hence thesis;

        end;

      end;

    end

    registration

      let S, m;

      cluster ((S -formulasOfMaxDepth m) \ ( AllFormulasOf S)) -> empty;

      coherence

      proof

        set Fm = (S -formulasOfMaxDepth m), FF = ( AllFormulasOf S);

        now

          let x be object;

          assume x in Fm;

          then

          reconsider phi = x as m -wff string of S by Def23;

          phi in FF;

          hence x in FF;

        end;

        then Fm c= FF;

        hence thesis;

      end;

    end

    registration

      let S;

      cluster (( AtomicFormulasOf S) \ ( AllFormulasOf S)) -> empty;

      coherence

      proof

        ((S -formulasOfMaxDepth 0 ) \ ( AllFormulasOf S)) = {} ;

        hence thesis by Lm16;

      end;

    end

    theorem :: FOMODEL2:22

    ( Depth ( <*l*> ^ phi1)) > ( Depth phi1) & ( Depth (( <*( TheNorSymbOf S)*> ^ phi1) ^ phi2)) > ( Depth phi1) & ( Depth (( <*( TheNorSymbOf S)*> ^ phi1) ^ phi2)) > ( Depth phi2) by Lm28, Lm30;

    theorem :: FOMODEL2:23

    

     Th23: ( not phi is 0wff) implies (phi = (( <*x*> ^ phi2) ^ p2) iff (x = ((S -firstChar ) . phi) & phi2 = ( head phi) & p2 = ( tail phi)))

    proof

      set Phi = ( SubWffsOf phi), F = (S -firstChar ), s = (F . phi), SS = ( AllSymbolsOf S);

      assume

       A1: not phi is 0wff;

      then

      consider phi1, p such that

       A2: p is SS -valued & Phi = [phi1, p] & phi = (( <*s*> ^ phi1) ^ p) by Def34;

      hereby

        assume

         A4: phi = (( <*x*> ^ phi2) ^ p2);

        

        then

         A5: (phi . 1) = (( <*x*> ^ (phi2 ^ p2)) . 1) by FINSEQ_1: 32

        .= x by FINSEQ_1: 41;

        hence x = s by FOMODEL0: 6;

        ( rng p2) c= ( rng phi) & ( rng phi) c= SS by A4, FINSEQ_1: 30, RELAT_1:def 19;

        then p2 is SS -valued & [phi2, p2] = [phi2, p2] & phi = (( <*s*> ^ phi2) ^ p2) by XBOOLE_1: 1, RELAT_1:def 19, A5, FOMODEL0: 6, A4;

        then Phi = [phi2, p2] by A1, Def34;

        hence phi2 = ( head phi) & p2 = ( tail phi);

      end;

      assume x = s & phi2 = ( head phi) & p2 = ( tail phi);

      hence thesis by A2;

    end;

    registration

      let S, m1;

      cluster non exal for non 0wffm1 -wff string of S;

      existence

      proof

        set phi = the 0 -wff string of S, N = ( TheNorSymbOf S), phi1 = (( <*N*> ^ phi) ^ phi);

        consider m such that

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

        phi1 is non 0wff(1 + ( 0 * m)) -wff string of S;

        then

        reconsider phi11 = phi1 as non 0wffm1 -wff string of S by A1;

        take phi11;

        thus thesis;

      end;

    end

    registration

      let S;

      let phi be exal wff string of S;

      cluster ( tail phi) -> empty;

      coherence

      proof

        set d = ( Depth phi), L = ( LettersOf S), h = ( head phi), t = ( tail phi), F = (S -firstChar ), FF = ( AllFormulasOf S), SS = ( AllSymbolsOf S), s = (F . phi);

        consider m such that

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

        set Phim = (S -formulasOfMaxDepth m);

        phi in (m -ExFormulasOf S) by A1, Lm27;

        then

        consider ll be Element of L, phim be Element of Phim such that

         A2: phi = ( <*ll*> ^ phim);

        reconsider phimm = phim as m -wff string of S by Def23;

        phi = (( <*ll*> ^ phimm) ^ {} ) by A2;

        hence thesis by Th23;

      end;

    end

    

     Lm38: (( Depth phi) = (m + 1) & not phi is exal) implies ex phi2 be m -wff string of S st ( tail phi) = phi2

    proof

      set d = ( Depth phi), Phim = (S -formulasOfMaxDepth m), N = ( TheNorSymbOf S);

      assume d = (m + 1) & not phi is exal;

      then phi in (m -NorFormulasOf S) by Lm29;

      then

      consider phi1,phi2 be Element of Phim such that

       A1: phi = (( <*N*> ^ phi1) ^ phi2);

      reconsider phi11 = phi1, phi22 = phi2 as m -wff string of S by Def23;

      set d1 = ( Depth phi11), d2 = ( Depth phi22);

      take phi22;

      phi = (( <*N*> ^ phi11) ^ phi22) by A1;

      hence phi22 = ( tail phi) by Th23;

      thus thesis;

    end;

    definition

      let S;

      let phi be non exal non 0wff wff string of S;

      :: original: tail

      redefine

      func tail phi -> wff string of S ;

      coherence

      proof

        consider m such that

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

        consider phi2 be m -wff string of S such that

         A2: ( tail phi) = phi2 by A1, Lm38;

        thus thesis by A2;

      end;

    end

    registration

      let S;

      let phi be non exal non 0wff wff string of S;

      cluster ( tail phi) -> wff;

      coherence ;

    end

    registration

      let S, phi0;

      identify phi0 null with head phi0;

      compatibility

      proof

        phi0 = ( [phi0, {} ] `1 ) & ( SubWffsOf phi0) = [phi0, {} ] by Def34;

        hence thesis;

      end;

    end

    registration

      let S;

      let phi be non 0wff non exal wff string of S;

      cluster (((S -firstChar ) . phi) \+\ ( TheNorSymbOf S)) -> empty;

      coherence

      proof

        set F = (S -firstChar ), N = ( TheNorSymbOf S), s = (F . phi);

        consider m such that

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

        phi in (m -NorFormulasOf S) by A1, Lm29;

        then

        consider phi11,phi22 be Element of (S -formulasOfMaxDepth m) such that

         A2: phi = (( <*N*> ^ phi11) ^ phi22);

        (F . phi) = (phi . 1) by FOMODEL0: 6

        .= (( <*N*> ^ (phi11 ^ phi22)) . 1) by A2, FINSEQ_1: 32

        .= N by FINSEQ_1: 41;

        hence thesis;

      end;

    end

    

     Lm39: not phi is 0wff & not phi is exal & phi is (m + 1) -wff implies (( head phi) is m -wff string of S & ( tail phi) is m -wff string of S)

    proof

      assume not phi is 0wff & not phi is exal & phi is (m + 1) -wff;

      then

      reconsider phii = phi as non 0wff non exal(m + 1) -wff string of S;

      set N = ( TheNorSymbOf S), F = (S -firstChar ), s = (F . phii), dh = ( Depth ( head phii)), dt = ( Depth ( tail phii)), M = ( max (dh,dt)), d = ( Depth phii);

      reconsider h = ( head phii) as dh -wff string of S by Def30;

      reconsider t = ( tail phii) as dt -wff string of S by Def30;

      

       A1: d <= (m + 1) by Def30;

      ((F . phii) \+\ N) = {} ;

      then s = N by FOMODEL0: 29;

      then phii = (( <*N*> ^ h) ^ t) by Th23;

      then (M + 1) <= (m + 1) by A1, Th17;

      then ((M + 1) - 1) <= ((m + 1) - 1) by XREAL_1: 8;

      then (M + ( - dh)) <= (m + ( - dh)) & (M + ( - dt)) <= (m + ( - dt)) by XREAL_1: 6;

      then (( max (dh,dt)) - dh) <= (m - dh) & (( max (dh,dt)) - dt) <= (m - dt);

      then 0 <= (m - dh) & 0 <= (m - dt);

      then

      reconsider nh = (m - dh), nt = (m - dt) as Nat;

      h is (dh + ( 0 * nh)) -wff & t is (dt + ( 0 * nt)) -wff;

      then h is (dh + nh) -wff & t is (dt + nt) -wff;

      hence thesis;

    end;

    registration

      let m, S;

      let phi be (m + 1) -wff string of S;

      cluster ( head phi) -> m -wff;

      coherence

      proof

        set d = ( Depth phi), F = (S -firstChar ), s = (F . phi), N = ( TheNorSymbOf S), dh = ( Depth ( head phi));

        reconsider h = ( head phi) as dh -wff string of S by Def30;

        

         A1: d <= (m + 1) by Def30;

        per cases ;

          suppose phi is 0wff;

          then

          reconsider phi0 = phi as 0 -wff string of S;

          phi0 is ( 0 + ( 0 * m)) -wff;

          then (phi0 null phi0) is ( 0 + m) -wff string of S;

          then ( head phi0) is m -wff;

          hence thesis;

        end;

          suppose not phi is 0wff & not phi is exal;

          then

          reconsider phii = phi as non 0wff non exal(m + 1) -wff string of S;

          ( head phii) is m -wff string of S by Lm39;

          hence thesis;

        end;

          suppose not phi is 0wff & phi is exal;

          then

          reconsider phii = phi as non 0wff exal(m + 1) -wff string of S;

          set t = ( tail phii);

          phii = (( <*s*> ^ h) ^ t) by Th23

          .= ( <*s*> ^ h);

          then (dh + 1) <= (m + 1) by A1, Th17;

          then dh <= m by XREAL_1: 8;

          then (dh + ( - dh)) <= (m + ( - dh)) by XREAL_1: 6;

          then

          reconsider n = (m - dh) as Nat;

          h is (dh + ( 0 * n)) -wff;

          then h is (dh + n) -wff;

          hence thesis;

        end;

      end;

    end

    registration

      let m, S;

      let phi be (m + 1) -wff non exal non 0wff string of S;

      cluster ( tail phi) -> m -wff;

      coherence by Lm39;

    end

    theorem :: FOMODEL2:24

    

     Th24: for I be Element of (U -InterpretersOf S) holds ((I,m) -TruthEval ) in ( Funcs ((S -formulasOfMaxDepth m), BOOLEAN ))

    proof

      set Phim = (S -formulasOfMaxDepth m), II = (U -InterpretersOf S);

      let I be Element of II;

      reconsider F = ( curry ((S,U) -TruthEval m)) as Function of II, ( Funcs (Phim, BOOLEAN )) by Lm17;

      (F . I) in ( Funcs (Phim, BOOLEAN ));

      hence thesis;

    end;

    

     Lm40: for I be Element of (U -InterpretersOf S) holds (I -TruthEval phi0) = (I -AtomicEval phi0)

    proof

      set II = (U -InterpretersOf S);

      let I be Element of II;

      set LH = (I -TruthEval phi0), RH = (I -AtomicEval phi0), f = ((S,U) -TruthEval 0 ), Phi0 = (S -formulasOfMaxDepth 0 ), AF = ( AtomicFormulasOf S), SS = ( AllSymbolsOf S);

      reconsider phi000 = phi0 as Element of Phi0 by Def23;

      reconsider phi00 = phi000 as Element of AF by Lm16;

      reconsider z = 0 as Element of NAT ;

      ((I, 0 ) -TruthEval ) is Element of ( Funcs (Phi0, BOOLEAN )) by Th24;

      then

      reconsider g = ((I, 0 ) -TruthEval ) as Function of Phi0, BOOLEAN ;

      set F = ( curry f);

      reconsider F = ( curry f) as Function of II, ( PFuncs (((SS * ) \ { {} }), BOOLEAN )) by Lm11;

      ( dom F) = II & ( dom g) = Phi0 by FUNCT_2:def 1;

      then I in ( dom F) & g = (F . I) & phi000 in ( dom g);

      then

       A1: (g . phi0) = (f . (I,phi0)) & [I, phi0] in ( dom f) by FUNCT_5: 31;

      LH = (g . phi0) by Def25

      .= ((((S,U) -TruthEval ) . z) . [I, phi0]) by A1, Def20

      .= ((S -TruthEval U) . (I,phi00)) by Def19

      .= RH by Def14;

      hence thesis;

    end;

    registration

      let S, U;

      let I be Element of (U -InterpretersOf S);

      let phi0;

      identify I -AtomicEval phi0 with I -TruthEval phi0;

      compatibility by Lm40;

      identify I -TruthEval phi0 with I -AtomicEval phi0;

      compatibility ;

    end

    registration

      let S;

      cluster non literal for ofAtomicFormula Element of S;

      existence

      proof

        take ( TheEqSymbOf S);

        thus thesis;

      end;

    end

    

     Lm41: for I1,I2 be S, U -interpreter-like Function st (I1 | X) = (I2 | X) holds ((I1 -TermEval ) | (X * )) = ((I2 -TermEval ) | (X * ))

    proof

      set T = (S -termsOfMaxDepth ), O = ( OwnSymbolsOf S), TT = ( AllTermsOf S), SS = ( AllSymbolsOf S), L = ( LettersOf S), F = (S -firstChar ), C = (S -multiCat );

      let I1,I2 be S, U -interpreter-like Function;

      set E1 = (I1 -TermEval ), E2 = (I2 -TermEval ), I11 = (I1 | X), I22 = (I2 | X);

      assume

       A1: I11 = I22;

      then

       A2: ( dom E1) = TT & ( dom E2) = TT & I11 = I22 by FUNCT_2:def 1;

      defpred P[ Nat] means ((I1 -TermEval ) | ((X * ) /\ (T . $1))) = ((I2 -TermEval ) | ((X * ) /\ (T . $1)));

      

       A3: P[ 0 ]

      proof

        set d = ((X * ) /\ (T . 0 ));

        (T . 0 ) c= TT & d c= (T . 0 ) by FOMODEL1: 2;

        then

        reconsider dd = d as Subset of TT by XBOOLE_1: 1;

        

         A4: ( dom (E1 | dd)) = d & ( dom (E2 | dd)) = d by PARTFUN1:def 2;

        now

          let x be object;

          assume

           A5: x in ( dom (E1 | d));

          reconsider dd as non empty Subset of TT by A5;

          reconsider xd = x as Element of dd by A5;

          reconsider t = x as 0 -termal string of S by A5, A4, FOMODEL1:def 33;

          set o = (F . t), ST = ( SubTerms t);

          reconsider XX = X as non empty set by A5;

          reconsider tx = x as non empty Element of (XX * ) by A5, A4;

          ( {(tx . 1)} \ XX) = {} ;

          then (tx . 1) in XX by ZFMISC_1: 60;

          then

          reconsider oo = o as Element of XX by FOMODEL0: 6;

          ((I11 . oo) \+\ (I1 . oo)) = {} & ((I22 . oo) \+\ (I2 . oo)) = {} & (((E1 | dd) . xd) \+\ (E1 . xd)) = {} & (((E2 | dd) . xd) \+\ (E2 . xd)) = {} ;

          then

           A6: (I11 . o) = (I1 . o) & (I22 . o) = (I2 . o) & ((E1 | d) . x) = (E1 . x) & ((E2 | d) . x) = (E2 . x) by FOMODEL0: 29;

          

          hence ((E1 | d) . x) = ((I1 . o) . (E1 * ST)) by Th21

          .= ((I2 . o) . (E2 * ST)) by A1, A6

          .= ((E2 | d) . x) by A6, Th21;

        end;

        hence thesis by A4, FUNCT_1: 2;

      end;

      

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

      proof

        let n;

        set d = ((X * ) /\ (T . n)), D = ((X * ) /\ (T . (n + 1)));

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

        assume

         A8: P[n];

        D c= (T . NN) & d c= (T . nn) & (T . nn) c= TT & (T . NN) c= TT by FOMODEL1: 2;

        then

        reconsider DD = D, dd = d as Subset of TT by XBOOLE_1: 1;

        

         A9: ( dom (E1 | dd)) = d & ( dom (E2 | dd)) = d & ( dom (E1 | DD)) = D & ( dom (E2 | DD)) = D by PARTFUN1:def 2;

        now

          let x be object;

          assume

           A10: x in ( dom (E1 | D));

          reconsider t = x as (nn + 1) -termal string of S by A10, A9, FOMODEL1:def 33;

          reconsider XX = X as non empty set by A10;

          reconsider DD as non empty Subset of TT by A10;

          reconsider tx = x as non empty Element of (XX * ) by A10, A9;

          reconsider dx = x as Element of DD by A10;

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

          ( {(tx . 1)} \ XX) = {} ;

          then (tx . 1) in XX by ZFMISC_1: 60;

          then

          reconsider oo = o as Element of XX by FOMODEL0: 6;

          reconsider r = ( rng t) as Subset of X by A10, A9, RELAT_1:def 19;

          (r * ) c= (X * );

          then

          reconsider newords = (( rng t) * ) as non empty Subset of (X * );

          reconsider ST = ( SubTerms t) as newords -valuedm -element FinSequence;

          ((I11 . oo) \+\ (I1 . oo)) = {} & ((I22 . oo) \+\ (I2 . oo)) = {} ;

          then

           A11: (I11 . oo) = (I1 . oo) & (I22 . oo) = (I2 . oo) by FOMODEL0: 29;

          (((E1 | DD) . dx) \+\ (E1 . dx)) = {} & (((E2 | DD) . dx) \+\ (E2 . dx)) = {} ;

          then

           A12: ((E1 | D) . x) = (E1 . x) & ((E2 | D) . x) = (E2 . x) by FOMODEL0: 29;

          ( rng ST) c= (T . nn) & ( rng ST) c= (X * ) by RELAT_1:def 19;

          then

           A13: ((E1 | d) * ST) = (E1 * ST) & ((E2 | d) * ST) = (E2 * ST) by XBOOLE_1: 19, A9, RELAT_1: 165;

          then ((I1 . o) . ((E1 | d) * ST)) = (E1 . t) by Th21;

          hence ((E1 | D) . x) = ((E2 | D) . x) by A12, A8, A1, A11, A13, Th21;

        end;

        hence thesis by A9, FUNCT_1: 2;

      end;

      

       A14: for m holds P[m] from NAT_1:sch 2( A3, A7);

      set f1 = (E1 | (X * )), f2 = (E2 | (X * ));

      

       A15: ( dom f1) = ((X * ) /\ TT) & ( dom f2) = ((X * ) /\ TT) by RELAT_1: 61, A2;

      now

        let x be object;

        assume

         A16: x in ( dom f1);

        reconsider D = ((X * ) /\ TT) as non empty Subset of TT by A16, RELAT_1: 61, A2;

        reconsider t = x as termal string of S by A16, A15;

        set m = ( Depth t);

        reconsider t as m -termal string of S by FOMODEL1:def 40;

        

         A17: t in (X * ) & t in (T . m) by A16, FOMODEL1:def 33;

        reconsider Dm = ((X * ) /\ (T . m)) as non empty set by A17, XBOOLE_0:def 4;

        reconsider tt = t as Element of Dm by A17, XBOOLE_0:def 4;

        reconsider xx = x as Element of (X * ) by A16;

        set g1 = (E1 | Dm), g2 = (E2 | Dm);

        ((f1 . xx) \+\ (E1 . xx)) = {} & ((f2 . xx) \+\ (E2 . xx)) = {} & ((g1 . tt) \+\ (E1 . tt)) = {} & ((g2 . tt) \+\ (E2 . tt)) = {} ;

        then (f1 . x) = (E1 . x) & (f2 . x) = (E2 . x) & (g1 . x) = (E1 . x) & (g2 . x) = (E2 . x) by FOMODEL0: 29;

        hence (f1 . x) = (f2 . x) by A14;

      end;

      hence thesis by A15, FUNCT_1: 2;

    end;

    theorem :: FOMODEL2:25

     not l2 in ( rng p) implies ((((l2,u) ReassignIn I) -TermEval ) . p) = ((I -TermEval ) . p)

    proof

      set tt = p, II = (U -InterpretersOf S), I2 = ((l2,u) ReassignIn I), f2 = (l2 .--> ( {} .--> u));

      (tt null {} ) is ( {} \/ ( rng tt)) -valued FinSequence;

      then tt is FinSequence of ( rng tt) by FOMODEL0: 26;

      then

      reconsider ttt = tt as Element of (( rng tt) * );

      ((((I2 -TermEval ) | (( rng tt) * )) . ttt) \+\ ((I2 -TermEval ) . ttt)) = {} & ((((I -TermEval ) | (( rng tt) * )) . ttt) \+\ ((I -TermEval ) . ttt)) = {} ;

      then

       A1: (((I2 -TermEval ) | (( rng tt) * )) . tt) = ((I2 -TermEval ) . tt) & (((I -TermEval ) | (( rng tt) * )) . tt) = ((I -TermEval ) . tt) by FOMODEL0: 29;

      assume not l2 in ( rng tt);

      then {l2} misses ( rng tt) by ZFMISC_1: 50;

      then ( dom f2) misses ( rng tt);

      then (I2 | ( rng tt)) = (I | ( rng tt)) by FUNCT_4: 72;

      hence thesis by A1, Lm41;

    end;

    definition

      let X, S, s;

      :: FOMODEL2:def38

      attr s is X -occurring means

      : Def37: s in ( SymbolsOf (((( AllSymbolsOf S) * ) \ { {} }) /\ X));

    end

    definition

      let S, s;

      let X;

      :: FOMODEL2:def39

      attr X is s -containing means s in ( SymbolsOf ((( AllSymbolsOf S) * ) \ ( { {} } /\ X)));

    end

    notation

      let X, S, s;

      antonym s is X -absent for s is X -occurring;

    end

    notation

      let S, s, X;

      antonym X is s -free for X is s -containing;

    end

    registration

      let X be finite set;

      let S;

      cluster X -absent for literal Element of S;

      existence

      proof

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

        reconsider Y = (((SS * ) \ { {} }) /\ X) as FinSequence-membered Subset of X;

        reconsider Z = ( SymbolsOf Y) as finite set;

        reconsider free = (L \ Z) as infinite Subset of L;

        set ll = the Element of free;

        reconsider l = ll as literal Element of S by TARSKI:def 3;

        take l;

         not l in Z by XBOOLE_0:def 5;

        hence thesis;

      end;

    end

    

     Lm42: w is termal implies (( rng w) /\ ( LettersOf S)) <> {}

    proof

      set L = ( LettersOf S), F = (S -firstChar ), TT = ( AllTermsOf S), C = (S -multiCat ), SS = ( AllSymbolsOf S), CC = (SS -multiCat ), T = (S -termsOfMaxDepth );

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

      defpred P[ Nat] means for w st w is $1 -termal holds (( rng w) /\ L) <> {} ;

      

       A1: P[ 0 ]

      proof

        let w;

        assume w is 0 -termal;

        then

        reconsider t0 = w as 0 -termal string of S;

        reconsider l = (F . t0) as literal Element of S;

        reconsider ll = l as Element of L by FOMODEL1:def 14;

        t0 = ( <*l*> ^ (C . ( SubTerms t0))) by FOMODEL1:def 37

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

        .= <*l*>;

        then (( rng t0) /\ L) = ( {ll} null L) by FINSEQ_1: 38;

        hence thesis;

      end;

      

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

      proof

        let k;

        reconsider kk = k as Element of NAT by ORDINAL1:def 12;

        assume

         A3: P[k];

        let w;

        assume w is (k + 1) -termal;

        then

        reconsider t = w as (k + 1) -termal string of S;

        per cases ;

          suppose not t is 0 -termal;

          then (F . t) is operational by FOMODEL1: 16;

          then

          reconsider n = |.( ar (F . t)).| as non zero Nat;

          consider m such that

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

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

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

          reconsider ST = ( SubTerms t) as (m + 1) -element Element of (TT * ) by A4;

          ST is ((m + 1) + 0 ) -element;

          then ( {(ST . (m + 1))} \ TT) = {} ;

          then

          reconsider q = (ST . (m + 1)) as Element of TTT by ZFMISC_1: 60;

          q is Element of (SS * ) by TARSKI:def 3;

          then

          reconsider qq = q as SS -valued FinSequence;

          reconsider p = (ST | ( Seg m)) as TTT -valued FinSequence;

          (((ST | ( Seg m)) ^ <*(ST . (m + 1))*>) \+\ ST) = {} ;

          then

           A5: ST = (p ^ <*qq*>) by FOMODEL0: 29;

          

           A6: (C . ST) = ((C . p) ^ qq) by A5, FOMODEL0: 33;

          t = ( <*(F . t)*> ^ ((C . p) ^ qq)) by FOMODEL1:def 37, A6;

          

          then ( rng t) = (( rng <*(F . t)*>) \/ ( rng ((C . p) ^ qq))) by FINSEQ_1: 31

          .= ( {(F . t)} \/ ( rng ((C . p) ^ qq))) by FINSEQ_1: 38

          .= ( {(F . t)} \/ (( rng (C . p)) \/ ( rng qq))) by FINSEQ_1: 31

          .= (( rng qq) \/ ( {(F . t)} \/ ( rng (C . p)))) by XBOOLE_1: 4;

          then (( rng qq) null ( {(F . t)} \/ ( rng (C . p)))) c= ( rng t);

          then

           A7: (( rng q) /\ L) c= (( rng t) /\ L) by XBOOLE_1: 26;

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

          then

          reconsider STT = ST as (T . kk) -valued((m + 1) + 0 ) -element FinSequence;

          ( {(STT . (m + 1))} \ (T . kk)) = {} ;

          then

          reconsider qqq = q as Element of (T . kk) by ZFMISC_1: 60;

          reconsider tq = qqq as k -termal string of S by FOMODEL1:def 33;

          (( rng tq) /\ L) <> {} by A3;

          hence thesis by A7;

        end;

          suppose t is 0 -termal;

          hence thesis by A1;

        end;

      end;

      

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

      assume w is termal;

      then

      reconsider t = w as termal string of S;

      t is ( Depth t) -termal by FOMODEL1:def 40;

      hence thesis by A8;

    end;

    registration

      let S, t;

      cluster (( rng t) /\ ( LettersOf S)) -> non empty;

      coherence by Lm42;

    end

    

     Lm43: w is wff implies (( rng w) /\ ( LettersOf S)) <> {}

    proof

      set L = ( LettersOf S), F = (S -firstChar ), TT = ( AllTermsOf S), C = (S -multiCat ), SS = ( AllSymbolsOf S), CC = (SS -multiCat ), T = (S -termsOfMaxDepth );

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

      defpred P[ Nat] means for w st w is $1 -wff holds (( rng w) /\ L) <> {} ;

      

       A1: P[ 0 ]

      proof

        let w;

        assume w is 0 -wff;

        then

        reconsider phi0 = w as 0wff string of S;

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

        reconsider n = |.( ar r).| as non zero Nat;

        consider m such that

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

        reconsider ST = ( SubTerms phi0) as ((m + 1) + 0 ) -element Element of (TT * ) by A2;

        reconsider p = (ST | ( Seg m)) as (SS * ) -valued FinSequence;

        ( {(ST . (m + 1))} \ TT) = {} ;

        then

        reconsider q = (ST . (m + 1)) as Element of TT by ZFMISC_1: 60;

        reconsider t = q as termal string of S;

        (((ST | ( Seg m)) ^ <*q*>) \+\ ST) = {} ;

        then

         A3: ST = ((ST | ( Seg m)) ^ <*q*>) by FOMODEL0: 29;

        reconsider qq = q as SS -valued FinSequence;

        phi0 = ( <*r*> ^ (C . ST)) by FOMODEL1:def 38

        .= ( <*r*> ^ ((C . p) ^ qq)) by A3, FOMODEL0: 33;

        

        then ( rng phi0) = (( rng <*r*>) \/ ( rng ((C . p) ^ q))) by FINSEQ_1: 31

        .= (( rng <*r*>) \/ (( rng (C . p)) \/ ( rng q))) by FINSEQ_1: 31

        .= (( rng q) \/ (( rng <*r*>) \/ ( rng (C . p)))) by XBOOLE_1: 4;

        then (( rng t) null (( rng <*r*>) \/ ( rng (C . p)))) c= ( rng phi0);

        then (( rng t) /\ L) c= (( rng phi0) /\ L) by XBOOLE_1: 26;

        hence thesis;

      end;

      

       A4: for k st P[k] holds P[(k + 1)]

      proof

        let k;

        assume

         A5: P[k];

        let w;

        assume w is (k + 1) -wff;

        then

        reconsider phi = w as (k + 1) -wff string of S;

        per cases ;

          suppose not phi is 0wff;

          then

          reconsider phii = phi as non 0wff wff string of S;

          reconsider phi1 = ( head phii) as k -wff string of S;

          phii = (( <*(F . phii)*> ^ phi1) ^ ( tail phi)) by Th23;

          

          then ( rng phii) = (( rng ( <*(F . phii)*> ^ phi1)) \/ ( rng ( tail phi))) by FINSEQ_1: 31

          .= ((( rng phi1) \/ ( rng <*(F . phii)*>)) \/ ( rng ( tail phi))) by FINSEQ_1: 31

          .= (( rng phi1) \/ (( rng <*(F . phii)*>) \/ ( rng ( tail phi)))) by XBOOLE_1: 4;

          then (( rng phi1) null (( rng <*(F . phii)*>) \/ ( rng ( tail phi)))) c= ( rng phii);

          then (( rng phi1) /\ L) c= (( rng phii) /\ L) by XBOOLE_1: 26;

          hence thesis by A5, XBOOLE_1: 3;

        end;

          suppose phi is 0wff;

          hence thesis by A1;

        end;

      end;

      

       A6: for m holds P[m] from NAT_1:sch 2( A1, A4);

      assume w is wff;

      then

      reconsider phi = w as wff string of S;

      phi is ( Depth phi) -wff by Def30;

      hence thesis by A6;

    end;

    registration

      let S, phi;

      cluster (( rng phi) /\ ( LettersOf S)) -> non empty;

      coherence by Lm43;

    end

    registration

      let B, S;

      let A be Subset of B;

      cluster A -occurring -> B -occurring for Element of S;

      coherence

      proof

        set SS = ( AllSymbolsOf S), DA = (A /\ ((SS * ) \ { {} })), DB = (B /\ ((SS * ) \ { {} }));

        reconsider Y = DB as functional set;

        reconsider X = DA as Subset of Y by XBOOLE_1: 26;

        

         A1: ( SymbolsOf X) c= ( SymbolsOf Y) by FOMODEL0: 46;

        let s be Element of S;

        assume s is A -occurring;

        then s in ( SymbolsOf X);

        hence s is B -occurring by A1;

      end;

    end

    registration

      let A, B, S;

      cluster (A null B) -absent -> (A /\ B) -absent for Element of S;

      coherence ;

    end

    registration

      let F be finite set;

      let A, S;

      cluster A -absent -> (A \/ F) -absent for F -absent Element of S;

      coherence

      proof

        set SS = ( AllSymbolsOf S), strings = ((SS * ) \ { {} });

        reconsider DA = (strings /\ A), DF = (strings /\ F) as Subset of strings;

        reconsider D = (DA \/ DF) as Subset of strings;

        

         A1: D = (strings /\ (A \/ F)) by XBOOLE_1: 23;

        let s be F -absent Element of S;

        assume s is A -absent;

        then not s in ( SymbolsOf DA) & not s in ( SymbolsOf DF) by Def37;

        then not s in (( SymbolsOf DA) \/ ( SymbolsOf DF)) by XBOOLE_0:def 3;

        then not s in ( SymbolsOf D) by FOMODEL0: 47;

        hence thesis by A1;

      end;

    end

    registration

      let S, U;

      let I be S, U -interpreter-like Function;

      cluster (( OwnSymbolsOf S) \ ( dom I)) -> empty;

      coherence

      proof

        ( OwnSymbolsOf S) c= ( dom I) by Lm2;

        hence thesis;

      end;

    end

    theorem :: FOMODEL2:26

    ex u st u = ((I . l) . {} ) & ((l,u) ReassignIn I) = I

    proof

      set O = ( OwnSymbolsOf S);

      (O \ ( dom I)) = {} ;

      then

       A1: O c= ( dom I) & { {} } = { {} } by XBOOLE_1: 37;

      reconsider lo = l as Element of O by FOMODEL1:def 19;

      reconsider i = (I . l) as Interpreter of l, U;

      i is Function of ( 0 -tuples_on U), U & ( 0 -tuples_on U) = { {} } by FOMODEL0: 10, Def2;

      then

      reconsider ii = i as Function of { {} }, U;

      reconsider e = {} as Element of { {} } by TARSKI:def 1;

      reconsider u = (ii . e) as Element of U;

      take u;

      thus u = ((I . l) . {} );

      set h = ( {} .--> u), H = (l .--> h), J = ((l,u) ReassignIn I);

      h = ( { {} } --> u);

      then

      reconsider hh = h as Function of { {} }, U;

      

       A2: ( dom H) = {lo};

      then

       A3: ( dom H) c= ( dom I) by A1;

      for z be Element of { {} } holds (ii . z) = (hh . z);

      then

       A4: ii = hh by FUNCT_2: 63;

      now

        let z be object;

        assume

         A5: z in ( dom H);

        

        thus (H . z) = h by FUNCOP_1: 7, A5

        .= (I . z) by A4, A5, TARSKI:def 1;

      end;

      then H tolerates I by PARTFUN1: 53, A3;

      

      then J = (H +* I) by FUNCT_4: 34

      .= I by A2, A1, XBOOLE_1: 1, FUNCT_4: 19;

      hence thesis;

    end;

    definition

      let S, X;

      :: FOMODEL2:def40

      attr X is S -covering means for phi holds (phi in X or ( xnot phi) in X);

    end

    registration

      let S;

      cluster S -mincover -> S -covering for set;

      coherence ;

    end

    registration

      let U, S;

      let phi be non 0wff non exal wff string of S;

      let I be Element of (U -InterpretersOf S);

      cluster ((I -TruthEval phi) \+\ ((I -TruthEval ( head phi)) 'nor' (I -TruthEval ( tail phi)))) -> empty;

      coherence

      proof

        set h = ( head phi), t = ( tail phi), A = (I -TruthEval phi), B = (I -TruthEval h), C = (I -TruthEval t), RH = (B 'nor' C), F = (S -firstChar ), l = (F . phi), N = ( TheNorSymbOf S);

        (l \+\ N) = {} ;

        then l = N by FOMODEL0: 29;

        then

         A1: phi = (( <*N*> ^ h) ^ t) by Th23;

        RH = A

        proof

          per cases ;

            suppose

             A2: not RH = 0 ;

             not B = 1 & not C = 1 by A2;

            then B = 0 & C = 0 by FOMODEL0: 39;

            hence thesis by A1, Lm37;

          end;

            suppose

             A3: RH = 0 ;

            then (1 - B) = 0 or (1 - C) = 0 ;

            then not A = 1 by A1, Lm37;

            hence thesis by A3, FOMODEL0: 39;

          end;

        end;

        hence thesis;

      end;

    end

    definition

      let S;

      :: FOMODEL2:def41

      func ExFormulasOf S -> Subset of ((( AllSymbolsOf S) * ) \ { {} }) equals { phi where phi be string of S : phi is wff & phi is exal };

      coherence

      proof

        set SS = ( AllSymbolsOf S), strings = ((SS * ) \ { {} });

        defpred P[ string of S] means $1 is wff & $1 is exal;

        defpred Q[ set] means not contradiction;

        deffunc F( set) = $1;

        

         A1: for w holds P[w] implies Q[w];

        set IT = { F(w) : P[w] };

        IT c= { F(w) : Q[w] } from FRAENKEL:sch 1( A1);

        hence thesis by DOMAIN_1: 18;

      end;

    end

    registration

      let S;

      cluster ( ExFormulasOf S) -> non empty;

      coherence

      proof

         the exal wff string of S in ( ExFormulasOf S);

        hence thesis;

      end;

    end

    registration

      let S;

      cluster -> exal wff for Element of ( ExFormulasOf S);

      coherence

      proof

        set EF = ( ExFormulasOf S);

        let x be Element of ( ExFormulasOf S);

        x in EF;

        then

        consider w such that

         A1: x = w & w is wff & w is exal;

        reconsider phi = x as exal wff string of S by A1;

        phi is exal wff string of S;

        hence thesis;

      end;

    end

    registration

      let S;

      cluster -> wff for Element of ( ExFormulasOf S);

      coherence ;

    end

    registration

      let S;

      cluster -> exal for Element of ( ExFormulasOf S);

      coherence ;

    end

    registration

      let S;

      cluster (( ExFormulasOf S) \ ( AllFormulasOf S)) -> empty;

      coherence

      proof

        set EF = ( ExFormulasOf S), FF = ( AllFormulasOf S);

        for x be object st x in EF holds x in FF by Th16;

        then EF c= FF;

        hence thesis;

      end;

    end

    registration

      let U, S1;

      let S2 be S1 -extending Language;

      cluster S2, U -interpreter-like -> S1, U -interpreter-like for Function;

      coherence

      proof

        set O1 = ( OwnSymbolsOf S1), O2 = ( OwnSymbolsOf S2), a1 = the adicity of S1, a2 = the adicity of S2, AS1 = ( AtomicFormulaSymbolsOf S1), E2 = ( TheEqSymbOf S2), AS2 = ( AtomicFormulaSymbolsOf S2), E1 = ( TheEqSymbOf S1);

        let I2 be Function;

        assume I2 is S2, U -interpreter-like;

        then

        reconsider I222 = I2 as S2, U -interpreter-like Function;

        reconsider I22 = I222 as Interpreter of S2, U by Def4;

        (O1 \ O2) = {} ;

        then

         A1: O1 c= O2 & ( dom a1) = AS1 & ( dom a2) = AS2 by XBOOLE_1: 37, FUNCT_2:def 1;

        a1 c= a2 by FOMODEL1:def 41;

        then

         A2: ( dom a1) c= ( dom a2) by RELAT_1: 11;

        now

          let s1 be own Element of S1;

          

           A3: s1 in AS1 by FOMODEL1:def 20;

          then

           A4: s1 in ( dom a1) by FUNCT_2:def 1;

          s1 in AS2 by A3, A2, A1;

          then

          reconsider s2 = s1 as ofAtomicFormula Element of S2 by FOMODEL1:def 20;

          s1 <> E1;

          then s2 <> E2 & s2 <> ( TheNorSymbOf S2) by FOMODEL1:def 41;

          then s2 is Element of O2 by FOMODEL1: 15;

          then

          reconsider s2 as own Element of S2 by FOMODEL1:def 19;

          reconsider i2 = (I22 . s2) as Interpreter of s2, U by Def3;

          set m2 = ( ar s2), m1 = ( ar s1);

          (a2 . s2) = ((a2 +* a1) . s2) by FUNCT_4: 98, FOMODEL1:def 41

          .= (a1 . s2) by FUNCT_4: 13, A4;

          then

           A5: m1 = m2;

          per cases ;

            suppose s2 is relational;

            then s1 is relational & i2 is Function of ( |.m1.| -tuples_on U), BOOLEAN by A5, Def2;

            hence (I2 . s1) is Interpreter of s1, U by Def2;

          end;

            suppose not s2 is relational;

            then i2 is Function of ( |.m1.| -tuples_on U), U & not s1 is relational by A5, Def2;

            hence (I2 . s1) is Interpreter of s1, U by Def2;

          end;

        end;

        then I2 is Interpreter of S1, U & I222 is Function-yielding by Def3;

        hence thesis;

      end;

    end

    registration

      let U, S1;

      let S2 be S1 -extending Language;

      let I be S2, U -interpreter-like Function;

      cluster (I | ( OwnSymbolsOf S1)) -> S1, U -interpreter-like;

      coherence ;

    end

    registration

      let U, S1;

      let S2 be S1 -extending Language, I1 be Element of (U -InterpretersOf S1), I2 be S2, U -interpreter-like Function;

      cluster (I2 +* I1) -> S2, U -interpreter-like;

      coherence

      proof

        set IT = (I2 +* I1), O1 = ( OwnSymbolsOf S1), O2 = ( OwnSymbolsOf S2), a1 = the adicity of S1, a2 = the adicity of S2, AS1 = ( AtomicFormulaSymbolsOf S1);

        now

          let s2 be own Element of S2;

          per cases ;

            suppose s2 in ( dom I1);

            then

             A1: s2 in O1 & (IT . s2) = (I1 . s2) by FUNCT_4: 13;

            then

            reconsider s1 = s2 as own Element of S1 by FOMODEL1:def 19;

            s1 in AS1 by FOMODEL1:def 20;

            then

             A2: s1 in ( dom a1) by FUNCT_2:def 1;

            reconsider i1 = (I1 . s1) as Interpreter of s1, U;

            set m2 = ( ar s2), m1 = ( ar s1);

            (a2 . s2) = ((a2 +* a1) . s2) by FOMODEL1:def 41, FUNCT_4: 98

            .= (a1 . s2) by FUNCT_4: 13, A2;

            then

             A3: m1 = m2;

            per cases ;

              suppose s1 is relational;

              then s2 is relational & i1 is Function of ( |.m2.| -tuples_on U), BOOLEAN by A3, Def2;

              hence (IT . s2) is Interpreter of s2, U by A1, Def2;

            end;

              suppose not s1 is relational;

              then i1 is Function of ( |.m2.| -tuples_on U), U & not s2 is relational by A3, Def2;

              hence (IT . s2) is Interpreter of s2, U by Def2, A1;

            end;

          end;

            suppose not s2 in ( dom I1);

            then (IT . s2) = (I2 . s2) by FUNCT_4: 11;

            hence (IT . s2) is Interpreter of s2, U;

          end;

        end;

        then IT is Interpreter of S2, U by Def3;

        hence thesis;

      end;

    end

    definition

      let U, S;

      let I be Element of (U -InterpretersOf S);

      let X;

      :: FOMODEL2:def42

      attr X is I -satisfied means

      : Def41: for phi st phi in X holds (I -TruthEval phi) = 1;

    end

    definition

      let S, U, X;

      let I be Element of (U -InterpretersOf S);

      :: FOMODEL2:def43

      attr I is X -satisfying means X is I -satisfied;

    end

    registration

      let U, S;

      let e be empty set;

      let I be Element of (U -InterpretersOf S);

      cluster (e null I) -> I -satisfied;

      coherence ;

    end

    registration

      let X, U, S;

      let I be Element of (U -InterpretersOf S);

      cluster I -satisfied for Subset of X;

      existence

      proof

        reconsider e = ( {} null I) as Subset of X by XBOOLE_1: 2;

        take e;

        thus thesis;

      end;

    end

    registration

      let U, S;

      let I be Element of (U -InterpretersOf S);

      cluster I -satisfied for set;

      existence

      proof

        take the I -satisfied Subset of the set;

        thus thesis;

      end;

    end

    registration

      let U, S;

      let I be Element of (U -InterpretersOf S);

      let X be I -satisfied set;

      cluster -> I -satisfied for Subset of X;

      coherence by Def41;

    end

    registration

      let U, S;

      let I be Element of (U -InterpretersOf S);

      let X,Y be I -satisfied set;

      cluster (X \/ Y) -> I -satisfied;

      coherence

      proof

        now

          let phi;

          assume phi in (X \/ Y);

          then phi in X or phi in Y by XBOOLE_0:def 3;

          hence (I -TruthEval phi) = 1 by Def41;

        end;

        hence thesis;

      end;

    end

    registration

      let U, S;

      let I be Element of (U -InterpretersOf S);

      let X be I -satisfied set;

      cluster (I null X) -> X -satisfying;

      coherence ;

    end

    definition

      let S, X;

      :: FOMODEL2:def44

      attr X is S -correct means for U be non empty set, I be Element of (U -InterpretersOf S), x be I -satisfied set, phi st [x, phi] in X holds (I -TruthEval phi) = 1;

    end

    registration

      let S;

      cluster ( {} null S) -> S -correct;

      coherence ;

    end

    registration

      let S, X;

      cluster S -correct for Subset of X;

      existence

      proof

        reconsider IT = ( {} null S) as Subset of X by XBOOLE_1: 2;

        take IT;

        thus IT is S -correct;

      end;

    end

    theorem :: FOMODEL2:27

    for I be Element of (U -InterpretersOf S) holds (I -TruthEval phi) = 1 iff {phi} is I -satisfied

    proof

      let I be Element of (U -InterpretersOf S);

      thus (I -TruthEval phi) = 1 implies {phi} is I -satisfied by TARSKI:def 1;

      assume {phi} is I -satisfied;

      then

      reconsider X = {phi} as I -satisfied set;

      phi in X by TARSKI:def 1;

      hence (I -TruthEval phi) = 1 by Def41;

    end;

    theorem :: FOMODEL2:28

    s is {w} -occurring iff s in ( rng w) by FOMODEL0: 45;

    registration

      let U, S;

      let phi1, phi2;

      let I be Element of (U -InterpretersOf S);

      cluster ((I -TruthEval (( <*( TheNorSymbOf S)*> ^ phi1) ^ phi2)) \+\ ((I -TruthEval phi1) 'nor' (I -TruthEval phi2))) -> empty;

      coherence

      proof

        set F = (S -firstChar ), N = ( TheNorSymbOf S), phi = (( <*N*> ^ phi1) ^ phi2), A = (I -TruthEval phi), A1 = (I -TruthEval phi1), A2 = (I -TruthEval phi2), h = ( head phi), t = ( tail phi), H = (I -TruthEval h), T = (I -TruthEval t);

        phi1 = h & phi2 = t by Th23;

        hence thesis;

      end;

    end

    registration

      let S, phi, U;

      let I be Element of (U -InterpretersOf S);

      cluster ((I -TruthEval ( xnot phi)) \+\ ( 'not' (I -TruthEval phi))) -> empty;

      coherence

      proof

        set N = ( TheNorSymbOf S), v1 = (I -TruthEval phi), psi = ( xnot phi);

        ((I -TruthEval psi) \+\ (v1 'nor' v1)) = {} ;

        hence thesis;

      end;

    end

    definition

      let X, S, phi;

      :: FOMODEL2:def45

      attr phi is X -implied means for U be non empty set, I be Element of (U -InterpretersOf S) st X is I -satisfied holds (I -TruthEval phi) = 1;

    end

    registration

      let S, l, phi;

      cluster (( head ( <*l*> ^ phi)) \+\ phi) -> empty;

      coherence

      proof

        set Phi = ( <*l*> ^ phi);

        Phi = (( <*l*> ^ phi) null {} )

        .= (( <*l*> ^ phi) ^ {} );

        then phi = ( head Phi) by Th23;

        hence thesis;

      end;

    end