:: BVFUNC24 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: BVFUNC24:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J being a_partition of Y st G = {A,B,C,D,E,F,J} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & B <> C & B <> D & B <> E & B <> F & B <> J & C <> D & C <> E & C <> F & C <> J & D <> E & D <> F & D <> J & E <> F & E <> J & F <> J holds
CompF A,G = ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J
proof end;

theorem Th2: :: BVFUNC24:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J being a_partition of Y st G = {A,B,C,D,E,F,J} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & B <> C & B <> D & B <> E & B <> F & B <> J & C <> D & C <> E & C <> F & C <> J & D <> E & D <> F & D <> J & E <> F & E <> J & F <> J holds
CompF B,G = ((((A '/\' C) '/\' D) '/\' E) '/\' F) '/\' J
proof end;

theorem Th3: :: BVFUNC24:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J being a_partition of Y st G = {A,B,C,D,E,F,J} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & B <> C & B <> D & B <> E & B <> F & B <> J & C <> D & C <> E & C <> F & C <> J & D <> E & D <> F & D <> J & E <> F & E <> J & F <> J holds
CompF C,G = ((((A '/\' B) '/\' D) '/\' E) '/\' F) '/\' J
proof end;

theorem Th4: :: BVFUNC24:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J being a_partition of Y st G = {A,B,C,D,E,F,J} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & B <> C & B <> D & B <> E & B <> F & B <> J & C <> D & C <> E & C <> F & C <> J & D <> E & D <> F & D <> J & E <> F & E <> J & F <> J holds
CompF D,G = ((((A '/\' B) '/\' C) '/\' E) '/\' F) '/\' J
proof end;

theorem Th5: :: BVFUNC24:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J being a_partition of Y st G = {A,B,C,D,E,F,J} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & B <> C & B <> D & B <> E & B <> F & B <> J & C <> D & C <> E & C <> F & C <> J & D <> E & D <> F & D <> J & E <> F & E <> J & F <> J holds
CompF E,G = ((((A '/\' B) '/\' C) '/\' D) '/\' F) '/\' J
proof end;

theorem Th6: :: BVFUNC24:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J being a_partition of Y st G = {A,B,C,D,E,F,J} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & B <> C & B <> D & B <> E & B <> F & B <> J & C <> D & C <> E & C <> F & C <> J & D <> E & D <> F & D <> J & E <> F & E <> J & F <> J holds
CompF F,G = ((((A '/\' B) '/\' C) '/\' D) '/\' E) '/\' J
proof end;

theorem :: BVFUNC24:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J being a_partition of Y st G = {A,B,C,D,E,F,J} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & B <> C & B <> D & B <> E & B <> F & B <> J & C <> D & C <> E & C <> F & C <> J & D <> E & D <> F & D <> J & E <> F & E <> J & F <> J holds
CompF J,G = ((((A '/\' B) '/\' C) '/\' D) '/\' E) '/\' F
proof end;

theorem Th8: :: BVFUNC24:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C, D, E, F, J being set
for h being Function
for A', B', C', D', E', F', J' being set st A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & B <> C & B <> D & B <> E & B <> F & B <> J & C <> D & C <> E & C <> F & C <> J & D <> E & D <> F & D <> J & E <> F & E <> J & F <> J & h = ((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (A .--> A') holds
( h . A = A' & h . B = B' & h . C = C' & h . D = D' & h . E = E' & h . F = F' & h . J = J' )
proof end;

theorem Th9: :: BVFUNC24:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C, D, E, F, J being set
for h being Function
for A', B', C', D', E', F', J' being set st h = ((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (A .--> A') holds
dom h = {A,B,C,D,E,F,J}
proof end;

theorem Th10: :: BVFUNC24:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C, D, E, F, J being set
for h being Function
for A', B', C', D', E', F', J' being set st h = ((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (A .--> A') holds
rng h = {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J)}
proof end;

theorem :: BVFUNC24:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J being a_partition of Y
for z, u being Element of Y st G is independent & G = {A,B,C,D,E,F,J} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & B <> C & B <> D & B <> E & B <> F & B <> J & C <> D & C <> E & C <> F & C <> J & D <> E & D <> F & D <> J & E <> F & E <> J & F <> J holds
EqClass u,(((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) meets EqClass z,A
proof end;

theorem :: BVFUNC24:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J being a_partition of Y
for z, u being Element of Y st G is independent & G = {A,B,C,D,E,F,J} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & B <> C & B <> D & B <> E & B <> F & B <> J & C <> D & C <> E & C <> F & C <> J & D <> E & D <> F & D <> J & E <> F & E <> J & F <> J & EqClass z,((((C '/\' D) '/\' E) '/\' F) '/\' J) = EqClass u,((((C '/\' D) '/\' E) '/\' F) '/\' J) holds
EqClass u,(CompF A,G) meets EqClass z,(CompF B,G)
proof end;

theorem Th13: :: BVFUNC24:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J, M being a_partition of Y st G = {A,B,C,D,E,F,J,M} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & C <> D & C <> E & C <> F & C <> J & C <> M & D <> E & D <> F & D <> J & D <> M & E <> F & E <> J & E <> M & F <> J & F <> M & J <> M holds
CompF A,G = (((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M
proof end;

theorem Th14: :: BVFUNC24:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J, M being a_partition of Y st G = {A,B,C,D,E,F,J,M} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & C <> D & C <> E & C <> F & C <> J & C <> M & D <> E & D <> F & D <> J & D <> M & E <> F & E <> J & E <> M & F <> J & F <> M & J <> M holds
CompF B,G = (((((A '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M
proof end;

theorem Th15: :: BVFUNC24:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J, M being a_partition of Y st G = {A,B,C,D,E,F,J,M} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & C <> D & C <> E & C <> F & C <> J & C <> M & D <> E & D <> F & D <> J & D <> M & E <> F & E <> J & E <> M & F <> J & F <> M & J <> M holds
CompF C,G = (((((A '/\' B) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M
proof end;

theorem Th16: :: BVFUNC24:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J, M being a_partition of Y st G = {A,B,C,D,E,F,J,M} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & C <> D & C <> E & C <> F & C <> J & C <> M & D <> E & D <> F & D <> J & D <> M & E <> F & E <> J & E <> M & F <> J & F <> M & J <> M holds
CompF D,G = (((((A '/\' B) '/\' C) '/\' E) '/\' F) '/\' J) '/\' M
proof end;

theorem Th17: :: BVFUNC24:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J, M being a_partition of Y st G = {A,B,C,D,E,F,J,M} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & C <> D & C <> E & C <> F & C <> J & C <> M & D <> E & D <> F & D <> J & D <> M & E <> F & E <> J & E <> M & F <> J & F <> M & J <> M holds
CompF E,G = (((((A '/\' B) '/\' C) '/\' D) '/\' F) '/\' J) '/\' M
proof end;

theorem Th18: :: BVFUNC24:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J, M being a_partition of Y st G = {A,B,C,D,E,F,J,M} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & C <> D & C <> E & C <> F & C <> J & C <> M & D <> E & D <> F & D <> J & D <> M & E <> F & E <> J & E <> M & F <> J & F <> M & J <> M holds
CompF F,G = (((((A '/\' B) '/\' C) '/\' D) '/\' E) '/\' J) '/\' M
proof end;

theorem Th19: :: BVFUNC24:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J, M being a_partition of Y st G = {A,B,C,D,E,F,J,M} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & C <> D & C <> E & C <> F & C <> J & C <> M & D <> E & D <> F & D <> J & D <> M & E <> F & E <> J & E <> M & F <> J & F <> M & J <> M holds
CompF J,G = (((((A '/\' B) '/\' C) '/\' D) '/\' E) '/\' F) '/\' M
proof end;

theorem :: BVFUNC24:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J, M being a_partition of Y st G = {A,B,C,D,E,F,J,M} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & C <> D & C <> E & C <> F & C <> J & C <> M & D <> E & D <> F & D <> J & D <> M & E <> F & E <> J & E <> M & F <> J & F <> M & J <> M holds
CompF M,G = (((((A '/\' B) '/\' C) '/\' D) '/\' E) '/\' F) '/\' J
proof end;

theorem Th21: :: BVFUNC24:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C, D, E, F, J, M being set
for h being Function
for A', B', C', D', E', F', J', M' being set st A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & C <> D & C <> E & C <> F & C <> J & C <> M & D <> E & D <> F & D <> J & D <> M & E <> F & E <> J & E <> M & F <> J & F <> M & J <> M & h = (((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (M .--> M')) +* (A .--> A') holds
( h . B = B' & h . C = C' & h . D = D' & h . E = E' & h . F = F' & h . J = J' )
proof end;

theorem Th22: :: BVFUNC24:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C, D, E, F, J, M being set
for h being Function
for A', B', C', D', E', F', J', M' being set st h = (((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (M .--> M')) +* (A .--> A') holds
dom h = {A,B,C,D,E,F,J,M}
proof end;

theorem Th23: :: BVFUNC24:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C, D, E, F, J, M being set
for h being Function
for A', B', C', D', E', F', J', M' being set st h = (((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (M .--> M')) +* (A .--> A') holds
rng h = {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M)}
proof end;

theorem :: BVFUNC24:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J, M being a_partition of Y
for z, u being Element of Y st G is independent & G = {A,B,C,D,E,F,J,M} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & C <> D & C <> E & C <> F & C <> J & C <> M & D <> E & D <> F & D <> J & D <> M & E <> F & E <> J & E <> M & F <> J & F <> M & J <> M holds
(EqClass u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) /\ (EqClass z,A) <> {}
proof end;

theorem :: BVFUNC24:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J, M being a_partition of Y
for z, u being Element of Y st G is independent & G = {A,B,C,D,E,F,J,M} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & C <> D & C <> E & C <> F & C <> J & C <> M & D <> E & D <> F & D <> J & D <> M & E <> F & E <> J & E <> M & F <> J & F <> M & J <> M & EqClass z,(((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) = EqClass u,(((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) holds
EqClass u,(CompF A,G) meets EqClass z,(CompF B,G)
proof end;

Lm1: for x, X, y being set holds
( x in union {X,{y}} iff ( x in X or x = y ) )
proof end;

definition
let x1, x2, x3, x4, x5, x6, x7, x8, x9 be set ;
func {x1,x2,x3,x4,x5,x6,x7,x8,x9} -> set means :Def1: :: BVFUNC24:def 1
for x being set holds
( x in it iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 ) )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 ) ) ) & ( for x being set holds
( x in b2 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines { BVFUNC24:def 1 :
for x1, x2, x3, x4, x5, x6, x7, x8, x9, b10 being set holds
( b10 = {x1,x2,x3,x4,x5,x6,x7,x8,x9} iff for x being set holds
( x in b10 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 ) ) );

Lm2: for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8,x9}
proof end;

theorem :: BVFUNC24:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th27: :: BVFUNC24:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1} \/ {x2,x3,x4,x5,x6,x7,x8,x9}
proof end;

theorem Th28: :: BVFUNC24:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2} \/ {x3,x4,x5,x6,x7,x8,x9}
proof end;

theorem Th29: :: BVFUNC24:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3} \/ {x4,x5,x6,x7,x8,x9}
proof end;

theorem :: BVFUNC24:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8,x9} by Lm2;

theorem Th31: :: BVFUNC24:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4,x5} \/ {x6,x7,x8,x9}
proof end;

theorem Th32: :: BVFUNC24:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4,x5,x6} \/ {x7,x8,x9}
proof end;

theorem Th33: :: BVFUNC24:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4,x5,x6,x7} \/ {x8,x9}
proof end;

theorem :: BVFUNC24:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4,x5,x6,x7,x8} \/ {x9}
proof end;

theorem Th35: :: BVFUNC24:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J, M, N being a_partition of Y st G = {A,B,C,D,E,F,J,M,N} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & A <> N & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & B <> N & C <> D & C <> E & C <> F & C <> J & C <> M & C <> N & D <> E & D <> F & D <> J & D <> M & D <> N & E <> F & E <> J & E <> M & E <> N & F <> J & F <> M & F <> N & J <> M & J <> N & M <> N holds
CompF A,G = ((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N
proof end;

theorem Th36: :: BVFUNC24:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J, M, N being a_partition of Y st G = {A,B,C,D,E,F,J,M,N} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & A <> N & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & B <> N & C <> D & C <> E & C <> F & C <> J & C <> M & C <> N & D <> E & D <> F & D <> J & D <> M & D <> N & E <> F & E <> J & E <> M & E <> N & F <> J & F <> M & F <> N & J <> M & J <> N & M <> N holds
CompF B,G = ((((((A '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N
proof end;

theorem Th37: :: BVFUNC24:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J, M, N being a_partition of Y st G = {A,B,C,D,E,F,J,M,N} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & A <> N & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & B <> N & C <> D & C <> E & C <> F & C <> J & C <> M & C <> N & D <> E & D <> F & D <> J & D <> M & D <> N & E <> F & E <> J & E <> M & E <> N & F <> J & F <> M & F <> N & J <> M & J <> N & M <> N holds
CompF C,G = ((((((A '/\' B) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N
proof end;

theorem Th38: :: BVFUNC24:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J, M, N being a_partition of Y st G = {A,B,C,D,E,F,J,M,N} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & A <> N & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & B <> N & C <> D & C <> E & C <> F & C <> J & C <> M & C <> N & D <> E & D <> F & D <> J & D <> M & D <> N & E <> F & E <> J & E <> M & E <> N & F <> J & F <> M & F <> N & J <> M & J <> N & M <> N holds
CompF D,G = ((((((A '/\' B) '/\' C) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N
proof end;

theorem Th39: :: BVFUNC24:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J, M, N being a_partition of Y st G = {A,B,C,D,E,F,J,M,N} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & A <> N & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & B <> N & C <> D & C <> E & C <> F & C <> J & C <> M & C <> N & D <> E & D <> F & D <> J & D <> M & D <> N & E <> F & E <> J & E <> M & E <> N & F <> J & F <> M & F <> N & J <> M & J <> N & M <> N holds
CompF E,G = ((((((A '/\' B) '/\' C) '/\' D) '/\' F) '/\' J) '/\' M) '/\' N
proof end;

theorem Th40: :: BVFUNC24:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J, M, N being a_partition of Y st G = {A,B,C,D,E,F,J,M,N} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & A <> N & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & B <> N & C <> D & C <> E & C <> F & C <> J & C <> M & C <> N & D <> E & D <> F & D <> J & D <> M & D <> N & E <> F & E <> J & E <> M & E <> N & F <> J & F <> M & F <> N & J <> M & J <> N & M <> N holds
CompF F,G = ((((((A '/\' B) '/\' C) '/\' D) '/\' E) '/\' J) '/\' M) '/\' N
proof end;

theorem Th41: :: BVFUNC24:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J, M, N being a_partition of Y st G = {A,B,C,D,E,F,J,M,N} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & A <> N & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & B <> N & C <> D & C <> E & C <> F & C <> J & C <> M & C <> N & D <> E & D <> F & D <> J & D <> M & D <> N & E <> F & E <> J & E <> M & E <> N & F <> J & F <> M & F <> N & J <> M & J <> N & M <> N holds
CompF J,G = ((((((A '/\' B) '/\' C) '/\' D) '/\' E) '/\' F) '/\' M) '/\' N
proof end;

theorem Th42: :: BVFUNC24:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J, M, N being a_partition of Y st G = {A,B,C,D,E,F,J,M,N} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & A <> N & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & B <> N & C <> D & C <> E & C <> F & C <> J & C <> M & C <> N & D <> E & D <> F & D <> J & D <> M & D <> N & E <> F & E <> J & E <> M & E <> N & F <> J & F <> M & F <> N & J <> M & J <> N & M <> N holds
CompF M,G = ((((((A '/\' B) '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' N
proof end;

theorem :: BVFUNC24:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J, M, N being a_partition of Y st G = {A,B,C,D,E,F,J,M,N} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & A <> N & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & B <> N & C <> D & C <> E & C <> F & C <> J & C <> M & C <> N & D <> E & D <> F & D <> J & D <> M & D <> N & E <> F & E <> J & E <> M & E <> N & F <> J & F <> M & F <> N & J <> M & J <> N & M <> N holds
CompF N,G = ((((((A '/\' B) '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M
proof end;

theorem Th44: :: BVFUNC24:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C, D, E, F, J, M, N being set
for h being Function
for A', B', C', D', E', F', J', M', N' being set st A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & A <> N & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & B <> N & C <> D & C <> E & C <> F & C <> J & C <> M & C <> N & D <> E & D <> F & D <> J & D <> M & D <> N & E <> F & E <> J & E <> M & E <> N & F <> J & F <> M & F <> N & J <> M & J <> N & M <> N & h = ((((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (M .--> M')) +* (N .--> N')) +* (A .--> A') holds
( h . A = A' & h . B = B' & h . C = C' & h . D = D' & h . E = E' & h . F = F' & h . J = J' & h . M = M' & h . N = N' )
proof end;

theorem Th45: :: BVFUNC24:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C, D, E, F, J, M, N being set
for h being Function
for A', B', C', D', E', F', J', M', N' being set st h = ((((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (M .--> M')) +* (N .--> N')) +* (A .--> A') holds
dom h = {A,B,C,D,E,F,J,M,N}
proof end;

theorem Th46: :: BVFUNC24:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C, D, E, F, J, M, N being set
for h being Function
for A', B', C', D', E', F', J', M', N' being set st h = ((((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (M .--> M')) +* (N .--> N')) +* (A .--> A') holds
rng h = {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)}
proof end;

theorem :: BVFUNC24:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J, M, N being a_partition of Y
for z, u being Element of Y st G is independent & G = {A,B,C,D,E,F,J,M,N} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & A <> N & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & B <> N & C <> D & C <> E & C <> F & C <> J & C <> M & C <> N & D <> E & D <> F & D <> J & D <> M & D <> N & E <> F & E <> J & E <> M & E <> N & F <> J & F <> M & F <> N & J <> M & J <> N & M <> N holds
(EqClass u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)) /\ (EqClass z,A) <> {}
proof end;

theorem :: BVFUNC24:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J, M, N being a_partition of Y
for z, u being Element of Y st G is independent & G = {A,B,C,D,E,F,J,M,N} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & A <> N & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & B <> N & C <> D & C <> E & C <> F & C <> J & C <> M & C <> N & D <> E & D <> F & D <> J & D <> M & D <> N & E <> F & E <> J & E <> M & E <> N & F <> J & F <> M & F <> N & J <> M & J <> N & M <> N & EqClass z,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) = EqClass u,((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) holds
EqClass u,(CompF A,G) meets EqClass z,(CompF B,G)
proof end;