henmodel.miz



    begin

    reserve Al for QC-alphabet;

    reserve a,a1,a2,b,c,d for set,

X,Y,Z for Subset of ( CQC-WFF Al),

i,k,m,n for Nat,

p,q for Element of ( CQC-WFF Al),

P for QC-pred_symbol of k, Al,

ll for CQC-variable_list of k, Al,

f,f1,f2,g for FinSequence of ( CQC-WFF Al);

    reserve A for non empty finite Subset of NAT ;

    theorem :: HENMODEL:1

    

     Th1: for f be Function of n, A st ((ex m st ( succ m) = n) & ( rng f) = A & for n, m st m in ( dom f) & n in ( dom f) & n < m holds (f . n) in (f . m)) holds (f . ( union n)) = ( union ( rng f))

    proof

      let f be Function of n, A such that

       A1: ex m st ( succ m) = n and

       A2: ( rng f) = A and

       A3: for n, m st m in ( dom f) & n in ( dom f) & n < m holds (f . n) in (f . m);

      thus (f . ( union n)) c= ( union ( rng f))

      proof

        let a be object;

        consider m such that

         A4: n = ( succ m) by A1;

        ( dom f) = n by FUNCT_2:def 1;

        then

         A5: (f . m) in ( rng f) by A4, FUNCT_1: 3, ORDINAL1: 6;

        assume a in (f . ( union n));

        then a in (f . m) by A4, ORDINAL2: 2;

        hence thesis by A5, TARSKI:def 4;

      end;

      thus ( union ( rng f)) c= (f . ( union n))

      proof

        let a be object;

        assume a in ( union ( rng f));

        then

        consider b such that

         A6: a in b and

         A7: b in ( rng f) by TARSKI:def 4;

        consider c be object such that

         A8: c in ( dom f) and

         A9: (f . c) = b by A7, FUNCT_1:def 3;

        ( dom f) = n by PARTFUN1:def 2;

        then

         A10: ( dom f) in NAT by ORDINAL1:def 12;

        reconsider i = c as Ordinal by A8;

        reconsider i as Element of NAT by A8, ORDINAL1: 10, A10;

        consider m such that

         A11: n = ( succ m) by A1;

        i c= m by A8, A11, ORDINAL1: 22;

        then i c< m or i = m;

        then

         A12: i in m or i = m by ORDINAL1: 11;

        

         A13: ( dom f) = n by FUNCT_2:def 1;

        then

         A14: m in ( dom f) by A11, ORDINAL1: 6;

         A15:

        now

          i in ( dom f) by A12, A13, A14, ORDINAL1: 10;

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

          then

          reconsider i1 = (f . i) as Nat by A2;

          (f . m) in ( rng f) by A11, A13, FUNCT_1: 3, ORDINAL1: 6;

          then

          reconsider i2 = (f . m) as Nat by A2;

          assume (f . i) in (f . m);

          then i1 c= i2 by ORDINAL1:def 2;

          then a in i2 by A6, A9;

          hence thesis by A11, ORDINAL2: 2;

        end;

        i in { k where k be Nat : k < m } or i = m by A12, AXIOMS: 4;

        then (ex k be Nat st k = i & k < m) or i = m;

        hence thesis by A3, A6, A8, A9, A11, A14, A15, ORDINAL2: 2;

      end;

    end;

    theorem :: HENMODEL:2

    

     Th2: ( union A) in A & for a st a in A holds (a in ( union A) or a = ( union A))

    proof

      consider a be Ordinal such that

       A1: (( RelIncl A),( RelIncl a)) are_isomorphic by WELLORD2: 8, WELLORD2: 13;

      consider F1 be Function such that

       A2: F1 is_isomorphism_of (( RelIncl A),( RelIncl a)) by A1, WELLORD1:def 8;

      

       A3: ( dom F1) = ( field ( RelIncl A)) by A2, WELLORD1:def 7;

      then ( dom F1) = A by WELLORD2:def 1;

      then

      consider b be object such that

       A4: b in ( dom F1) by XBOOLE_0:def 1;

      ( rng F1) is finite by A3, FINSET_1: 8;

      then ( field ( RelIncl a)) is finite by A2, WELLORD1:def 7;

      then

       A5: a is finite by WELLORD2:def 1;

      (F1 . b) in ( rng F1) by A4, FUNCT_1: 3;

      then ( field ( RelIncl a)) is non empty by A2, WELLORD1:def 7;

      then a is non empty by WELLORD2:def 1;

      then

       A6: {} in a by ORDINAL1: 16, XBOOLE_1: 3;

       A7:

      now

        assume a is limit_ordinal;

        then omega c= a by A6, ORDINAL1:def 11;

        hence contradiction by A5;

      end;

      (( RelIncl a),( RelIncl A)) are_isomorphic by A1, WELLORD1: 40;

      then

      consider F be Function such that

       A8: F is_isomorphism_of (( RelIncl a),( RelIncl A)) by WELLORD1:def 8;

      

       A9: for m, n st m in ( dom F) & n in ( dom F) & n < m holds (F . n) in (F . m)

      proof

        let m, n such that

         A10: m in ( dom F) and

         A11: n in ( dom F) and

         A12: n < m;

        (F . n) in ( rng F) by A11, FUNCT_1: 3;

        then (F . n) in ( field ( RelIncl A)) by A8, WELLORD1:def 7;

        then

         A13: (F . n) in A by WELLORD2:def 1;

        then

        reconsider b = (F . n) as Nat;

        n in ( field ( RelIncl a)) by A8, A11, WELLORD1:def 7;

        then

         A14: n in a by WELLORD2:def 1;

        (F . m) in ( rng F) by A10, FUNCT_1: 3;

        then (F . m) in ( field ( RelIncl A)) by A8, WELLORD1:def 7;

        then

         A15: (F . m) in A by WELLORD2:def 1;

        then

        reconsider c = (F . m) as Nat;

        n in { i where i be Nat : i < m } by A12;

        then n in m by AXIOMS: 4;

        then

         A16: n c= m by ORDINAL1:def 2;

        m in ( field ( RelIncl a)) by A8, A10, WELLORD1:def 7;

        then m in a by WELLORD2:def 1;

        then [n, m] in ( RelIncl a) by A14, A16, WELLORD2:def 1;

        then [(F . n), (F . m)] in ( RelIncl A) by A8, WELLORD1:def 7;

        then

         A17: (F . n) c= (F . m) by A13, A15, WELLORD2:def 1;

        F is one-to-one by A8, WELLORD1:def 7;

        then (F . n) <> (F . m) by A10, A11, A12;

        then (F . n) c< (F . m) by A17;

        then b in c by ORDINAL1: 11;

        hence thesis;

      end;

      reconsider a as Nat by A5;

      ( dom F) = ( field ( RelIncl a)) by A8, WELLORD1:def 7;

      then

       A18: ( dom F) = a by WELLORD2:def 1;

       A19:

      now

        let b be Ordinal;

        

         A20: a in NAT by ORDINAL1:def 12;

        assume ( succ b) = a;

        then b in a by ORDINAL1: 6;

        hence b in NAT by ORDINAL1: 10, A20;

      end;

      

       A21: ex m st ( succ m) = a

      proof

        consider b be Ordinal such that

         A22: ( succ b) = a by A7, ORDINAL1: 29;

        reconsider b as Element of NAT by A19, A22;

        take b;

        thus thesis by A22;

      end;

      then

      consider m such that

       A23: ( succ m) = a;

      

       A24: ( rng F) = ( field ( RelIncl A)) by A8, WELLORD1:def 7;

      then

       A25: ( rng F) = A by WELLORD2:def 1;

      then

      reconsider F as Function of a, A by A18, FUNCT_2: 1;

      

       A26: for n, m st m in ( dom F) & n in ( dom F) & n < m holds (F . n) in (F . m) by A9;

      ( rng F) = A by A24, WELLORD2:def 1;

      then

       A27: (F . ( union a)) = ( union ( rng F)) by A21, A26, Th1;

      

       A28: ( union a) = m by A23, ORDINAL2: 2;

      hence ( union A) in A by A25, A18, A23, A27, FUNCT_1: 3, ORDINAL1: 6;

      thus for b st b in A holds (b in ( union A) or b = ( union A))

      proof

        let b such that

         A29: b in A;

        now

          

           A30: m in ( dom F) by A18, A23, ORDINAL1: 6;

          assume

           A31: b <> ( union A);

          consider c be object such that

           A32: c in ( dom F) and

           A33: (F . c) = b by A25, A29, FUNCT_1:def 3;

          ( dom F) = a by PARTFUN1:def 2;

          then

           A34: ( dom F) in NAT by ORDINAL1:def 12;

          reconsider c as Element of NAT by A32, ORDINAL1: 10, A34;

          c in m or c = m by A23, A32, ORDINAL1: 8;

          then c in { k where k be Nat : k < m } by A25, A23, A27, A31, A33, AXIOMS: 4, ORDINAL2: 2;

          then ex k be Nat st k = c & k < m;

          hence thesis by A9, A25, A27, A28, A32, A33, A30;

        end;

        hence thesis;

      end;

    end;

    reserve C for non empty set;

    theorem :: HENMODEL:3

    

     Th3: for f be sequence of C, X be finite set st (for n, m st m in ( dom f) & n in ( dom f) & n < m holds (f . n) c= (f . m)) & X c= ( union ( rng f)) holds ex k st X c= (f . k)

    proof

      let f be sequence of C, X be finite set such that

       A1: for n, m st m in ( dom f) & n in ( dom f) & n < m holds (f . n) c= (f . m) and

       A2: X c= ( union ( rng f));

       A3:

      now

        deffunc F( object) = ( min* { i : $1 in (f . i) });

        consider g be Function such that

         A4: ( dom g) = X & for a be object st a in X holds (g . a) = F(a) from FUNCT_1:sch 3;

        reconsider A = ( rng g) as finite set by A4, FINSET_1: 8;

         A5:

        now

          let b be object;

          assume b in A;

          then

          consider a be object such that

           A6: a in ( dom g) & (g . a) = b by FUNCT_1:def 3;

          b = ( min* { i : a in (f . i) }) by A4, A6;

          hence b in NAT ;

        end;

        assume not X is empty;

        then ex c be object st c in ( dom g) by A4;

        then

        reconsider A as non empty finite Subset of NAT by A5, FUNCT_1: 3, TARSKI:def 3;

        ( union A) in A by Th2;

        then

        reconsider a = ( union A) as Nat;

        take a;

        thus X c= (f . a)

        proof

          let b be object;

          assume

           A7: b in X;

          then

          consider c such that

           A8: b in c and

           A9: c in ( rng f) by A2, TARSKI:def 4;

          consider d be object such that

           A10: d in ( dom f) and

           A11: (f . d) = c by A9, FUNCT_1:def 3;

          reconsider d as Nat by A10;

          d in { i : b in (f . i) } by A8, A11;

          then

          reconsider Y = { i : b in (f . i) } as non empty set;

          now

            let a be object;

            assume a in Y;

            then ex i st i = a & b in (f . i);

            hence a in NAT by ORDINAL1:def 12;

          end;

          then

          reconsider Y as non empty Subset of NAT by TARSKI:def 3;

          

           A12: (g . b) = ( min* Y) by A4, A7;

          then

          reconsider Y9 = (g . b) as Nat;

          Y9 in Y by A12, NAT_1:def 1;

          then

           A13: ex i st i = (g . b) & b in (f . i);

          

           A14: ( dom f) = NAT by FUNCT_2:def 1;

           A15:

          now

            assume Y9 in a;

            then Y9 in { k where k be Nat : k < a } by AXIOMS: 4;

            then

            consider k be Nat such that

             A16: k = Y9 & k < a;

            

             A17: a in NAT by ORDINAL1:def 12;

            Y9 in NAT by ORDINAL1:def 12;

            then (f . Y9) c= (f . a) by A1, A14, A16, A17;

            hence thesis by A13;

          end;

          Y9 in A by A4, A7, FUNCT_1: 3;

          hence thesis by A13, A15, Th2;

        end;

      end;

      now

        assume

         A18: X is empty;

        take k = 0 ;

         {} c= (f . k);

        hence thesis by A18;

      end;

      hence thesis by A3;

    end;

    definition

      let Al;

      let X, p;

      :: HENMODEL:def1

      pred X |- p means ex f st ( rng f) c= X & |- (f ^ <*p*>);

    end

    definition

      let Al;

      let X;

      :: HENMODEL:def2

      attr X is Consistent means for p holds not (X |- p & X |- ( 'not' p));

    end

    notation

      let Al;

      let X;

      antonym X is Inconsistent for X is Consistent;

    end

    definition

      let Al;

      let f be FinSequence of ( CQC-WFF Al);

      :: HENMODEL:def3

      attr f is Consistent means for p holds not ( |- (f ^ <*p*>) & |- (f ^ <*( 'not' p)*>));

    end

    notation

      let Al;

      let f be FinSequence of ( CQC-WFF Al);

      antonym f is Inconsistent for f is Consistent;

    end

    theorem :: HENMODEL:4

    

     Th4: X is Consistent & ( rng g) c= X implies g is Consistent

    proof

      assume that

       A1: X is Consistent and

       A2: ( rng g) c= X;

      now

        assume g is Inconsistent;

        then

        consider p such that

         A3: |- (g ^ <*p*>) & |- (g ^ <*( 'not' p)*>);

        X |- p & X |- ( 'not' p) by A2, A3;

        hence contradiction by A1;

      end;

      hence thesis;

    end;

    theorem :: HENMODEL:5

    

     Th5: |- (f ^ <*p*>) implies |- ((f ^ g) ^ <*p*>)

    proof

      

       A1: ( Ant (f ^ <*p*>)) = f & ( Ant ((f ^ g) ^ <*p*>)) = (f ^ g) by CALCUL_1: 5;

      ( Suc ((f ^ g) ^ <*p*>)) = p by CALCUL_1: 5;

      then

       A2: ( Suc (f ^ <*p*>)) = ( Suc ((f ^ g) ^ <*p*>)) by CALCUL_1: 5;

      assume |- (f ^ <*p*>);

      hence thesis by A1, A2, CALCUL_1: 8, CALCUL_1: 36;

    end;

    theorem :: HENMODEL:6

    

     Th6: X is Inconsistent iff for p holds X |- p

    proof

      thus X is Inconsistent implies for p holds X |- p

      proof

        assume X is Inconsistent;

        then

        consider q such that

         A1: X |- q and

         A2: X |- ( 'not' q);

        consider f2 such that

         A3: ( rng f2) c= X and

         A4: |- (f2 ^ <*( 'not' q)*>) by A2;

        let p;

        consider f1 such that

         A5: ( rng f1) c= X and

         A6: |- (f1 ^ <*q*>) by A1;

        take f3 = (f1 ^ f2);

        

         A7: ( rng f3) = (( rng f1) \/ ( rng f2)) by FINSEQ_1: 31;

        

         A8: |- ((f1 ^ f2) ^ <*( 'not' q)*>) by A4, CALCUL_2: 20;

         |- ((f1 ^ f2) ^ <*q*>) by A6, Th5;

        hence thesis by A5, A3, A8, A7, CALCUL_2: 25, XBOOLE_1: 8;

      end;

      assume for p holds X |- p;

      then X |- ( VERUM Al) & X |- ( 'not' ( VERUM Al));

      hence thesis;

    end;

    theorem :: HENMODEL:7

    

     Th7: X is Inconsistent implies ex Y st Y c= X & Y is finite & Y is Inconsistent

    proof

      assume X is Inconsistent;

      then

      consider p such that

       A1: X |- p and

       A2: X |- ( 'not' p);

      consider f1 such that

       A3: ( rng f1) c= X and

       A4: |- (f1 ^ <*p*>) by A1;

      consider f2 such that

       A5: ( rng f2) c= X and

       A6: |- (f2 ^ <*( 'not' p)*>) by A2;

      reconsider Y = ( rng (f1 ^ f2)) as Subset of ( CQC-WFF Al);

      take Y;

      Y = (( rng f1) \/ ( rng f2)) by FINSEQ_1: 31;

      hence Y c= X by A3, A5, XBOOLE_1: 8;

       |- ((f1 ^ f2) ^ <*( 'not' p)*>) by A6, CALCUL_2: 20;

      then

       A7: Y |- ( 'not' p);

       |- ((f1 ^ f2) ^ <*p*>) by A4, Th5;

      then Y |- p;

      hence thesis by A7;

    end;

    

     Lm1: for f,g be FinSequence holds ( Seg ( len (f ^ g))) = (( Seg ( len f)) \/ ( seq (( len f),( len g))))

    proof

      let f,g be FinSequence;

      

      thus ( Seg ( len (f ^ g))) = ( dom (f ^ g)) by FINSEQ_1:def 3

      .= (( dom f) \/ ( seq (( len f),( len g)))) by CALCUL_2: 9

      .= (( Seg ( len f)) \/ ( seq (( len f),( len g)))) by FINSEQ_1:def 3;

    end;

    theorem :: HENMODEL:8

    (X \/ {p}) |- q implies ex g st ( rng g) c= X & |- ((g ^ <*p*>) ^ <*q*>)

    proof

      assume (X \/ {p}) |- q;

      then

      consider f such that

       A1: ( rng f) c= (X \/ {p}) and

       A2: |- (f ^ <*q*>);

       A3:

      now

        set g = (f - {p});

        reconsider A = (f " {p}) as finite set;

        reconsider B = ( dom f) as finite set;

        set n = ( card A);

        set h = (g ^ ( IdFinS (p,n)));

        

         A4: ( len ( IdFinS (p,n))) = n by CARD_1:def 7;

        A c= B by RELAT_1: 132;

        then

         A5: A c= ( Seg ( len f)) by FINSEQ_1:def 3;

         A6:

        now

          let i;

          reconsider j = (i - ( len g)) as Integer;

          assume

           A7: i in ( seq (( len g),n));

          then

           A8: (1 + ( len g)) <= i by CALCUL_2: 1;

          then

           A9: 1 <= j by XREAL_1: 19;

          i <= (n + ( len g)) by A7, CALCUL_2: 1;

          then

           A10: j <= n by XREAL_1: 20;

           0 <= j by A8, XREAL_1: 19;

          then

          reconsider j as Element of NAT by INT_1: 3;

          j in ( Seg n) by A9, A10, FINSEQ_1: 1;

          hence (i - ( len g)) in ( dom ( Sgm A)) by A5, FINSEQ_3: 40;

        end;

        assume not ( rng f) c= X;

        then

        consider a be object such that

         A11: a in ( rng f) and

         A12: not a in X;

        a in X or a in {p} by A1, A11, XBOOLE_0:def 3;

        then a = p by A12, TARSKI:def 1;

        then

        consider i be Nat such that

         A13: i in B and

         A14: (f . i) = p by A11, FINSEQ_2: 10;

        reconsider C = (B \ A) as finite set;

        defpred P[ Nat, object] means ($1 in ( Seg ( len g)) implies $2 = (( Sgm (B \ A)) . $1)) & ($1 in ( seq (( len g),n)) implies $2 = (( Sgm A) . ($1 - ( len g))));

        

         A15: ( card C) = (( card B) - n) by CARD_2: 44, RELAT_1: 132

        .= (( card ( Seg ( len f))) - n) by FINSEQ_1:def 3

        .= (( len f) - n) by FINSEQ_1: 57

        .= ( len g) by FINSEQ_3: 59;

        

         A16: for k be Nat st k in ( Seg ( len h)) holds ex a be object st P[k, a]

        proof

          let k be Nat such that k in ( Seg ( len h));

          now

            assume

             A17: k in ( Seg ( len g));

            take a = (( Sgm (B \ A)) . k);

            ( Seg ( len g)) misses ( seq (( len g),n)) by CALCUL_2: 8;

            hence P[k, a] by A17, XBOOLE_0: 3;

          end;

          hence thesis;

        end;

        consider F be FinSequence such that

         A18: ( dom F) = ( Seg ( len h)) & for k be Nat st k in ( Seg ( len h)) holds P[k, (F . k)] from FINSEQ_1:sch 1( A16);

        now

          let b be object;

          assume b in C;

          then b in ( dom f);

          hence b in ( Seg ( len f)) by FINSEQ_1:def 3;

        end;

        then

         A19: C c= ( Seg ( len f));

        then

         A20: ( dom ( Sgm C)) = ( Seg ( card C)) by FINSEQ_3: 40;

        

         A21: ( rng F) = B

        proof

          now

            let a be object;

            assume a in ( rng F);

            then

            consider i be Nat such that

             A22: i in ( dom F) and

             A23: (F . i) = a by FINSEQ_2: 10;

             A24:

            now

              assume i in ( Seg ( len g));

              then a = (( Sgm C) . i) & i in ( dom ( Sgm C)) by A18, A19, A15, A22, A23, FINSEQ_3: 40;

              then a in ( rng ( Sgm C)) by FUNCT_1: 3;

              then a in C by A19, FINSEQ_1:def 13;

              hence a in B;

            end;

             A25:

            now

              

               A26: ( rng ( Sgm A)) = A by A5, FINSEQ_1:def 13;

              

               A27: A c= B by RELAT_1: 132;

              assume

               A28: i in ( seq (( len g),n));

              then a = (( Sgm A) . (i - ( len g))) by A18, A22, A23;

              then a in A by A6, A28, A26, FUNCT_1: 3;

              hence a in B by A27;

            end;

            i in (( Seg ( len g)) \/ ( seq (( len g),n))) by A4, A18, A22, Lm1;

            hence a in B by A24, A25, XBOOLE_0:def 3;

          end;

          hence ( rng F) c= B;

          let a be object such that

           A29: a in B;

           A30:

          now

            now

              let b be object;

              assume b in C;

              then b in ( dom f);

              hence b in ( Seg ( len f)) by FINSEQ_1:def 3;

            end;

            then

             A31: C c= ( Seg ( len f));

            assume not a in A;

            then a in C by A29, XBOOLE_0:def 5;

            then a in ( rng ( Sgm C)) by A31, FINSEQ_1:def 13;

            then

            consider i be Nat such that

             A32: i in ( dom ( Sgm C)) and

             A33: (( Sgm C) . i) = a by FINSEQ_2: 10;

            

             A34: 1 <= i by A32, FINSEQ_3: 25;

            ( len ( Sgm C)) = ( len g) by A20, A15, FINSEQ_1:def 3;

            then

             A35: i <= ( len g) by A32, FINSEQ_3: 25;

            ( len g) <= ( len h) by CALCUL_1: 6;

            then i <= ( len h) by A35, XXREAL_0: 2;

            then

             A36: i in ( Seg ( len h)) by A34, FINSEQ_1: 1;

            i in ( Seg ( len g)) by A34, A35, FINSEQ_1: 1;

            then a = (F . i) by A18, A33, A36;

            hence thesis by A18, A36, FUNCT_1: 3;

          end;

          now

            assume

             A37: a in A;

            ( rng ( Sgm A)) = A by A5, FINSEQ_1:def 13;

            then

            consider i be Nat such that

             A38: i in ( dom ( Sgm A)) and

             A39: (( Sgm A) . i) = a by A37, FINSEQ_2: 10;

            reconsider i as Nat;

            set m = (i + ( len g));

            ( len ( Sgm A)) = n by A5, FINSEQ_3: 39;

            then i <= n by A38, FINSEQ_3: 25;

            then

             A40: m <= (n + ( len g)) by XREAL_1: 6;

            then m <= (( len g) + ( len ( IdFinS (p,n)))) by CARD_1:def 7;

            then

             A41: m <= ( len h) by FINSEQ_1: 22;

            

             A42: 1 <= i by A38, FINSEQ_3: 25;

            then (1 + ( len g)) <= m by XREAL_1: 6;

            then

             A43: m in ( seq (( len g),n)) by A40, CALCUL_2: 1;

            i <= m by NAT_1: 11;

            then 1 <= m by A42, XXREAL_0: 2;

            then m in ( dom h) by A41, FINSEQ_3: 25;

            then

             A44: m in ( Seg ( len h)) by FINSEQ_1:def 3;

            a = (( Sgm A) . (m - ( len g))) by A39;

            then a = (F . m) by A18, A43, A44;

            hence thesis by A18, A44, FUNCT_1: 3;

          end;

          hence thesis by A30;

        end;

        

         A45: ( len h) = (( len g) + ( len ( IdFinS (p,n)))) by FINSEQ_1: 22

        .= ((( len f) - n) + ( len ( IdFinS (p,n)))) by FINSEQ_3: 59

        .= ((( len f) - n) + n) by CARD_1:def 7

        .= ( len f);

        then

         A46: ( dom F) = B by A18, FINSEQ_1:def 3;

        then

        reconsider F as Relation of B, B by A21, RELSET_1: 4;

        ( rng F) c= B;

        then

        reconsider F as Function of B, B by A46, FUNCT_2: 2;

        F is one-to-one

        proof

          let a1,a2 be object such that

           A47: a1 in ( dom F) and

           A48: a2 in ( dom F) and

           A49: (F . a1) = (F . a2);

          

           A50: a2 in (( Seg ( len g)) \/ ( seq (( len g),n))) by A4, A18, A48, Lm1;

           A51:

          now

            assume

             A52: a1 in ( Seg ( len g));

            then

             A53: a1 in ( dom ( Sgm C)) by A19, A15, FINSEQ_3: 40;

            (F . a1) = (( Sgm C) . a1) by A18, A47, A52;

            then (F . a1) in ( rng ( Sgm C)) by A53, FUNCT_1: 3;

            then

             A54: (F . a1) in C by A19, FINSEQ_1:def 13;

             A55:

            now

              assume

               A56: a2 in ( seq (( len g),n));

              then

              reconsider i = a2 as Nat;

              (( Sgm A) . (i - ( len g))) in ( rng ( Sgm A)) by A6, A56, FUNCT_1: 3;

              then (F . a2) in ( rng ( Sgm A)) by A18, A48, A56;

              then (F . a2) in A by A5, FINSEQ_1:def 13;

              hence contradiction by A49, A54, XBOOLE_0:def 5;

            end;

            now

              assume

               A57: a2 in ( Seg ( len g));

              then (F . a2) = (( Sgm C) . a2) by A18, A48;

              then

               A58: (( Sgm C) . a1) = (( Sgm C) . a2) by A18, A47, A49, A52;

              

               A59: ( Sgm C) is one-to-one by A19, FINSEQ_3: 92;

              a2 in ( dom ( Sgm C)) by A19, A15, A57, FINSEQ_3: 40;

              hence thesis by A53, A58, A59;

            end;

            hence thesis by A50, A55, XBOOLE_0:def 3;

          end;

           A60:

          now

            assume

             A61: a1 in ( seq (( len g),n));

            then

            reconsider i = a1 as Nat;

            

             A62: (i - ( len g)) in ( dom ( Sgm A)) by A6, A61;

             A63:

            now

              assume

               A64: a2 in ( seq (( len g),n));

              then

              reconsider i1 = a2 as Nat;

              (F . a2) = (( Sgm A) . (i1 - ( len g))) by A18, A48, A64;

              then

               A65: (( Sgm A) . (i1 - ( len g))) = (( Sgm A) . (i - ( len g))) by A18, A47, A49, A61;

              

               A66: ( Sgm A) is one-to-one by A5, FINSEQ_3: 92;

              (i1 - ( len g)) in ( dom ( Sgm A)) by A6, A64;

              then ((i1 - ( len g)) + ( len g)) = ((i - ( len g)) + ( len g)) by A62, A65, A66;

              hence thesis;

            end;

            (( Sgm A) . (i - ( len g))) in ( rng ( Sgm A)) by A6, A61, FUNCT_1: 3;

            then (F . a1) in ( rng ( Sgm A)) by A18, A47, A61;

            then

             A67: (F . a1) in A by A5, FINSEQ_1:def 13;

            now

              assume a2 in ( Seg ( len g));

              then (F . a2) = (( Sgm C) . a2) & a2 in ( dom ( Sgm C)) by A18, A19, A15, A48, FINSEQ_3: 40;

              then (F . a2) in ( rng ( Sgm C)) by FUNCT_1: 3;

              then (F . a2) in C by A19, FINSEQ_1:def 13;

              hence contradiction by A49, A67, XBOOLE_0:def 5;

            end;

            hence thesis by A50, A63, XBOOLE_0:def 3;

          end;

          a1 in (( Seg ( len g)) \/ ( seq (( len g),n))) by A4, A18, A47, Lm1;

          hence thesis by A51, A60, XBOOLE_0:def 3;

        end;

        then

        reconsider F as Permutation of ( dom f) by A21, FUNCT_2: 57;

        consider j be Nat such that

         A68: j in ( dom F) and

         A69: (F . j) = i by A21, A13, FINSEQ_2: 10;

        

         A70: ( dom ( Per (f,F))) = B by CALCUL_2: 19

        .= ( dom F) by A18, A45, FINSEQ_1:def 3

        .= ( dom h) by A18, FINSEQ_1:def 3;

         A71:

        now

          let k be Nat such that

           A72: k in ( dom h);

          

           A73: k in ( Seg ( len h)) by A72, FINSEQ_1:def 3;

           A74:

          now

            

             A75: k in ( dom (F * f)) by A70, A72, CALCUL_2:def 2;

            given i be Nat such that

             A76: i in ( dom ( IdFinS (p,n))) and

             A77: k = (( len g) + i);

            ( len ( IdFinS (p,n))) = n by CARD_1:def 7;

            then

             A78: i <= n by A76, FINSEQ_3: 25;

            then

             A79: k <= (n + ( len g)) by A77, XREAL_1: 6;

            

             A80: 1 <= i by A76, FINSEQ_3: 25;

            then (1 + ( len g)) <= k by A77, XREAL_1: 6;

            then

             A81: k in ( seq (( len g),n)) by A79, CALCUL_2: 1;

            then (F . k) = (( Sgm A) . (k - ( len g))) by A18, A73;

            then (F . k) in ( rng ( Sgm A)) by A6, A81, FUNCT_1: 3;

            then (F . k) in A by A5, FINSEQ_1:def 13;

            then (f . (F . k)) in {p} by FUNCT_1:def 7;

            then (f . (F . k)) = p by TARSKI:def 1;

            then ((F * f) . k) = p by A75, FUNCT_1: 12;

            then

             A82: (( Per (f,F)) . k) = p by CALCUL_2:def 2;

            i in ( Seg n) by A80, A78, FINSEQ_1: 1;

            

            hence (( Per (f,F)) . k) = (( IdFinS (p,n)) . i) by A82, FUNCOP_1: 7

            .= (h . k) by A76, A77, FINSEQ_1:def 7;

          end;

          now

            assume

             A83: k in ( dom g);

            then

             A84: k in ( dom ( Sgm C)) by A20, A15, FINSEQ_1:def 3;

            k in ( Seg ( len g)) by A83, FINSEQ_1:def 3;

            then

             A85: (F . k) = (( Sgm C) . k) by A18, A73;

            k in ( dom (F * f)) by A70, A72, CALCUL_2:def 2;

            then ((F * f) . k) = (f . (( Sgm C) . k)) by A85, FUNCT_1: 12;

            

            hence (( Per (f,F)) . k) = (f . (( Sgm C) . k)) by CALCUL_2:def 2

            .= ((( Sgm C) * f) . k) by A84, FUNCT_1: 13

            .= (g . k) by FINSEQ_3:def 1

            .= (h . k) by A83, FINSEQ_1:def 7;

          end;

          hence (( Per (f,F)) . k) = (h . k) by A72, A74, FINSEQ_1: 25;

        end;

        then

         A86: ( Per (f,F)) = h by A70;

        reconsider h as FinSequence of ( CQC-WFF Al) by A70, A71, FINSEQ_1: 13;

        ((F * f) . j) = p by A14, A68, A69, FUNCT_1: 13;

        then

         A87: (h . j) = p by A86, CALCUL_2:def 2;

         A88:

        now

          assume

           A89: j in ( dom g);

          then (g . j) = p by A87, FINSEQ_1:def 7;

          then

           A90: (g . j) in {p} by TARSKI:def 1;

          

           A91: ( rng g) = (( rng f) \ {p}) by FINSEQ_3: 65;

          (g . j) in ( rng g) by A89, FUNCT_1: 3;

          hence contradiction by A90, A91, XBOOLE_0:def 5;

        end;

        j in ( dom f) by A68;

        then j in ( dom h) by A70, CALCUL_2: 19;

        then

        consider k be Nat such that

         A92: k in ( dom ( IdFinS (p,n))) and j = (( len g) + k) by A88, FINSEQ_1: 25;

        reconsider g as FinSequence of ( CQC-WFF Al) by FINSEQ_3: 86;

        1 <= k & k <= ( len ( IdFinS (p,n))) by A92, FINSEQ_3: 25;

        then 1 <= ( len ( IdFinS (p,n))) by XXREAL_0: 2;

        then

         A93: 1 <= n by CARD_1:def 7;

         |- (h ^ <*q*>) by A2, A86, CALCUL_2: 30;

        then

         A94: |- ((g ^ <*p*>) ^ <*q*>) by A93, CALCUL_2: 32;

        take g;

        ( rng g) = (( rng f) \ {p}) & (( rng f) \ {p}) c= ((X \/ {p}) \ {p}) by A1, FINSEQ_3: 65, XBOOLE_1: 33;

        then

         A95: ( rng g) c= (X \ {p}) by XBOOLE_1: 40;

        (X \ {p}) c= X by XBOOLE_1: 36;

        hence thesis by A94, A95, XBOOLE_1: 1;

      end;

      now

        assume

         A96: ( rng f) c= X;

        take f;

         |- ((f ^ <*p*>) ^ <*q*>) by A2, Th5;

        hence thesis by A96;

      end;

      hence thesis by A3;

    end;

    theorem :: HENMODEL:9

    X |- p iff (X \/ {( 'not' p)}) is Inconsistent

    proof

      thus X |- p implies (X \/ {( 'not' p)}) is Inconsistent

      proof

        assume X |- p;

        then

        consider f such that

         A1: ( rng f) c= X and

         A2: |- (f ^ <*p*>);

        set f2 = (f ^ <*( 'not' p)*>);

        set f1 = ((f ^ <*( 'not' p)*>) ^ <*( 'not' p)*>);

        

         A3: ( Ant f1) = (f ^ <*( 'not' p)*>) by CALCUL_1: 5;

        1 in ( Seg 1) by FINSEQ_1: 1;

        then 1 in ( dom <*( 'not' p)*>) by FINSEQ_1: 38;

        then

         A4: (( len f) + 1) in ( dom ( Ant f1)) by A3, FINSEQ_1: 28;

        ( Suc f1) = ( 'not' p) by CALCUL_1: 5;

        then (( Ant f1) . (( len f) + 1)) = ( Suc f1) by A3, FINSEQ_1: 42;

        then ( Suc f1) is_tail_of ( Ant f1) by A4, CALCUL_1:def 16;

        then

         A5: |- f1 by CALCUL_1: 33;

        

         A6: ( 0 + 1) <= ( len f2) by CALCUL_1: 10;

        ( Ant f2) = f & ( Suc f2) = ( 'not' p) by CALCUL_1: 5;

        then

         A7: ( rng f2) = (( rng f) \/ {( 'not' p)}) by A6, CALCUL_1: 3;

         |- ((f ^ <*( 'not' p)*>) ^ <*p*>) by A2, Th5;

        then not (f ^ <*( 'not' p)*>) is Consistent by A5;

        hence thesis by A1, A7, Th4, XBOOLE_1: 9;

      end;

      thus (X \/ {( 'not' p)}) is Inconsistent implies X |- p

      proof

        assume (X \/ {( 'not' p)}) is Inconsistent;

        then (X \/ {( 'not' p)}) |- p by Th6;

        then

        consider f such that

         A8: ( rng f) c= (X \/ {( 'not' p)}) and

         A9: |- (f ^ <*p*>);

        now

          set g = (f - {( 'not' p)});

          reconsider A = (f " {( 'not' p)}) as finite set;

          reconsider B = ( dom f) as finite set;

          set n = ( card A);

          set h = (g ^ ( IdFinS (( 'not' p),n)));

          

           A10: ( len ( IdFinS (( 'not' p),n))) = n by CARD_1:def 7;

          A c= B by RELAT_1: 132;

          then

           A11: A c= ( Seg ( len f)) by FINSEQ_1:def 3;

           A12:

          now

            let i;

            reconsider j = (i - ( len g)) as Integer;

            assume

             A13: i in ( seq (( len g),n));

            then

             A14: (1 + ( len g)) <= i by CALCUL_2: 1;

            then

             A15: 1 <= j by XREAL_1: 19;

            i <= (n + ( len g)) by A13, CALCUL_2: 1;

            then

             A16: j <= n by XREAL_1: 20;

             0 <= j by A14, XREAL_1: 19;

            then

            reconsider j as Element of NAT by INT_1: 3;

            j in ( Seg n) by A15, A16, FINSEQ_1: 1;

            hence (i - ( len g)) in ( dom ( Sgm A)) by A11, FINSEQ_3: 40;

          end;

          assume not ( rng f) c= X;

          then

          consider a be object such that

           A17: a in ( rng f) and

           A18: not a in X;

          a in X or a in {( 'not' p)} by A8, A17, XBOOLE_0:def 3;

          then a = ( 'not' p) by A18, TARSKI:def 1;

          then

          consider i be Nat such that

           A19: i in B and

           A20: (f . i) = ( 'not' p) by A17, FINSEQ_2: 10;

          reconsider C = (B \ A) as finite set;

          defpred P[ Nat, object] means ($1 in ( Seg ( len g)) implies $2 = (( Sgm (B \ A)) . $1)) & ($1 in ( seq (( len g),n)) implies $2 = (( Sgm A) . ($1 - ( len g))));

          

           A21: ( card C) = (( card B) - n) by CARD_2: 44, RELAT_1: 132

          .= (( card ( Seg ( len f))) - n) by FINSEQ_1:def 3

          .= (( len f) - n) by FINSEQ_1: 57

          .= ( len g) by FINSEQ_3: 59;

          

           A22: for k be Nat st k in ( Seg ( len h)) holds ex a be object st P[k, a]

          proof

            let k be Nat such that k in ( Seg ( len h));

            now

              assume

               A23: k in ( Seg ( len g));

              take a = (( Sgm (B \ A)) . k);

              ( Seg ( len g)) misses ( seq (( len g),n)) by CALCUL_2: 8;

              hence P[k, a] by A23, XBOOLE_0: 3;

            end;

            hence thesis;

          end;

          consider F be FinSequence such that

           A24: ( dom F) = ( Seg ( len h)) & for k be Nat st k in ( Seg ( len h)) holds P[k, (F . k)] from FINSEQ_1:sch 1( A22);

          now

            let b be object;

            assume b in C;

            then b in ( dom f);

            hence b in ( Seg ( len f)) by FINSEQ_1:def 3;

          end;

          then

           A25: C c= ( Seg ( len f));

          then

           A26: ( dom ( Sgm C)) = ( Seg ( card C)) by FINSEQ_3: 40;

          

           A27: ( rng F) = B

          proof

            now

              let a be object;

              assume a in ( rng F);

              then

              consider i be Nat such that

               A28: i in ( dom F) and

               A29: (F . i) = a by FINSEQ_2: 10;

               A30:

              now

                assume i in ( Seg ( len g));

                then a = (( Sgm C) . i) & i in ( dom ( Sgm C)) by A24, A25, A21, A28, A29, FINSEQ_3: 40;

                then a in ( rng ( Sgm C)) by FUNCT_1: 3;

                then a in C by A25, FINSEQ_1:def 13;

                hence a in B;

              end;

               A31:

              now

                

                 A32: ( rng ( Sgm A)) = A by A11, FINSEQ_1:def 13;

                

                 A33: A c= B by RELAT_1: 132;

                assume

                 A34: i in ( seq (( len g),n));

                then a = (( Sgm A) . (i - ( len g))) by A24, A28, A29;

                then a in A by A12, A34, A32, FUNCT_1: 3;

                hence a in B by A33;

              end;

              i in (( Seg ( len g)) \/ ( seq (( len g),n))) by A10, A24, A28, Lm1;

              hence a in B by A30, A31, XBOOLE_0:def 3;

            end;

            hence ( rng F) c= B;

            let a be object such that

             A35: a in B;

             A36:

            now

              now

                let b be object;

                assume b in C;

                then b in ( dom f);

                hence b in ( Seg ( len f)) by FINSEQ_1:def 3;

              end;

              then

               A37: C c= ( Seg ( len f));

              assume not a in A;

              then a in C by A35, XBOOLE_0:def 5;

              then a in ( rng ( Sgm C)) by A37, FINSEQ_1:def 13;

              then

              consider i be Nat such that

               A38: i in ( dom ( Sgm C)) and

               A39: (( Sgm C) . i) = a by FINSEQ_2: 10;

              

               A40: 1 <= i by A38, FINSEQ_3: 25;

              ( len ( Sgm C)) = ( len g) by A26, A21, FINSEQ_1:def 3;

              then

               A41: i <= ( len g) by A38, FINSEQ_3: 25;

              ( len g) <= ( len h) by CALCUL_1: 6;

              then i <= ( len h) by A41, XXREAL_0: 2;

              then

               A42: i in ( Seg ( len h)) by A40, FINSEQ_1: 1;

              i in ( Seg ( len g)) by A40, A41, FINSEQ_1: 1;

              then a = (F . i) by A24, A39, A42;

              hence thesis by A24, A42, FUNCT_1: 3;

            end;

            now

              assume

               A43: a in A;

              ( rng ( Sgm A)) = A by A11, FINSEQ_1:def 13;

              then

              consider i be Nat such that

               A44: i in ( dom ( Sgm A)) and

               A45: (( Sgm A) . i) = a by A43, FINSEQ_2: 10;

              reconsider i as Nat;

              set m = (i + ( len g));

              ( len ( Sgm A)) = n by A11, FINSEQ_3: 39;

              then i <= n by A44, FINSEQ_3: 25;

              then

               A46: m <= (n + ( len g)) by XREAL_1: 6;

              then m <= (( len g) + ( len ( IdFinS (( 'not' p),n)))) by CARD_1:def 7;

              then

               A47: m <= ( len h) by FINSEQ_1: 22;

              

               A48: 1 <= i by A44, FINSEQ_3: 25;

              then (1 + ( len g)) <= m by XREAL_1: 6;

              then

               A49: m in ( seq (( len g),n)) by A46, CALCUL_2: 1;

              i <= m by NAT_1: 11;

              then 1 <= m by A48, XXREAL_0: 2;

              then m in ( dom h) by A47, FINSEQ_3: 25;

              then

               A50: m in ( Seg ( len h)) by FINSEQ_1:def 3;

              a = (( Sgm A) . (m - ( len g))) by A45;

              then a = (F . m) by A24, A49, A50;

              hence thesis by A24, A50, FUNCT_1: 3;

            end;

            hence thesis by A36;

          end;

          

           A51: ( len h) = (( len g) + ( len ( IdFinS (( 'not' p),n)))) by FINSEQ_1: 22

          .= ((( len f) - n) + ( len ( IdFinS (( 'not' p),n)))) by FINSEQ_3: 59

          .= ((( len f) - n) + n) by CARD_1:def 7

          .= ( len f);

          then

           A52: ( dom F) = B by A24, FINSEQ_1:def 3;

          then

          reconsider F as Relation of B, B by A27, RELSET_1: 4;

          ( rng F) c= B;

          then

          reconsider F as Function of B, B by A52, FUNCT_2: 2;

          F is one-to-one

          proof

            let a1,a2 be object such that

             A53: a1 in ( dom F) and

             A54: a2 in ( dom F) and

             A55: (F . a1) = (F . a2);

            

             A56: a2 in (( Seg ( len g)) \/ ( seq (( len g),n))) by A10, A24, A54, Lm1;

             A57:

            now

              assume

               A58: a1 in ( Seg ( len g));

              then

               A59: a1 in ( dom ( Sgm C)) by A25, A21, FINSEQ_3: 40;

              (F . a1) = (( Sgm C) . a1) by A24, A53, A58;

              then (F . a1) in ( rng ( Sgm C)) by A59, FUNCT_1: 3;

              then

               A60: (F . a1) in C by A25, FINSEQ_1:def 13;

               A61:

              now

                assume

                 A62: a2 in ( seq (( len g),n));

                then

                reconsider i = a2 as Nat;

                (( Sgm A) . (i - ( len g))) in ( rng ( Sgm A)) by A12, A62, FUNCT_1: 3;

                then (F . a2) in ( rng ( Sgm A)) by A24, A54, A62;

                then (F . a2) in A by A11, FINSEQ_1:def 13;

                hence contradiction by A55, A60, XBOOLE_0:def 5;

              end;

              now

                assume

                 A63: a2 in ( Seg ( len g));

                then (F . a2) = (( Sgm C) . a2) by A24, A54;

                then

                 A64: (( Sgm C) . a1) = (( Sgm C) . a2) by A24, A53, A55, A58;

                

                 A65: ( Sgm C) is one-to-one by A25, FINSEQ_3: 92;

                a2 in ( dom ( Sgm C)) by A25, A21, A63, FINSEQ_3: 40;

                hence thesis by A59, A64, A65;

              end;

              hence thesis by A56, A61, XBOOLE_0:def 3;

            end;

             A66:

            now

              assume

               A67: a1 in ( seq (( len g),n));

              then

              reconsider i = a1 as Nat;

              

               A68: (i - ( len g)) in ( dom ( Sgm A)) by A12, A67;

               A69:

              now

                assume

                 A70: a2 in ( seq (( len g),n));

                then

                reconsider i1 = a2 as Nat;

                (F . a2) = (( Sgm A) . (i1 - ( len g))) by A24, A54, A70;

                then

                 A71: (( Sgm A) . (i1 - ( len g))) = (( Sgm A) . (i - ( len g))) by A24, A53, A55, A67;

                

                 A72: ( Sgm A) is one-to-one by A11, FINSEQ_3: 92;

                (i1 - ( len g)) in ( dom ( Sgm A)) by A12, A70;

                then (i1 - ( len g)) = (i - ( len g)) by A68, A71, A72;

                hence thesis;

              end;

              (( Sgm A) . (i - ( len g))) in ( rng ( Sgm A)) by A12, A67, FUNCT_1: 3;

              then (F . a1) in ( rng ( Sgm A)) by A24, A53, A67;

              then

               A73: (F . a1) in A by A11, FINSEQ_1:def 13;

              now

                assume a2 in ( Seg ( len g));

                then (F . a2) = (( Sgm C) . a2) & a2 in ( dom ( Sgm C)) by A24, A25, A21, A54, FINSEQ_3: 40;

                then (F . a2) in ( rng ( Sgm C)) by FUNCT_1: 3;

                then (F . a2) in C by A25, FINSEQ_1:def 13;

                hence contradiction by A55, A73, XBOOLE_0:def 5;

              end;

              hence thesis by A56, A69, XBOOLE_0:def 3;

            end;

            a1 in (( Seg ( len g)) \/ ( seq (( len g),n))) by A10, A24, A53, Lm1;

            hence thesis by A57, A66, XBOOLE_0:def 3;

          end;

          then

          reconsider F as Permutation of ( dom f) by A27, FUNCT_2: 57;

          consider j be Nat such that

           A74: j in ( dom F) and

           A75: (F . j) = i by A27, A19, FINSEQ_2: 10;

          

           A76: ( dom ( Per (f,F))) = B by CALCUL_2: 19

          .= ( dom F) by A24, A51, FINSEQ_1:def 3

          .= ( dom h) by A24, FINSEQ_1:def 3;

           A77:

          now

            let k be Nat such that

             A78: k in ( dom h);

            

             A79: k in ( Seg ( len h)) by A78, FINSEQ_1:def 3;

             A80:

            now

              

               A81: k in ( dom (F * f)) by A76, A78, CALCUL_2:def 2;

              given i be Nat such that

               A82: i in ( dom ( IdFinS (( 'not' p),n))) and

               A83: k = (( len g) + i);

              ( len ( IdFinS (( 'not' p),n))) = n by CARD_1:def 7;

              then

               A84: i <= n by A82, FINSEQ_3: 25;

              then

               A85: k <= (n + ( len g)) by A83, XREAL_1: 6;

              

               A86: 1 <= i by A82, FINSEQ_3: 25;

              then (1 + ( len g)) <= k by A83, XREAL_1: 6;

              then

               A87: k in ( seq (( len g),n)) by A85, CALCUL_2: 1;

              then (F . k) = (( Sgm A) . (k - ( len g))) by A24, A79;

              then (F . k) in ( rng ( Sgm A)) by A12, A87, FUNCT_1: 3;

              then (F . k) in A by A11, FINSEQ_1:def 13;

              then (f . (F . k)) in {( 'not' p)} by FUNCT_1:def 7;

              then (f . (F . k)) = ( 'not' p) by TARSKI:def 1;

              then ((F * f) . k) = ( 'not' p) by A81, FUNCT_1: 12;

              then

               A88: (( Per (f,F)) . k) = ( 'not' p) by CALCUL_2:def 2;

              i in ( Seg n) by A86, A84, FINSEQ_1: 1;

              

              hence (( Per (f,F)) . k) = (( IdFinS (( 'not' p),n)) . i) by A88, FUNCOP_1: 7

              .= (h . k) by A82, A83, FINSEQ_1:def 7;

            end;

            now

              assume

               A89: k in ( dom g);

              then

               A90: k in ( dom ( Sgm C)) by A26, A21, FINSEQ_1:def 3;

              k in ( Seg ( len g)) by A89, FINSEQ_1:def 3;

              then

               A91: (F . k) = (( Sgm C) . k) by A24, A79;

              k in ( dom (F * f)) by A76, A78, CALCUL_2:def 2;

              then ((F * f) . k) = (f . (( Sgm C) . k)) by A91, FUNCT_1: 12;

              

              hence (( Per (f,F)) . k) = (f . (( Sgm C) . k)) by CALCUL_2:def 2

              .= ((( Sgm C) * f) . k) by A90, FUNCT_1: 13

              .= (g . k) by FINSEQ_3:def 1

              .= (h . k) by A89, FINSEQ_1:def 7;

            end;

            hence (( Per (f,F)) . k) = (h . k) by A78, A80, FINSEQ_1: 25;

          end;

          then

           A92: ( Per (f,F)) = h by A76;

          reconsider h as FinSequence of ( CQC-WFF Al) by A76, A77, FINSEQ_1: 13;

          ((F * f) . j) = ( 'not' p) by A20, A74, A75, FUNCT_1: 13;

          then

           A93: (h . j) = ( 'not' p) by A92, CALCUL_2:def 2;

           A94:

          now

            assume

             A95: j in ( dom g);

            then (g . j) = ( 'not' p) by A93, FINSEQ_1:def 7;

            then

             A96: (g . j) in {( 'not' p)} by TARSKI:def 1;

            

             A97: ( rng g) = (( rng f) \ {( 'not' p)}) by FINSEQ_3: 65;

            (g . j) in ( rng g) by A95, FUNCT_1: 3;

            hence contradiction by A96, A97, XBOOLE_0:def 5;

          end;

          j in ( dom f) by A74;

          then j in ( dom h) by A76, CALCUL_2: 19;

          then

          consider k be Nat such that

           A98: k in ( dom ( IdFinS (( 'not' p),n))) and j = (( len g) + k) by A94, FINSEQ_1: 25;

          reconsider g as FinSequence of ( CQC-WFF Al) by FINSEQ_3: 86;

          1 <= k & k <= ( len ( IdFinS (( 'not' p),n))) by A98, FINSEQ_3: 25;

          then 1 <= ( len ( IdFinS (( 'not' p),n))) by XXREAL_0: 2;

          then

           A99: 1 <= n by CARD_1:def 7;

           |- (h ^ <*p*>) by A9, A92, CALCUL_2: 30;

          then

           A100: |- ((g ^ <*( 'not' p)*>) ^ <*p*>) by A99, CALCUL_2: 32;

          ( rng g) = (( rng f) \ {( 'not' p)}) & (( rng f) \ {( 'not' p)}) c= ((X \/ {( 'not' p)}) \ {( 'not' p)}) by A8, FINSEQ_3: 65, XBOOLE_1: 33;

          then

           A101: ( rng g) c= (X \ {( 'not' p)}) by XBOOLE_1: 40;

          (X \ {( 'not' p)}) c= X by XBOOLE_1: 36;

          then

           A102: ( rng g) c= X by A101;

           |- ((g ^ <*p*>) ^ <*p*>) by CALCUL_2: 21;

          then |- (g ^ <*p*>) by A100, CALCUL_2: 26;

          hence thesis by A102;

        end;

        hence thesis by A9;

      end;

    end;

    theorem :: HENMODEL:10

    X |- ( 'not' p) iff (X \/ {p}) is Inconsistent

    proof

      thus X |- ( 'not' p) implies (X \/ {p}) is Inconsistent

      proof

        assume X |- ( 'not' p);

        then

        consider f such that

         A1: ( rng f) c= X and

         A2: |- (f ^ <*( 'not' p)*>);

        set f2 = (f ^ <*p*>);

        set f1 = ((f ^ <*p*>) ^ <*p*>);

        

         A3: ( Ant f1) = (f ^ <*p*>) by CALCUL_1: 5;

        1 in ( Seg 1) by FINSEQ_1: 1;

        then 1 in ( dom <*p*>) by FINSEQ_1: 38;

        then

         A4: (( len f) + 1) in ( dom ( Ant f1)) by A3, FINSEQ_1: 28;

        ( Suc f1) = p by CALCUL_1: 5;

        then (( Ant f1) . (( len f) + 1)) = ( Suc f1) by A3, FINSEQ_1: 42;

        then ( Suc f1) is_tail_of ( Ant f1) by A4, CALCUL_1:def 16;

        then

         A5: |- f1 by CALCUL_1: 33;

        

         A6: ( 0 + 1) <= ( len f2) by CALCUL_1: 10;

        ( Ant f2) = f & ( Suc f2) = p by CALCUL_1: 5;

        then

         A7: ( rng f2) = (( rng f) \/ {p}) by A6, CALCUL_1: 3;

         |- ((f ^ <*p*>) ^ <*( 'not' p)*>) by A2, Th5;

        then not (f ^ <*p*>) is Consistent by A5;

        hence thesis by A1, A7, Th4, XBOOLE_1: 9;

      end;

      thus (X \/ {p}) is Inconsistent implies X |- ( 'not' p)

      proof

        assume (X \/ {p}) is Inconsistent;

        then (X \/ {p}) |- ( 'not' p) by Th6;

        then

        consider f such that

         A8: ( rng f) c= (X \/ {p}) and

         A9: |- (f ^ <*( 'not' p)*>);

        now

          set g = (f - {p});

          reconsider A = (f " {p}) as finite set;

          reconsider B = ( dom f) as finite set;

          set n = ( card A);

          set h = (g ^ ( IdFinS (p,n)));

          

           A10: ( len ( IdFinS (p,n))) = n by CARD_1:def 7;

          A c= B by RELAT_1: 132;

          then

           A11: A c= ( Seg ( len f)) by FINSEQ_1:def 3;

           A12:

          now

            let i;

            reconsider j = (i - ( len g)) as Integer;

            assume

             A13: i in ( seq (( len g),n));

            then

             A14: (1 + ( len g)) <= i by CALCUL_2: 1;

            then

             A15: 1 <= j by XREAL_1: 19;

            i <= (n + ( len g)) by A13, CALCUL_2: 1;

            then

             A16: j <= n by XREAL_1: 20;

             0 <= j by A14, XREAL_1: 19;

            then

            reconsider j as Element of NAT by INT_1: 3;

            j in ( Seg n) by A15, A16, FINSEQ_1: 1;

            hence (i - ( len g)) in ( dom ( Sgm A)) by A11, FINSEQ_3: 40;

          end;

          assume not ( rng f) c= X;

          then

          consider a be object such that

           A17: a in ( rng f) and

           A18: not a in X;

          a in X or a in {p} by A8, A17, XBOOLE_0:def 3;

          then a = p by A18, TARSKI:def 1;

          then

          consider i be Nat such that

           A19: i in B and

           A20: (f . i) = p by A17, FINSEQ_2: 10;

          reconsider C = (B \ A) as finite set;

          defpred P[ Nat, object] means ($1 in ( Seg ( len g)) implies $2 = (( Sgm (B \ A)) . $1)) & ($1 in ( seq (( len g),n)) implies $2 = (( Sgm A) . ($1 - ( len g))));

          

           A21: ( card C) = (( card B) - n) by CARD_2: 44, RELAT_1: 132

          .= (( card ( Seg ( len f))) - n) by FINSEQ_1:def 3

          .= (( len f) - n) by FINSEQ_1: 57

          .= ( len g) by FINSEQ_3: 59;

          

           A22: for k be Nat st k in ( Seg ( len h)) holds ex a be object st P[k, a]

          proof

            let k be Nat such that k in ( Seg ( len h));

            now

              assume

               A23: k in ( Seg ( len g));

              take a = (( Sgm (B \ A)) . k);

              ( Seg ( len g)) misses ( seq (( len g),n)) by CALCUL_2: 8;

              hence P[k, a] by A23, XBOOLE_0: 3;

            end;

            hence thesis;

          end;

          consider F be FinSequence such that

           A24: ( dom F) = ( Seg ( len h)) & for k be Nat st k in ( Seg ( len h)) holds P[k, (F . k)] from FINSEQ_1:sch 1( A22);

          now

            let b be object;

            assume b in C;

            then b in ( dom f);

            hence b in ( Seg ( len f)) by FINSEQ_1:def 3;

          end;

          then

           A25: C c= ( Seg ( len f));

          then

           A26: ( dom ( Sgm C)) = ( Seg ( card C)) by FINSEQ_3: 40;

          

           A27: ( rng F) = B

          proof

            now

              let a be object;

              assume a in ( rng F);

              then

              consider i be Nat such that

               A28: i in ( dom F) and

               A29: (F . i) = a by FINSEQ_2: 10;

               A30:

              now

                assume i in ( Seg ( len g));

                then a = (( Sgm C) . i) & i in ( dom ( Sgm C)) by A24, A25, A21, A28, A29, FINSEQ_3: 40;

                then a in ( rng ( Sgm C)) by FUNCT_1: 3;

                then a in C by A25, FINSEQ_1:def 13;

                hence a in B;

              end;

               A31:

              now

                

                 A32: ( rng ( Sgm A)) = A by A11, FINSEQ_1:def 13;

                

                 A33: A c= B by RELAT_1: 132;

                assume

                 A34: i in ( seq (( len g),n));

                then a = (( Sgm A) . (i - ( len g))) by A24, A28, A29;

                then a in A by A12, A34, A32, FUNCT_1: 3;

                hence a in B by A33;

              end;

              i in (( Seg ( len g)) \/ ( seq (( len g),n))) by A10, A24, A28, Lm1;

              hence a in B by A30, A31, XBOOLE_0:def 3;

            end;

            hence ( rng F) c= B;

            let a be object such that

             A35: a in B;

             A36:

            now

              now

                let b be object;

                assume b in C;

                then b in ( dom f);

                hence b in ( Seg ( len f)) by FINSEQ_1:def 3;

              end;

              then

               A37: C c= ( Seg ( len f));

              assume not a in A;

              then a in C by A35, XBOOLE_0:def 5;

              then a in ( rng ( Sgm C)) by A37, FINSEQ_1:def 13;

              then

              consider i be Nat such that

               A38: i in ( dom ( Sgm C)) and

               A39: (( Sgm C) . i) = a by FINSEQ_2: 10;

              

               A40: 1 <= i by A38, FINSEQ_3: 25;

              ( len ( Sgm C)) = ( len g) by A26, A21, FINSEQ_1:def 3;

              then

               A41: i <= ( len g) by A38, FINSEQ_3: 25;

              ( len g) <= ( len h) by CALCUL_1: 6;

              then i <= ( len h) by A41, XXREAL_0: 2;

              then

               A42: i in ( Seg ( len h)) by A40, FINSEQ_1: 1;

              i in ( Seg ( len g)) by A40, A41, FINSEQ_1: 1;

              then a = (F . i) by A24, A39, A42;

              hence thesis by A24, A42, FUNCT_1: 3;

            end;

            now

              assume

               A43: a in A;

              ( rng ( Sgm A)) = A by A11, FINSEQ_1:def 13;

              then

              consider i be Nat such that

               A44: i in ( dom ( Sgm A)) and

               A45: (( Sgm A) . i) = a by A43, FINSEQ_2: 10;

              reconsider i as Nat;

              set m = (i + ( len g));

              ( len ( Sgm A)) = n by A11, FINSEQ_3: 39;

              then i <= n by A44, FINSEQ_3: 25;

              then

               A46: m <= (n + ( len g)) by XREAL_1: 6;

              then m <= (( len g) + ( len ( IdFinS (p,n)))) by CARD_1:def 7;

              then

               A47: m <= ( len h) by FINSEQ_1: 22;

              

               A48: 1 <= i by A44, FINSEQ_3: 25;

              then (1 + ( len g)) <= m by XREAL_1: 6;

              then

               A49: m in ( seq (( len g),n)) by A46, CALCUL_2: 1;

              i <= m by NAT_1: 11;

              then 1 <= m by A48, XXREAL_0: 2;

              then m in ( dom h) by A47, FINSEQ_3: 25;

              then

               A50: m in ( Seg ( len h)) by FINSEQ_1:def 3;

              a = (( Sgm A) . (m - ( len g))) by A45;

              then a = (F . m) by A24, A49, A50;

              hence thesis by A24, A50, FUNCT_1: 3;

            end;

            hence thesis by A36;

          end;

          

           A51: ( len h) = (( len g) + ( len ( IdFinS (p,n)))) by FINSEQ_1: 22

          .= ((( len f) - n) + ( len ( IdFinS (p,n)))) by FINSEQ_3: 59

          .= ((( len f) - n) + n) by CARD_1:def 7

          .= ( len f);

          then

           A52: ( dom F) = B by A24, FINSEQ_1:def 3;

          then

          reconsider F as Relation of B, B by A27, RELSET_1: 4;

          ( rng F) c= B;

          then

          reconsider F as Function of B, B by A52, FUNCT_2: 2;

          F is one-to-one

          proof

            let a1,a2 be object such that

             A53: a1 in ( dom F) and

             A54: a2 in ( dom F) and

             A55: (F . a1) = (F . a2);

            

             A56: a2 in (( Seg ( len g)) \/ ( seq (( len g),n))) by A10, A24, A54, Lm1;

             A57:

            now

              assume

               A58: a1 in ( Seg ( len g));

              then

               A59: a1 in ( dom ( Sgm C)) by A25, A21, FINSEQ_3: 40;

              (F . a1) = (( Sgm C) . a1) by A24, A53, A58;

              then (F . a1) in ( rng ( Sgm C)) by A59, FUNCT_1: 3;

              then

               A60: (F . a1) in C by A25, FINSEQ_1:def 13;

               A61:

              now

                assume

                 A62: a2 in ( seq (( len g),n));

                then

                reconsider i = a2 as Nat;

                (( Sgm A) . (i - ( len g))) in ( rng ( Sgm A)) by A12, A62, FUNCT_1: 3;

                then (F . a2) in ( rng ( Sgm A)) by A24, A54, A62;

                then (F . a2) in A by A11, FINSEQ_1:def 13;

                hence contradiction by A55, A60, XBOOLE_0:def 5;

              end;

              now

                assume

                 A63: a2 in ( Seg ( len g));

                then (F . a2) = (( Sgm C) . a2) by A24, A54;

                then

                 A64: (( Sgm C) . a1) = (( Sgm C) . a2) by A24, A53, A55, A58;

                

                 A65: ( Sgm C) is one-to-one by A25, FINSEQ_3: 92;

                a2 in ( dom ( Sgm C)) by A25, A21, A63, FINSEQ_3: 40;

                hence thesis by A59, A64, A65;

              end;

              hence thesis by A56, A61, XBOOLE_0:def 3;

            end;

             A66:

            now

              assume

               A67: a1 in ( seq (( len g),n));

              then

              reconsider i = a1 as Nat;

              

               A68: (i - ( len g)) in ( dom ( Sgm A)) by A12, A67;

               A69:

              now

                assume

                 A70: a2 in ( seq (( len g),n));

                then

                reconsider i1 = a2 as Nat;

                (F . a2) = (( Sgm A) . (i1 - ( len g))) by A24, A54, A70;

                then

                 A71: (( Sgm A) . (i1 - ( len g))) = (( Sgm A) . (i - ( len g))) by A24, A53, A55, A67;

                

                 A72: ( Sgm A) is one-to-one by A11, FINSEQ_3: 92;

                (i1 - ( len g)) in ( dom ( Sgm A)) by A12, A70;

                then ((i1 - ( len g)) + ( len g)) = ((i - ( len g)) + ( len g)) by A68, A71, A72;

                hence thesis;

              end;

              (( Sgm A) . (i - ( len g))) in ( rng ( Sgm A)) by A12, A67, FUNCT_1: 3;

              then (F . a1) in ( rng ( Sgm A)) by A24, A53, A67;

              then

               A73: (F . a1) in A by A11, FINSEQ_1:def 13;

              now

                assume a2 in ( Seg ( len g));

                then (F . a2) = (( Sgm C) . a2) & a2 in ( dom ( Sgm C)) by A24, A25, A21, A54, FINSEQ_3: 40;

                then (F . a2) in ( rng ( Sgm C)) by FUNCT_1: 3;

                then (F . a2) in C by A25, FINSEQ_1:def 13;

                hence contradiction by A55, A73, XBOOLE_0:def 5;

              end;

              hence thesis by A56, A69, XBOOLE_0:def 3;

            end;

            a1 in (( Seg ( len g)) \/ ( seq (( len g),n))) by A10, A24, A53, Lm1;

            hence thesis by A57, A66, XBOOLE_0:def 3;

          end;

          then

          reconsider F as Permutation of ( dom f) by A27, FUNCT_2: 57;

          consider j be Nat such that

           A74: j in ( dom F) and

           A75: (F . j) = i by A27, A19, FINSEQ_2: 10;

          

           A76: ( dom ( Per (f,F))) = B by CALCUL_2: 19

          .= ( dom F) by A24, A51, FINSEQ_1:def 3

          .= ( dom h) by A24, FINSEQ_1:def 3;

           A77:

          now

            let k be Nat such that

             A78: k in ( dom h);

            

             A79: k in ( Seg ( len h)) by A78, FINSEQ_1:def 3;

             A80:

            now

              

               A81: k in ( dom (F * f)) by A76, A78, CALCUL_2:def 2;

              given i be Nat such that

               A82: i in ( dom ( IdFinS (p,n))) and

               A83: k = (( len g) + i);

              ( len ( IdFinS (p,n))) = n by CARD_1:def 7;

              then

               A84: i <= n by A82, FINSEQ_3: 25;

              then

               A85: k <= (n + ( len g)) by A83, XREAL_1: 6;

              

               A86: 1 <= i by A82, FINSEQ_3: 25;

              then (1 + ( len g)) <= k by A83, XREAL_1: 6;

              then

               A87: k in ( seq (( len g),n)) by A85, CALCUL_2: 1;

              then (F . k) = (( Sgm A) . (k - ( len g))) by A24, A79;

              then (F . k) in ( rng ( Sgm A)) by A12, A87, FUNCT_1: 3;

              then (F . k) in A by A11, FINSEQ_1:def 13;

              then (f . (F . k)) in {p} by FUNCT_1:def 7;

              then (f . (F . k)) = p by TARSKI:def 1;

              then ((F * f) . k) = p by A81, FUNCT_1: 12;

              then

               A88: (( Per (f,F)) . k) = p by CALCUL_2:def 2;

              i in ( Seg n) by A86, A84, FINSEQ_1: 1;

              

              hence (( Per (f,F)) . k) = (( IdFinS (p,n)) . i) by A88, FUNCOP_1: 7

              .= (h . k) by A82, A83, FINSEQ_1:def 7;

            end;

            now

              assume

               A89: k in ( dom g);

              then

               A90: k in ( dom ( Sgm C)) by A26, A21, FINSEQ_1:def 3;

              k in ( Seg ( len g)) by A89, FINSEQ_1:def 3;

              then

               A91: (F . k) = (( Sgm C) . k) by A24, A79;

              k in ( dom (F * f)) by A76, A78, CALCUL_2:def 2;

              then ((F * f) . k) = (f . (( Sgm C) . k)) by A91, FUNCT_1: 12;

              

              hence (( Per (f,F)) . k) = (f . (( Sgm C) . k)) by CALCUL_2:def 2

              .= ((( Sgm C) * f) . k) by A90, FUNCT_1: 13

              .= (g . k) by FINSEQ_3:def 1

              .= (h . k) by A89, FINSEQ_1:def 7;

            end;

            hence (( Per (f,F)) . k) = (h . k) by A78, A80, FINSEQ_1: 25;

          end;

          then

           A92: ( Per (f,F)) = h by A76;

          reconsider h as FinSequence of ( CQC-WFF Al) by A76, A77, FINSEQ_1: 13;

          ((F * f) . j) = p by A20, A74, A75, FUNCT_1: 13;

          then

           A93: (h . j) = p by A92, CALCUL_2:def 2;

           A94:

          now

            assume

             A95: j in ( dom g);

            then (g . j) = p by A93, FINSEQ_1:def 7;

            then

             A96: (g . j) in {p} by TARSKI:def 1;

            

             A97: ( rng g) = (( rng f) \ {p}) by FINSEQ_3: 65;

            (g . j) in ( rng g) by A95, FUNCT_1: 3;

            hence contradiction by A96, A97, XBOOLE_0:def 5;

          end;

          j in ( dom f) by A74;

          then j in ( dom h) by A76, CALCUL_2: 19;

          then

          consider k be Nat such that

           A98: k in ( dom ( IdFinS (p,n))) and j = (( len g) + k) by A94, FINSEQ_1: 25;

          reconsider g as FinSequence of ( CQC-WFF Al) by FINSEQ_3: 86;

          1 <= k & k <= ( len ( IdFinS (p,n))) by A98, FINSEQ_3: 25;

          then 1 <= ( len ( IdFinS (p,n))) by XXREAL_0: 2;

          then

           A99: 1 <= n by CARD_1:def 7;

           |- (h ^ <*( 'not' p)*>) by A9, A92, CALCUL_2: 30;

          then

           A100: |- ((g ^ <*p*>) ^ <*( 'not' p)*>) by A99, CALCUL_2: 32;

          ( rng g) = (( rng f) \ {p}) & (( rng f) \ {p}) c= ((X \/ {p}) \ {p}) by A8, FINSEQ_3: 65, XBOOLE_1: 33;

          then

           A101: ( rng g) c= (X \ {p}) by XBOOLE_1: 40;

          (X \ {p}) c= X by XBOOLE_1: 36;

          then

           A102: ( rng g) c= X by A101;

           |- ((g ^ <*( 'not' p)*>) ^ <*( 'not' p)*>) by CALCUL_2: 21;

          then |- (g ^ <*( 'not' p)*>) by A100, CALCUL_2: 26;

          hence thesis by A102;

        end;

        hence thesis by A9;

      end;

    end;

    begin

    theorem :: HENMODEL:11

    for f be sequence of ( bool ( CQC-WFF Al)) st (for n, m st m in ( dom f) & n in ( dom f) & n < m holds (f . n) is Consistent & (f . n) c= (f . m)) holds ( union ( rng f)) is Consistent

    proof

      let f be sequence of ( bool ( CQC-WFF Al));

      assume

       A1: for n, m st m in ( dom f) & n in ( dom f) & n < m holds (f . n) is Consistent & (f . n) c= (f . m);

      now

        

         A2: for n st n in ( dom f) holds (f . n) is Consistent

        proof

          let n such that

           A3: n in ( dom f);

          (n + 1) in NAT ;

          then n < (n + 1) & (n + 1) in ( dom f) by FUNCT_2:def 1, NAT_1: 13;

          hence thesis by A1, A3;

        end;

        assume not ( union ( rng f)) is Consistent;

        then

        consider Z such that

         A4: Z c= ( union ( rng f)) & Z is finite and

         A5: Z is Inconsistent by Th7;

        for n, m st m in ( dom f) & n in ( dom f) & n < m holds (f . n) c= (f . m) by A1;

        then

        consider k such that

         A6: Z c= (f . k) by A4, Th3;

        reconsider Y = (f . k) as Subset of ( CQC-WFF Al);

        consider p such that

         A7: Z |- p and

         A8: Z |- ( 'not' p) by A5;

        consider f1 such that

         A9: ( rng f1) c= Z and

         A10: |- (f1 ^ <*p*>) by A7;

        consider f2 such that

         A11: ( rng f2) c= Z and

         A12: |- (f2 ^ <*( 'not' p)*>) by A8;

        ( rng (f1 ^ f2)) = (( rng f1) \/ ( rng f2)) by FINSEQ_1: 31;

        then ( rng (f1 ^ f2)) c= Z by A9, A11, XBOOLE_1: 8;

        then

         A13: ( rng (f1 ^ f2)) c= Y by A6;

         |- ((f1 ^ f2) ^ <*( 'not' p)*>) by A12, CALCUL_2: 20;

        then

         A14: Y |- ( 'not' p) by A13;

         |- ((f1 ^ f2) ^ <*p*>) by A10, Th5;

        then Y |- p by A13;

        then

         A15: not Y is Consistent by A14;

        k in NAT by ORDINAL1:def 12;

        then k in ( dom f) by FUNCT_2:def 1;

        hence contradiction by A15, A2;

      end;

      hence thesis;

    end;

    begin

    reserve A for non empty set,

v for Element of ( Valuations_in (Al,A)),

J for interpretation of Al, A;

    theorem :: HENMODEL:12

    

     Th12: X is Inconsistent implies for J, v holds not (J,v) |= X

    proof

      reconsider p = ( 'not' ( VERUM Al)) as Element of ( CQC-WFF Al);

      assume not X is Consistent;

      then X |- ( 'not' ( VERUM Al)) by Th6;

      then

      consider f such that

       A1: ( rng f) c= X and

       A2: |- (f ^ <*( 'not' ( VERUM Al))*>);

      let J, v;

      

       A3: ( Suc (f ^ <*p*>)) = p by CALCUL_1: 5;

      ( rng ( Ant (f ^ <*p*>))) c= X by A1, CALCUL_1: 5;

      then p is_formal_provable_from X by A2, A3, CALCUL_1:def 10;

      then

       A4: X |= p by CALCUL_1: 32;

      now

        assume (J,v) |= X;

        then (J,v) |= ( 'not' ( VERUM Al)) by A4, CALCUL_1:def 12;

        then not (J,v) |= ( VERUM Al) by VALUAT_1: 17;

        hence contradiction by VALUAT_1: 32;

      end;

      hence thesis;

    end;

    theorem :: HENMODEL:13

    

     Th13: {( VERUM Al)} is Consistent

    proof

      set A = the non empty set, J = the interpretation of Al, A, v = the Element of ( Valuations_in (Al,A));

      (J,v) |= ( VERUM Al) by VALUAT_1: 32;

      then for p st p in {( VERUM Al)} holds (J,v) |= p by TARSKI:def 1;

      then (J,v) |= {( VERUM Al)} by CALCUL_1:def 11;

      hence thesis by Th12;

    end;

    registration

      let Al;

      cluster Consistent for Subset of ( CQC-WFF Al);

      existence

      proof

         {( VERUM Al)} is Consistent by Th13;

        hence thesis;

      end;

    end

    reserve CX for Consistent Subset of ( CQC-WFF Al),

P9 for Element of ( QC-pred_symbols Al);

    definition

      let Al;

      :: HENMODEL:def4

      func HCar (Al) -> non empty set equals ( bound_QC-variables Al);

      coherence ;

    end

    definition

      let Al;

      let P be Element of ( QC-pred_symbols Al), ll be CQC-variable_list of ( the_arity_of P), Al;

      :: original: !

      redefine

      func P ! ll -> Element of ( CQC-WFF Al) ;

      coherence

      proof

        set k = ( the_arity_of P);

        reconsider P9 = P as QC-pred_symbol of k, Al by QC_LANG3: 1;

        (P9 ! ll) is Element of ( CQC-WFF Al);

        hence thesis;

      end;

    end

    definition

      let Al;

      let CX;

      :: HENMODEL:def5

      mode Henkin_interpretation of CX -> interpretation of Al, ( HCar Al) means

      : Def5: for P be Element of ( QC-pred_symbols Al), r be Element of ( relations_on ( HCar Al)) st (it . P) = r holds for a holds a in r iff ex ll be CQC-variable_list of ( the_arity_of P), Al st a = ll & CX |- (P ! ll);

      existence

      proof

        defpred P[ object, object] means ex P9 st P9 = $1 & $2 = { ll where ll be CQC-variable_list of ( the_arity_of P9), Al : CX |- (P9 ! ll) };

        set A = ( QC-pred_symbols Al);

        

         A1: for a be object st a in A holds ex b be object st P[a, b]

        proof

          let a be object;

          assume a in A;

          then

          reconsider a as Element of ( QC-pred_symbols Al);

          consider b such that

           A2: b = { ll where ll be CQC-variable_list of ( the_arity_of a), Al : CX |- (a ! ll) };

          take b;

          take a;

          thus thesis by A2;

        end;

        consider f be Function such that

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

        

         A4: for P be Element of ( QC-pred_symbols Al), r be Element of ( relations_on ( HCar Al)) st (f . P) = r holds for a holds a in r iff ex ll be CQC-variable_list of ( the_arity_of P), Al st a = ll & CX |- (P ! ll)

        proof

          let P be Element of ( QC-pred_symbols Al), r be Element of ( relations_on ( HCar Al)) such that

           A5: (f . P) = r;

          let a;

          thus a in r implies ex ll be CQC-variable_list of ( the_arity_of P), Al st a = ll & CX |- (P ! ll)

          proof

            assume

             A6: a in r;

            ex P9 st P9 = P & (f . P) = { ll where ll be CQC-variable_list of ( the_arity_of P9), Al : CX |- (P9 ! ll) } by A3;

            hence thesis by A5, A6;

          end;

          thus (ex ll be CQC-variable_list of ( the_arity_of P), Al st a = ll & CX |- (P ! ll)) implies a in r

          proof

            given ll be CQC-variable_list of ( the_arity_of P), Al such that

             A7: a = ll & CX |- (P ! ll);

            ex P9 st P9 = P & (f . P) = { l where l be CQC-variable_list of ( the_arity_of P9), Al : CX |- (P9 ! l) } by A3;

            hence thesis by A5, A7;

          end;

        end;

        

         A8: for P be Element of ( QC-pred_symbols Al), r be Element of ( relations_on ( HCar Al)) st (f . P) = r holds r = ( empty_rel ( HCar Al)) or ( the_arity_of P) = ( the_arity_of r)

        proof

          let P be Element of ( QC-pred_symbols Al), r be Element of ( relations_on ( HCar Al)) such that

           A9: (f . P) = r;

          consider P9 such that

           A10: P9 = P & (f . P) = { ll where ll be CQC-variable_list of ( the_arity_of P9), Al : CX |- (P9 ! ll) } by A3;

          assume

           A11: not r = ( empty_rel ( HCar Al));

          then r <> {} by MARGREL1: 9;

          then

          consider a be object such that

           A12: a in r by XBOOLE_0:def 1;

          consider ll9 be CQC-variable_list of ( the_arity_of P9), Al such that

           A13: a = ll9 and CX |- (P9 ! ll9) by A9, A12, A10;

          ( rng ll9) c= ( bound_QC-variables Al) by RELAT_1:def 19;

          then

          reconsider a as FinSequence of ( HCar Al) by A13, FINSEQ_1:def 4;

          ( the_arity_of r) = ( len a) by A11, A12, MARGREL1:def 10;

          hence thesis by A10, A13, CARD_1:def 7;

        end;

        for b be object holds b in ( rng f) implies b in ( relations_on ( HCar Al))

        proof

          let b be object;

          reconsider bb = b as set by TARSKI: 1;

          assume b in ( rng f);

          then

          consider a be object such that

           A14: a in ( dom f) and

           A15: b = (f . a) by FUNCT_1:def 3;

          consider P9 such that

           A16: P9 = a & (f . a) = { ll where ll be CQC-variable_list of ( the_arity_of P9), Al : CX |- (P9 ! ll) } by A3, A14;

          for c be object holds c in bb implies c in (( HCar Al) * )

          proof

            let c be object;

            assume c in bb;

            then

            consider ll be CQC-variable_list of ( the_arity_of P9), Al such that

             A17: c = ll and CX |- (P9 ! ll) by A15, A16;

            ( rng ll) c= ( bound_QC-variables Al) by RELAT_1:def 19;

            then ll is FinSequence of ( HCar Al) by FINSEQ_1:def 4;

            hence thesis by A17, FINSEQ_1:def 11;

          end;

          then

           A18: bb c= (( HCar Al) * );

          for fin,fin9 be FinSequence of ( HCar Al) st fin in bb & fin9 in bb holds ( len fin) = ( len fin9)

          proof

            let fin,fin9 be FinSequence of ( HCar Al);

            assume that

             A19: fin in bb and

             A20: fin9 in bb;

            ex ll be CQC-variable_list of ( the_arity_of P9), Al st fin = ll & CX |- (P9 ! ll) by A15, A16, A19;

            then

             A21: ( len fin) = ( the_arity_of P9) by CARD_1:def 7;

            ex ll9 be CQC-variable_list of ( the_arity_of P9), Al st fin9 = ll9 & CX |- (P9 ! ll9) by A15, A16, A20;

            hence thesis by A21, CARD_1:def 7;

          end;

          hence thesis by A18, MARGREL1:def 7;

        end;

        then ( rng f) c= ( relations_on ( HCar Al));

        then

        reconsider f as Function of A, ( relations_on ( HCar Al)) by A3, FUNCT_2: 2;

        reconsider f as interpretation of Al, ( HCar Al) by A8, VALUAT_1:def 5;

        take f;

        thus thesis by A4;

      end;

    end

    definition

      let Al;

      :: HENMODEL:def6

      func valH (Al) -> Element of ( Valuations_in (Al,( HCar Al))) equals ( id ( bound_QC-variables Al));

      coherence by VALUAT_1:def 1;

    end

    begin

    reserve JH for Henkin_interpretation of CX;

    theorem :: HENMODEL:14

    

     Th14: (( valH Al) *' ll) = ll

    proof

      

       A1: for i st i in ( dom (( valH Al) *' ll)) holds (( valH Al) . (ll . i)) = (ll . i)

      proof

        

         A2: ( dom (( valH Al) *' ll)) c= ( dom ll) by RELAT_1: 25;

        let i;

        assume i in ( dom (( valH Al) *' ll));

        then

         A3: (ll . i) in ( rng ll) by A2, FUNCT_1: 3;

        ( rng ll) c= ( bound_QC-variables Al) by RELAT_1:def 19;

        hence thesis by A3, FUNCT_1: 18;

      end;

      

       A4: for i st 1 <= i & i <= k holds (( valH Al) . (ll . i)) = (ll . i)

      proof

        let i such that

         A5: 1 <= i and

         A6: i <= k;

        i <= ( len (( valH Al) *' ll)) by A6, VALUAT_1:def 3;

        then i in ( dom (( valH Al) *' ll)) by A5, FINSEQ_3: 25;

        hence thesis by A1;

      end;

      

       A7: ( len ll) = k by CARD_1:def 7;

      then

       A8: ( dom ll) = ( Seg k) by FINSEQ_1:def 3;

      

       A9: for i be Nat st i in ( dom ll) holds ((( valH Al) *' ll) . i) = (ll . i)

      proof

        let i be Nat such that

         A10: i in ( dom ll);

        reconsider i as Nat;

        

         A11: 1 <= i & i <= k by A8, A10, FINSEQ_1: 1;

        then ((( valH Al) *' ll) . i) = (( valH Al) . (ll . i)) by VALUAT_1:def 3;

        hence thesis by A4, A11;

      end;

      ( len (( valH Al) *' ll)) = k by VALUAT_1:def 3;

      hence thesis by A7, A9, FINSEQ_2: 9;

    end;

    theorem :: HENMODEL:15

    

     Th15: |- (f ^ <*( VERUM Al)*>)

    proof

      set PR = <* [(f ^ <*( VERUM Al)*>), 1]*>;

      

       A1: ( rng PR) = { [(f ^ <*( VERUM Al)*>), 1]} by FINSEQ_1: 38;

      now

        let a be object;

        assume a in ( rng PR);

        then

         A2: a = [(f ^ <*( VERUM Al)*>), 1] by A1, TARSKI:def 1;

        (f ^ <*( VERUM Al)*>) in ( set_of_CQC-WFF-seq Al) by CALCUL_1:def 6;

        hence a in [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :] by A2, CQC_THE1: 21, ZFMISC_1: 87;

      end;

      then ( rng PR) c= [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :];

      then

      reconsider PR as FinSequence of [:( set_of_CQC-WFF-seq Al), Proof_Step_Kinds :] by FINSEQ_1:def 4;

      now

        let n be Nat such that

         A3: 1 <= n and

         A4: n <= ( len PR);

        n <= 1 by A4, FINSEQ_1: 39;

        then n = 1 by A3, XXREAL_0: 1;

        then (PR . n) = [(f ^ <*( VERUM Al)*>), 1] by FINSEQ_1: 40;

        then ((PR . n) `1 ) = (f ^ <*( VERUM Al)*>) & ((PR . n) `2 ) = 1;

        hence (PR,n) is_a_correct_step by CALCUL_1:def 7;

      end;

      then

       A5: PR is a_proof by CALCUL_1:def 8;

      (PR . 1) = [(f ^ <*( VERUM Al)*>), 1] by FINSEQ_1: 40;

      then (PR . ( len PR)) = [(f ^ <*( VERUM Al)*>), 1] by FINSEQ_1: 40;

      then ((PR . ( len PR)) `1 ) = (f ^ <*( VERUM Al)*>);

      hence thesis by A5, CALCUL_1:def 9;

    end;

    theorem :: HENMODEL:16

    (JH,( valH Al)) |= ( VERUM Al) iff CX |- ( VERUM Al)

    proof

      set f = ( <*> ( CQC-WFF Al));

      ( rng f) c= CX & |- (f ^ <*( VERUM Al)*>) by Th15;

      hence thesis by VALUAT_1: 32;

    end;

    theorem :: HENMODEL:17

    (JH,( valH Al)) |= (P ! ll) iff CX |- (P ! ll)

    proof

      thus (JH,( valH Al)) |= (P ! ll) implies CX |- (P ! ll)

      proof

        set rel = (JH . P);

        reconsider rel as Element of ( relations_on ( HCar Al));

        assume (JH,( valH Al)) |= (P ! ll);

        then (( Valid ((P ! ll),JH)) . ( valH Al)) = TRUE by VALUAT_1:def 7;

        then (( valH Al) *' ll) in rel by VALUAT_1: 7;

        then ll in rel by Th14;

        then ex ll9 be CQC-variable_list of ( the_arity_of P), Al st ll9 = ll & CX |- (P ! ll9) by Def5;

        hence thesis;

      end;

      thus CX |- (P ! ll) implies (JH,( valH Al)) |= (P ! ll)

      proof

        P is QC-pred_symbol of ( the_arity_of P), Al by QC_LANG3: 1;

        then

         A1: ( the_arity_of P) = k by SUBSTUT2: 3;

        assume CX |- (P ! ll);

        then ll in (JH . P) by A1, Def5;

        then (( valH Al) *' ll) in (JH . P) by Th14;

        then (( Valid ((P ! ll),JH)) . ( valH Al)) = TRUE by VALUAT_1: 7;

        hence thesis by VALUAT_1:def 7;

      end;

    end;