The Mizar article:

Predicate Calculus for Boolean Valued Functions. Part V

by

Shunichi Kobayashi, and

Yatsuka Nakamura

Received August 17, 1999

Copyright (c) 1999 Association of Mizar Users

MML identifier: BVFUNC13

[ MML identifier index ]

environ

 vocabulary FUNCT_2, MARGREL1, PARTIT1, EQREL_1, ZF_LANG, BVFUNC_2, BVFUNC_1,
      T_1TOPSP;
 notation XBOOLE_0, SUBSET_1, MARGREL1, VALUAT_1, FRAENKEL, EQREL_1, BVFUNC_1,
      BVFUNC_2;
 constructors BVFUNC_2, BVFUNC_1;
 clusters MARGREL1, VALUAT_1, FRAENKEL;
 definitions BVFUNC_1;
 theorems T_1TOPSP, MARGREL1, BVFUNC_1, BVFUNC_2, BVFUNC11, BVFUNC12, VALUAT_1,
      PARTIT_2, BVFUNC_4;

begin :: Chap. 1  Predicate Calculus

reserve Y for non empty set,
        a,b for Element of Funcs(Y,BOOLEAN),
        G for Subset of PARTITIONS(Y),
        A, B for a_partition of Y;

Lm1:
 a '<' b implies All(a,A,G) '<' Ex(b,A,G)
 proof
  assume a '<' b;
then A1:All(a,A,G) '<' All(b,A,G) by PARTIT_2:13;
    All(b,A,G) '<' Ex(b,A,G) by BVFUNC_4:18;
  hence thesis by A1,BVFUNC_1:18;
 end;

theorem Th1: G is independent implies
All('not' All(a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G)
proof
  assume G is independent;
then A1:All(All(a,B,G),A,G) = All(All(a,A,G),B,G) by PARTIT_2:17;
A2:All('not' All(a,A,G),B,G) = 'not' Ex(All(a,A,G),B,G) by BVFUNC_2:21;
    All(All(a,B,G),A,G) '<' Ex(All(a,A,G),B,G) by A1,Lm1;
  hence thesis by A2,PARTIT_2:11;
end;

theorem Th2:
All(All('not' a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G)
 proof
A1:All('not' a,A,G) = B_INF('not' a,CompF(A,G)) by BVFUNC_2:def 9;
    let z be Element of Y;
    assume A2:Pj(All(All('not' a,A,G),B,G),z)=TRUE;
A3:z in EqClass(z,CompF(A,G)) & EqClass(z,CompF(A,G)) in CompF(A,G)
      by T_1TOPSP:def 1;
A4:z in EqClass(z,CompF(B,G)) &
      EqClass(z,CompF(B,G)) in CompF(B,G)
      by T_1TOPSP:def 1;
 now assume
        not (for x being Element of Y st x in EqClass(z,CompF(B,G)) holds
       Pj(All('not' a,A,G),x)=TRUE);
      then Pj(B_INF(All('not' a,A,G),CompF(B,G)),z) = FALSE by BVFUNC_1:def 19
;
      then Pj(All(All('not' a,A,G),B,G),z)=FALSE by BVFUNC_2:def 9;
      hence contradiction by A2,MARGREL1:43;
    end;
    then A5:Pj(All('not' a,A,G),z)=TRUE by A4;
      now assume
        not (for x being Element of Y st x in EqClass(z,CompF(A,G)) holds
         Pj('not' a,x)=TRUE);
      then Pj(B_INF('not' a,CompF(A,G)),z) = FALSE by BVFUNC_1:def 19;
      hence contradiction by A1,A5,MARGREL1:43;
    end;
    then Pj('not' a,z)=TRUE by A3;
    then 'not' Pj(a,z)=TRUE by VALUAT_1:def 5;
    then Pj(a,z)=FALSE by MARGREL1:41;
    then Pj(a,z)<>TRUE by MARGREL1:43;
    then Pj(B_INF(a,CompF(B,G)),z) = FALSE by A4,BVFUNC_1:def 19;
    then Pj(All(a,B,G),z)=FALSE by BVFUNC_2:def 9;
    then Pj(All(a,B,G),z)<>TRUE by MARGREL1:43;
    then Pj(B_INF(All(a,B,G),CompF(A,G)),z) = FALSE by A3,BVFUNC_1:def 19;
    then Pj(All(All(a,B,G),A,G),z)=FALSE by BVFUNC_2:def 9;
    then 'not' Pj(All(All(a,B,G),A,G),z)=TRUE by MARGREL1:41;
    hence thesis by VALUAT_1:def 5;
 end;

theorem Th3:
All('not' Ex(a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G)
proof
    All('not' Ex(a,A,G),B,G) = All(All('not' a,A,G),B,G) by BVFUNC_2:21;
  hence thesis by Th2;
end;

theorem Th4: G is independent implies
All(Ex('not' a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G)
proof
  assume A1:G is independent;
    Ex('not' a,A,G) = 'not' All(a,A,G) by BVFUNC_2:20;
then A2:All(Ex('not' a,A,G),B,G) = 'not' Ex(All(a,A,G),B,G) by BVFUNC_2:21;
    All(All(a,B,G),A,G) '<' Ex(All(a,A,G),B,G) by A1,BVFUNC11:11;
  hence thesis by A2,PARTIT_2:11;
end;

canceled;

theorem G is independent implies
Ex(All('not' a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G)
proof
  assume A1:G is independent;
then A2:Ex(All('not' a,A,G),B,G) '<' All(Ex('not' a,B,G),A,G) by PARTIT_2:19;
    All(Ex('not' a,B,G),A,G) '<' 'not' All(All(a,A,G),B,G) by A1,Th4;
  then Ex(All('not' a,A,G),B,G) '<' 'not' All(All(a,A,G),B,G) by A2,BVFUNC_1:18
;
  hence thesis by A1,PARTIT_2:17;
end;

theorem Th7: G is independent implies
Ex('not' Ex(a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G)
proof
  assume A1:G is independent;
A2:Ex('not' Ex(a,A,G),B,G) = 'not' All(Ex(a,A,G),B,G) by BVFUNC_2:20;
A3:All(All(a,B,G),A,G) = All(All(a,A,G),B,G) by A1,PARTIT_2:17;
    All(a,A,G) '<' Ex(a,A,G) by Lm1;
  then All(All(a,A,G),B,G) '<' All(Ex(a,A,G),B,G) by PARTIT_2:13;
  hence thesis by A2,A3,PARTIT_2:11;
end;

canceled;

theorem Th9: G is independent implies
'not' All(Ex(a,A,G),B,G) '<' 'not' Ex(All(a,B,G),A,G)
proof
  assume G is independent;
  then Ex(All(a,B,G),A,G) '<' All(Ex(a,A,G),B,G) by PARTIT_2:19;
  hence thesis by PARTIT_2:11;
end;

theorem Th10: G is independent implies
'not' Ex(Ex(a,A,G),B,G) '<' 'not' Ex(All(a,B,G),A,G)
proof
  assume G is independent;
then A1:Ex(Ex(a,A,G),B,G) = Ex(Ex(a,B,G),A,G) by PARTIT_2:18;
    All(a,B,G) '<' Ex(a,B,G) by Lm1;
  then Ex(All(a,B,G),A,G) '<' Ex(Ex(a,A,G),B,G) by A1,PARTIT_2:15;
  hence thesis by PARTIT_2:11;
end;

theorem Th11:
'not' Ex(Ex(a,A,G),B,G) '<' 'not' All(Ex(a,B,G),A,G)
 proof
A1:Ex(a,A,G) = B_SUP(a,CompF(A,G)) by BVFUNC_2:def 10;
    let z be Element of Y;
    assume Pj('not' Ex(Ex(a,A,G),B,G),z)=TRUE;
    then 'not' Pj(Ex(Ex(a,A,G),B,G),z)=TRUE by VALUAT_1:def 5;
    then A2:Pj(Ex(Ex(a,A,G),B,G),z)=FALSE by MARGREL1:41;
A3:now assume
        ex x being Element of Y st
            x in EqClass(z,CompF(B,G)) & Pj(Ex(a,A,G),x)=TRUE;
      then Pj(B_SUP(Ex(a,A,G),CompF(B,G)),z) = TRUE by BVFUNC_1:def 20;
      then Pj(Ex(Ex(a,A,G),B,G),z)=TRUE by BVFUNC_2:def 10;
      hence contradiction by A2,MARGREL1:43;
    end;
A4:for x being Element of Y st x in EqClass(z,CompF(B,G)) holds
   (for y being Element of Y st y in EqClass(x,CompF(A,G)) holds Pj(a,y)<>TRUE)
    proof
      let x be Element of Y;
      assume x in EqClass(z,CompF(B,G));
      then Pj(Ex(a,A,G),x)<>TRUE by A3;
      hence thesis by A1,BVFUNC_1:def 20;
    end;
    A5:z in EqClass(z,CompF(A,G)) by T_1TOPSP:def 1;
      for x being Element of Y st x in EqClass(z,CompF(B,G)) holds Pj(a,x)<>
TRUE
    proof
      let x be Element of Y;
      assume A6:x in EqClass(z,CompF(B,G));
        x in EqClass(x,CompF(A,G)) by T_1TOPSP:def 1;
      hence thesis by A4,A6;
    end;
    then Pj(B_SUP(a,CompF(B,G)),z) = FALSE by BVFUNC_1:def 20;
    then Pj(Ex(a,B,G),z)=FALSE by BVFUNC_2:def 10;
    then Pj(Ex(a,B,G),z)<>TRUE by MARGREL1:43;
    then Pj(B_INF(Ex(a,B,G),CompF(A,G)),z) = FALSE by A5,BVFUNC_1:def 19;
    then Pj(All(Ex(a,B,G),A,G),z)=FALSE by BVFUNC_2:def 9;
    then 'not' Pj(All(Ex(a,B,G),A,G),z)=TRUE by MARGREL1:41;
    hence thesis by VALUAT_1:def 5;
 end;

canceled 2;

theorem G is independent implies
'not' Ex(All(a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G)
proof
  assume G is independent;
  then All('not' All(a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G) by Th1;
  hence thesis by BVFUNC_2:21;
end;

theorem G is independent implies
'not' All(Ex(a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G)
proof
  assume G is independent;
  then A1:Ex('not' Ex(a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G) by Th7;
    Ex('not' Ex(a,A,G),B,G) = Ex(All('not' a,A,G),B,G) by BVFUNC_2:21;
  hence thesis by A1,BVFUNC12:5;
end;

theorem
  'not' Ex(Ex(a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G)
proof
    All('not' Ex(a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G) by Th3;
  hence thesis by BVFUNC_2:21;
end;

theorem Th17: G is independent implies
'not' Ex(All(a,A,G),B,G) '<' Ex('not' All(a,B,G),A,G)
proof
  assume G is independent;
  then A1:All('not' All(a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G) by Th1;
    'not' Ex(All(a,A,G),B,G) = All('not' All(a,A,G),B,G) by BVFUNC_2:21;
  hence thesis by A1,BVFUNC_2:20;
end;

theorem Th18: G is independent implies
'not' All(Ex(a,A,G),B,G) '<' Ex('not' All(a,B,G),A,G)
proof
  assume G is independent;
  then A1:Ex('not' Ex(a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G) by Th7;
  A2:'not' All(Ex(a,A,G),B,G) = Ex(All('not' a,A,G),B,G) by BVFUNC12:5;
    Ex('not' Ex(a,A,G),B,G) = Ex(All('not' a,A,G),B,G) by BVFUNC_2:21;
  hence thesis by A1,A2,BVFUNC_2:20;
end;

theorem Th19:
'not' Ex(Ex(a,A,G),B,G) '<' Ex('not' All(a,B,G),A,G)
proof
  A1:All('not' Ex(a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G) by Th3;
    'not' Ex(Ex(a,A,G),B,G) = All('not' Ex(a,A,G),B,G) by BVFUNC_2:21;
  hence thesis by A1,BVFUNC_2:20;
end;

theorem Th20: G is independent implies
'not' All(Ex(a,A,G),B,G) '<' All('not' All(a,B,G),A,G)
proof
  assume G is independent;
  then 'not' All(Ex(a,A,G),B,G) '<' 'not' Ex(All(a,B,G),A,G) by Th9;
  hence thesis by BVFUNC_2:21;
end;

theorem Th21: G is independent implies
'not' Ex(Ex(a,A,G),B,G) '<' All('not' All(a,B,G),A,G)
proof
  assume G is independent;
  then 'not' Ex(Ex(a,A,G),B,G) '<' 'not' Ex(All(a,B,G),A,G) by Th10;
  hence thesis by BVFUNC_2:21;
end;

theorem Th22:
'not' Ex(Ex(a,A,G),B,G) '<' Ex('not' Ex(a,B,G),A,G)
proof
  A1:'not' Ex(Ex(a,A,G),B,G) '<' 'not' All(Ex(a,B,G),A,G) by Th11;
    Ex('not' Ex(a,B,G),A,G) = Ex(All('not' a,B,G),A,G) by BVFUNC_2:21;
  hence thesis by A1,BVFUNC12:5;
end;

theorem Th23: G is independent implies
'not' Ex(Ex(a,A,G),B,G) = All('not' Ex(a,B,G),A,G)
proof
  assume G is independent;
  then 'not' Ex(Ex(a,A,G),B,G) = 'not' Ex(Ex(a,B,G),A,G) by PARTIT_2:18;
  hence thesis by BVFUNC_2:21;
end;

theorem Th24: G is independent implies
'not' All(Ex(a,A,G),B,G) '<' Ex(Ex('not' a,B,G),A,G)
proof
  assume G is independent;
  then 'not' All(Ex(a,A,G),B,G) '<' Ex('not' All(a,B,G),A,G) by Th18;
  hence thesis by BVFUNC_2:20;
end;

theorem Th25:
'not' Ex(Ex(a,A,G),B,G) '<' Ex(Ex('not' a,B,G),A,G)
proof
    'not' Ex(Ex(a,A,G),B,G) '<' Ex('not' All(a,B,G),A,G) by Th19;
  hence thesis by BVFUNC_2:20;
end;

theorem Th26:
G is independent implies
'not' All(Ex(a,A,G),B,G) '<' All(Ex('not' a,B,G),A,G)
proof
  assume G is independent;
  then 'not' All(Ex(a,A,G),B,G) '<' All('not' All(a,B,G),A,G) by Th20;
  hence thesis by BVFUNC_2:20;
end;

theorem Th27:
G is independent implies
'not' Ex(Ex(a,A,G),B,G) '<' All(Ex('not' a,B,G),A,G)
proof
  assume G is independent;
  then 'not' Ex(Ex(a,A,G),B,G) '<' All('not' All(a,B,G),A,G) by Th21;
  hence thesis by BVFUNC_2:20;
end;

theorem Th28:
'not' Ex(Ex(a,A,G),B,G) '<' Ex(All('not' a,B,G),A,G)
proof
    'not' Ex(Ex(a,A,G),B,G) '<' Ex('not' Ex(a,B,G),A,G) by Th22;
  hence thesis by BVFUNC_2:21;
end;

theorem Th29: G is independent implies
'not' Ex(Ex(a,A,G),B,G) = All(All('not' a,B,G),A,G)
proof
  assume G is independent;
  then 'not' Ex(Ex(a,A,G),B,G) = All('not' Ex(a,B,G),A,G) by Th23;
  hence thesis by BVFUNC_2:21;
end;

theorem G is independent implies
Ex('not' Ex(a,A,G),B,G) '<' 'not' Ex(All(a,B,G),A,G)
proof
  assume G is independent;
  then A1:'not' All(Ex(a,A,G),B,G) '<' 'not' Ex(All(a,B,G),A,G) by Th9;
    'not' All(Ex(a,A,G),B,G) = Ex(All('not' a,A,G),B,G) by BVFUNC12:5;
  hence thesis by A1,BVFUNC_2:21;
end;

theorem
  All('not' Ex(a,A,G),B,G) '<' 'not' Ex(All(a,B,G),A,G)
proof
A1:Ex(a,A,G) = B_SUP(a,CompF(A,G)) by BVFUNC_2:def 10;
A2:All('not' Ex(a,A,G),B,G) = B_INF('not' Ex(a,A,G),CompF(B,G))
     by BVFUNC_2:def 9;
A3:All(a,B,G) = B_INF(a,CompF(B,G)) by BVFUNC_2:def 9;
A4:Ex(All(a,B,G),A,G) = B_SUP(All(a,B,G),CompF(A,G))
    by BVFUNC_2:def 10;
    let z be Element of Y;
    assume A5:Pj(All('not' Ex(a,A,G),B,G),z)=TRUE;
A6:z in EqClass(z,CompF(B,G)) &
      EqClass(z,CompF(B,G)) in CompF(B,G)
      by T_1TOPSP:def 1;
      now assume
        not (for x being Element of Y st x in EqClass(z,CompF(B,G)) holds
       Pj('not' Ex(a,A,G),x)=TRUE);
      then Pj(All('not' Ex(a,A,G),B,G),z)=FALSE by A2,BVFUNC_1:def 19;
      hence contradiction by A5,MARGREL1:43;
    end;
    then Pj('not' Ex(a,A,G),z)=TRUE by A6;
    then 'not' Pj(Ex(a,A,G),z)=TRUE by VALUAT_1:def 5;
    then A7:Pj(Ex(a,A,G),z)=FALSE by MARGREL1:41;
    A8: now assume
        ex x being Element of Y st
            x in EqClass(z,CompF(A,G)) & Pj(a,x)=TRUE;
      then Pj(B_SUP(a,CompF(A,G)),z) = TRUE by BVFUNC_1:def 20;
      hence contradiction by A1,A7,MARGREL1:43;
    end;
      for x being Element of Y st
            x in EqClass(z,CompF(A,G)) holds Pj(All(a,B,G),x)<>TRUE
    proof
      let x be Element of Y;
      assume x in EqClass(z,CompF(A,G));
      then A9:Pj(a,x)<>TRUE by A8;
        x in EqClass(x,CompF(B,G)) & EqClass(x,CompF(B,G)) in CompF(B,G)
        by T_1TOPSP:def 1;
      then Pj(All(a,B,G),x)=FALSE by A3,A9,BVFUNC_1:def 19;
      hence thesis by MARGREL1:43;
    end;
    then Pj(B_SUP(All(a,B,G),CompF(A,G)),z) = FALSE by BVFUNC_1:def 20;
    then 'not' Pj(Ex(All(a,B,G),A,G),z)=TRUE by A4,MARGREL1:41;
    hence thesis by VALUAT_1:def 5;
end;

theorem
  All('not' Ex(a,A,G),B,G) '<' 'not' All(Ex(a,B,G),A,G)
proof
    'not' Ex(Ex(a,A,G),B,G) = All('not' Ex(a,A,G),B,G) by BVFUNC_2:21;
  hence thesis by Th11;
end;

theorem G is independent implies
All('not' Ex(a,A,G),B,G) = 'not' Ex(Ex(a,B,G),A,G)
proof
  assume A1:G is independent;
    'not' Ex(Ex(a,A,G),B,G) = All('not' Ex(a,A,G),B,G) by BVFUNC_2:21;
  hence thesis by A1,PARTIT_2:18;
end;

theorem G is independent implies
Ex('not' All(a,A,G),B,G) = Ex('not' All(a,B,G),A,G)
proof
  assume A1:G is independent;
    'not' All(All(a,A,G),B,G) = Ex('not' All(a,A,G),B,G) by BVFUNC_2:20;
  hence thesis by A1,BVFUNC11:17;
end;

theorem G is independent implies
All('not' All(a,A,G),B,G) '<' Ex('not' All(a,B,G),A,G)
proof
  assume A1:G is independent;
    'not' Ex(All(a,A,G),B,G) = All('not' All(a,A,G),B,G) by BVFUNC_2:21;
  hence thesis by A1,Th17;
end;

theorem G is independent implies
Ex('not' Ex(a,A,G),B,G) '<' Ex('not' All(a,B,G),A,G)
proof
  assume A1:G is independent;
  A2:'not' All(Ex(a,A,G),B,G) = Ex(All('not' a,A,G),B,G) by BVFUNC12:5;
    Ex('not' Ex(a,A,G),B,G) = Ex(All('not' a,A,G),B,G) by BVFUNC_2:21;
  hence thesis by A1,A2,Th18;
end;

theorem
  All('not' Ex(a,A,G),B,G) '<' Ex('not' All(a,B,G),A,G)
proof
    'not' Ex(Ex(a,A,G),B,G) = All('not' Ex(a,A,G),B,G) by BVFUNC_2:21;
  hence thesis by Th19;
end;

theorem G is independent implies
Ex('not' Ex(a,A,G),B,G) '<' All('not' All(a,B,G),A,G)
proof
  assume A1:G is independent;
  A2:'not' All(Ex(a,A,G),B,G) = Ex(All('not' a,A,G),B,G) by BVFUNC12:5;
    Ex('not' Ex(a,A,G),B,G) = Ex(All('not' a,A,G),B,G) by BVFUNC_2:21;
  hence thesis by A1,A2,Th20;
end;

theorem
  G is independent implies
All('not' Ex(a,A,G),B,G) '<' All('not' All(a,B,G),A,G)
proof
  assume G is independent;
  then 'not' Ex(Ex(a,A,G),B,G) '<' All('not' All(a,B,G),A,G) by Th21;
  hence thesis by BVFUNC_2:21;
end;

theorem
  All('not' Ex(a,A,G),B,G) '<' Ex('not' Ex(a,B,G),A,G)
proof
    'not' Ex(Ex(a,A,G),B,G) = All('not' Ex(a,A,G),B,G) by BVFUNC_2:21;
  hence thesis by Th22;
end;

theorem
  G is independent implies
All('not' Ex(a,A,G),B,G) = All('not' Ex(a,B,G),A,G)
proof
  assume A1:G is independent;
    'not' Ex(Ex(a,A,G),B,G) = All('not' Ex(a,A,G),B,G) by BVFUNC_2:21;
  hence thesis by A1,Th23;
end;

theorem
  G is independent implies
Ex('not' Ex(a,A,G),B,G) '<' Ex(Ex('not' a,B,G),A,G)
proof
  assume A1:G is independent;
  A2:'not' All(Ex(a,A,G),B,G) = Ex(All('not' a,A,G),B,G) by BVFUNC12:5;
    Ex('not' Ex(a,A,G),B,G) = Ex(All('not' a,A,G),B,G) by BVFUNC_2:21;
  hence thesis by A1,A2,Th24;
end;

theorem
  All('not' Ex(a,A,G),B,G) '<' Ex(Ex('not' a,B,G),A,G)
proof
    'not' Ex(Ex(a,A,G),B,G) = All('not' Ex(a,A,G),B,G) by BVFUNC_2:21;
  hence thesis by Th25;
end;

theorem
  G is independent implies
Ex('not' Ex(a,A,G),B,G) '<' All(Ex('not' a,B,G),A,G)
proof
  assume A1:G is independent;
  A2:'not' All(Ex(a,A,G),B,G) = Ex(All('not' a,A,G),B,G) by BVFUNC12:5;
    Ex('not' Ex(a,A,G),B,G) = Ex(All('not' a,A,G),B,G) by BVFUNC_2:21;
  hence thesis by A1,A2,Th26;
end;

theorem G is independent implies
All('not' Ex(a,A,G),B,G) '<' All(Ex('not' a,B,G),A,G)
proof
  assume A1:G is independent;
    'not' Ex(Ex(a,A,G),B,G) = All('not' Ex(a,A,G),B,G) by BVFUNC_2:21;
  hence thesis by A1,Th27;
end;

theorem
  All('not' Ex(a,A,G),B,G) '<' Ex(All('not' a,B,G),A,G)
proof
    'not' Ex(Ex(a,A,G),B,G) = All('not' Ex(a,A,G),B,G) by BVFUNC_2:21;
  hence thesis by Th28;
end;

theorem G is independent implies
All('not' Ex(a,A,G),B,G) = All(All('not' a,B,G),A,G)
proof
  assume A1:G is independent;
    'not' Ex(Ex(a,A,G),B,G) = All('not' Ex(a,A,G),B,G) by BVFUNC_2:21;
  hence thesis by A1,Th29;
end;

theorem G is independent implies
Ex(All('not' a,A,G),B,G) '<' 'not' Ex(All(a,B,G),A,G)
proof
  assume A1:G is independent;
    'not' All(Ex(a,A,G),B,G) = Ex(All('not' a,A,G),B,G) by BVFUNC12:5;
  hence thesis by A1,Th9;
end;

theorem G is independent implies
All(All('not' a,A,G),B,G) '<' 'not' Ex(All(a,B,G),A,G)
proof
  assume A1:G is independent;
  A2:'not' Ex(Ex(a,A,G),B,G) = All('not' Ex(a,A,G),B,G) by BVFUNC_2:21;
    All('not' Ex(a,A,G),B,G) = All(All('not' a,A,G),B,G) by BVFUNC_2:21;
  hence thesis by A1,A2,Th10;
end;

theorem
  All(All('not' a,A,G),B,G) '<' 'not' All(Ex(a,B,G),A,G)
proof
  A1:'not' Ex(Ex(a,A,G),B,G) = All('not' Ex(a,A,G),B,G) by BVFUNC_2:21;
    All('not' Ex(a,A,G),B,G) = All(All('not' a,A,G),B,G) by BVFUNC_2:21;
  hence thesis by A1,Th11;
end;

theorem G is independent implies
All(All('not' a,A,G),B,G) '<' 'not' Ex(Ex(a,B,G),A,G)
proof
  assume A1:G is independent;
  A2:'not' Ex(Ex(a,A,G),B,G) = All('not' Ex(a,A,G),B,G) by BVFUNC_2:21;
    All('not' Ex(a,A,G),B,G) = All(All('not' a,A,G),B,G) by BVFUNC_2:21;
  hence thesis by A1,A2,PARTIT_2:18;
end;

theorem G is independent implies
Ex(Ex('not' a,A,G),B,G) '<' Ex('not' All(a,B,G),A,G)
proof
  assume A1:G is independent;
    'not' All(All(a,A,G),B,G) = Ex(Ex('not' a,A,G),B,G) by BVFUNC12:7;
  hence thesis by A1,BVFUNC11:17;
end;

theorem G is independent implies
All(Ex('not' a,A,G),B,G) '<' Ex('not' All(a,B,G),A,G)
proof
  assume A1:G is independent;
    'not' Ex(All(a,A,G),B,G) = All(Ex('not' a,A,G),B,G) by BVFUNC12:6;
  hence thesis by A1,Th17;
end;

theorem G is independent implies
Ex(All('not' a,A,G),B,G) '<' Ex('not' All(a,B,G),A,G)
proof
  assume A1:G is independent;
    'not' All(Ex(a,A,G),B,G) = Ex(All('not' a,A,G),B,G) by BVFUNC12:5;
  hence thesis by A1,Th18;
end;

theorem
  All(All('not' a,A,G),B,G) '<' Ex('not' All(a,B,G),A,G)
proof
  A1:'not' Ex(Ex(a,A,G),B,G) = All('not' Ex(a,A,G),B,G) by BVFUNC_2:21;
    All('not' Ex(a,A,G),B,G) = All(All('not' a,A,G),B,G) by BVFUNC_2:21;
  hence thesis by A1,Th19;
end;

theorem G is independent implies
Ex(All('not' a,A,G),B,G) '<' All('not' All(a,B,G),A,G)
proof
  assume A1:G is independent;
    'not' All(Ex(a,A,G),B,G) = Ex(All('not' a,A,G),B,G) by BVFUNC12:5;
  hence thesis by A1,Th20;
end;

theorem G is independent implies
All(All('not' a,A,G),B,G) '<' All('not' All(a,B,G),A,G)
proof
  assume A1:G is independent;
  A2:'not' Ex(Ex(a,A,G),B,G) = All('not' Ex(a,A,G),B,G) by BVFUNC_2:21;
    All('not' Ex(a,A,G),B,G) = All(All('not' a,A,G),B,G) by BVFUNC_2:21;
  hence thesis by A1,A2,Th21;
end;

theorem
  All(All('not' a,A,G),B,G) '<' Ex('not' Ex(a,B,G),A,G)
proof
  A1:'not' Ex(Ex(a,A,G),B,G) = All('not' Ex(a,A,G),B,G) by BVFUNC_2:21;
    All('not' Ex(a,A,G),B,G) = All(All('not' a,A,G),B,G) by BVFUNC_2:21;
  hence thesis by A1,Th22;
end;

theorem G is independent implies
All(All('not' a,A,G),B,G) = All('not' Ex(a,B,G),A,G)
proof
  assume G is independent;
  then All(All('not' a,A,G),B,G) = All(All('not' a,B,G),A,G) by PARTIT_2:17;
  hence thesis by BVFUNC_2:21;
end;

canceled;

theorem
  All(Ex('not' a,A,G),B,G) '<' Ex(Ex('not' a,B,G),A,G)
proof
    'not' Ex(All(a,A,G),B,G) = All(Ex('not' a,A,G),B,G) by BVFUNC12:6;
  hence thesis by BVFUNC11:15;
end;

theorem G is independent implies
Ex(All('not' a,A,G),B,G) '<' Ex(Ex('not' a,B,G),A,G)
proof
  assume A1:G is independent;
    'not' All(Ex(a,A,G),B,G) = Ex(All('not' a,A,G),B,G) by BVFUNC12:5;
  hence thesis by A1,Th24;
end;