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

theorem Th1: :: BVFUNC23: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 being a_partition of Y st G = {A,B,C,D,E,F} & A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F holds
CompF A,G = (((B '/\' C) '/\' D) '/\' E) '/\' F
proof end;

theorem Th2: :: BVFUNC23: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 being a_partition of Y st G is independent & G = {A,B,C,D,E,F} & A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F holds
CompF B,G = (((A '/\' C) '/\' D) '/\' E) '/\' F
proof end;

theorem Th3: :: BVFUNC23: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 being a_partition of Y st G is independent & G = {A,B,C,D,E,F} & A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F holds
CompF C,G = (((A '/\' B) '/\' D) '/\' E) '/\' F
proof end;

theorem Th4: :: BVFUNC23: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 being a_partition of Y st G is independent & G = {A,B,C,D,E,F} & A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F holds
CompF D,G = (((A '/\' B) '/\' C) '/\' E) '/\' F
proof end;

theorem Th5: :: BVFUNC23: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 being a_partition of Y st G is independent & G = {A,B,C,D,E,F} & A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F holds
CompF E,G = (((A '/\' B) '/\' C) '/\' D) '/\' F
proof end;

theorem :: BVFUNC23: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 being a_partition of Y st G is independent & G = {A,B,C,D,E,F} & A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F holds
CompF F,G = (((A '/\' B) '/\' C) '/\' D) '/\' E
proof end;

theorem Th7: :: BVFUNC23:7  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 being set
for h being Function
for A', B', C', D', E', F' being set st A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F & h = (((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (A .--> A') holds
( h . A = A' & h . B = B' & h . C = C' & h . D = D' & h . E = E' & h . F = F' )
proof end;

theorem Th8: :: BVFUNC23: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 being set
for h being Function
for A', B', C', D', E', F' being set st h = (((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (A .--> A') holds
dom h = {A,B,C,D,E,F}
proof end;

theorem Th9: :: BVFUNC23: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 being set
for h being Function
for A', B', C', D', E', F' being set st A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F & h = (((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (A .--> A') holds
rng h = {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F)}
proof end;

theorem :: BVFUNC23:10  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 being a_partition of Y
for z, u being Element of Y
for h being Function st G is independent & G = {A,B,C,D,E,F} & A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F holds
EqClass u,((((B '/\' C) '/\' D) '/\' E) '/\' F) meets EqClass z,A
proof end;

theorem :: BVFUNC23: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 being a_partition of Y
for z, u being Element of Y
for h being Function st G is independent & G = {A,B,C,D,E,F} & A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F & EqClass z,(((C '/\' D) '/\' E) '/\' F) = EqClass u,(((C '/\' D) '/\' E) '/\' F) holds
EqClass u,(CompF A,G) meets EqClass z,(CompF B,G)
proof end;