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

theorem Th1: :: BVFUNC14: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 z being Element of Y
for PA, PB being a_partition of Y holds EqClass z,(PA '/\' PB) = (EqClass z,PA) /\ (EqClass z,PB)
proof end;

theorem :: BVFUNC14: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 being a_partition of Y st G = {A,B} & A <> B holds
'/\' G = A '/\' B
proof end;

Lm1: for B, C, D, b, c, d being set holds dom (((B .--> b) +* (C .--> c)) +* (D .--> d)) = {B,C,D}
proof end;

Lm2: for f being Function
for C, D, c, d being set st C <> D holds
((f +* (C .--> c)) +* (D .--> d)) . C = c
proof end;

Lm3: for B, C, D, b, c, d being set st B <> C & D <> B holds
(((B .--> b) +* (C .--> c)) +* (D .--> d)) . B = b
proof end;

Lm4: for B, C, D, b, c, d being set
for h being Function st h = ((B .--> b) +* (C .--> c)) +* (D .--> d) holds
rng h = {(h . B),(h . C),(h . D)}
proof end;

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

theorem Th4: :: BVFUNC14: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 being a_partition of Y st G = {A,B,C} & A <> B & C <> A holds
CompF A,G = B '/\' C
proof end;

theorem Th5: :: BVFUNC14: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 being a_partition of Y st G = {A,B,C} & A <> B & B <> C holds
CompF B,G = C '/\' A
proof end;

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

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

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

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

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

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

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

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

theorem :: BVFUNC14:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for B, C, D, b, c, d being set holds dom (((B .--> b) +* (C .--> c)) +* (D .--> d)) = {B,C,D} by Lm1;

theorem :: BVFUNC14:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function
for C, D, c, d being set st C <> D holds
((f +* (C .--> c)) +* (D .--> d)) . C = c by Lm2;

theorem :: BVFUNC14:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for B, C, D, b, c, d being set st B <> C & D <> B holds
(((B .--> b) +* (C .--> c)) +* (D .--> d)) . B = b by Lm3;

theorem :: BVFUNC14:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for B, C, D, b, c, d being set
for h being Function st h = ((B .--> b) +* (C .--> c)) +* (D .--> d) holds
rng h = {(h . B),(h . C),(h . D)} by Lm4;

theorem Th18: :: BVFUNC14: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 being a_partition of Y
for h being Function
for A', B', C', D' being set st G = {A,B,C,D} & A <> B & A <> C & A <> D & B <> C & B <> D & C <> D & h = (((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (A .--> A') holds
( h . B = B' & h . C = C' & h . D = D' )
proof end;

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

theorem Th20: :: BVFUNC14: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 being a_partition of Y
for h being Function
for A', B', C', D' being set st G = {A,B,C,D} & h = (((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (A .--> A') holds
rng h = {(h . A),(h . B),(h . C),(h . D)}
proof end;

theorem :: BVFUNC14:21  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 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} & A <> B & A <> C & A <> D & B <> C & B <> D & C <> D holds
EqClass u,((B '/\' C) '/\' D) meets EqClass z,A
proof end;

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

theorem :: BVFUNC14:23  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 being a_partition of Y
for z, u being Element of Y st G is independent & G = {A,B,C} & A <> B & B <> C & C <> A & EqClass z,C = EqClass u,C holds
EqClass u,(CompF A,G) meets EqClass z,(CompF B,G)
proof end;

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

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

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

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

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

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

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

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

theorem :: BVFUNC14:32  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 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} & A <> B & A <> C & A <> D & A <> E & B <> C & B <> D & B <> E & C <> D & C <> E & D <> E holds
EqClass u,(((B '/\' C) '/\' D) '/\' E) meets EqClass z,A
proof end;

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