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

definition
let I be set ;
let A be ManySortedSet of I;
func bool A -> ManySortedSet of I means :Def1: :: MBOOLEAN:def 1
for i being set st i in I holds
it . i = bool (A . i);
existence
ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i = bool (A . i)
proof end;
uniqueness
for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = bool (A . i) ) & ( for i being set st i in I holds
b2 . i = bool (A . i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines bool MBOOLEAN:def 1 :
for I being set
for A, b3 being ManySortedSet of I holds
( b3 = bool A iff for i being set st i in I holds
b3 . i = bool (A . i) );

registration
let I be set ;
let A be ManySortedSet of I;
cluster bool A -> V3 ;
coherence
bool A is non-empty
proof end;
end;

Lm1: for i, I, X being set
for M being ManySortedSet of I st i in I holds
dom (M +* (i .--> X)) = I
proof end;

Lm2: for I being set
for A, B being ManySortedSet of I
for i being set st i in I holds
(bool (A \/ B)) . i = bool ((A . i) \/ (B . i))
proof end;

Lm3: for I being set
for A, B being ManySortedSet of I
for i being set st i in I holds
(bool (A /\ B)) . i = bool ((A . i) /\ (B . i))
proof end;

Lm4: for I being set
for A, B being ManySortedSet of I
for i being set st i in I holds
(bool (A \ B)) . i = bool ((A . i) \ (B . i))
proof end;

Lm5: for I being set
for A, B being ManySortedSet of I
for i being set st i in I holds
(bool (A \+\ B)) . i = bool ((A . i) \+\ (B . i))
proof end;

theorem Th1: :: MBOOLEAN:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I holds
( X = bool Y iff for A being ManySortedSet of I holds
( A in X iff A c= Y ) )
proof end;

theorem :: MBOOLEAN:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set holds bool ([0] I) = I --> {{} }
proof end;

theorem :: MBOOLEAN:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, x being set holds bool (I --> x) = I --> (bool x)
proof end;

theorem :: MBOOLEAN:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, x being set holds bool (I --> {x}) = I --> {{} ,{x}}
proof end;

theorem :: MBOOLEAN:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A being ManySortedSet of I holds [0] I c= A
proof end;

theorem :: MBOOLEAN:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A, B being ManySortedSet of I st A c= B holds
bool A c= bool B
proof end;

theorem :: MBOOLEAN:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A, B being ManySortedSet of I holds (bool A) \/ (bool B) c= bool (A \/ B)
proof end;

theorem :: MBOOLEAN:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A, B being ManySortedSet of I st (bool A) \/ (bool B) = bool (A \/ B) holds
for i being set st i in I holds
A . i,B . i are_c=-comparable
proof end;

theorem :: MBOOLEAN:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A, B being ManySortedSet of I holds bool (A /\ B) = (bool A) /\ (bool B)
proof end;

theorem :: MBOOLEAN:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A, B being ManySortedSet of I holds bool (A \ B) c= (I --> {{} }) \/ ((bool A) \ (bool B))
proof end;

theorem :: MBOOLEAN:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, A, B being ManySortedSet of I holds
( X c= A \ B iff ( X c= A & X misses B ) )
proof end;

theorem :: MBOOLEAN:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A, B being ManySortedSet of I holds (bool (A \ B)) \/ (bool (B \ A)) c= bool (A \+\ B)
proof end;

theorem :: MBOOLEAN:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, A, B being ManySortedSet of I holds
( X c= A \+\ B iff ( X c= A \/ B & X misses A /\ B ) )
proof end;

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

theorem :: MBOOLEAN:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, A, Y being ManySortedSet of I st ( X c= A or Y c= A ) holds
X /\ Y c= A
proof end;

theorem :: MBOOLEAN:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, A, Y being ManySortedSet of I st X c= A holds
X \ Y c= A
proof end;

theorem :: MBOOLEAN:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, A, Y being ManySortedSet of I st X c= A & Y c= A holds
X \+\ Y c= A
proof end;

theorem :: MBOOLEAN:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, Y being ManySortedSet of I holds [|X,Y|] c= bool (bool (X \/ Y))
proof end;

theorem :: MBOOLEAN:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, A being ManySortedSet of I holds
( X c= A iff X in bool A )
proof end;

theorem :: MBOOLEAN:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A, B being ManySortedSet of I holds MSFuncs A,B c= bool [|A,B|]
proof end;

definition
let I be set ;
let A be ManySortedSet of I;
func union A -> ManySortedSet of I means :Def2: :: MBOOLEAN:def 2
for i being set st i in I holds
it . i = union (A . i);
existence
ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i = union (A . i)
proof end;
uniqueness
for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = union (A . i) ) & ( for i being set st i in I holds
b2 . i = union (A . i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines union MBOOLEAN:def 2 :
for I being set
for A, b3 being ManySortedSet of I holds
( b3 = union A iff for i being set st i in I holds
b3 . i = union (A . i) );

registration
let I be set ;
cluster union ([0] I) -> V4 ;
coherence
union ([0] I) is empty-yielding
proof end;
end;

Lm6: for I being set
for A, B being ManySortedSet of I
for i being set st i in I holds
(union (A \/ B)) . i = union ((A . i) \/ (B . i))
proof end;

Lm7: for I being set
for A, B being ManySortedSet of I
for i being set st i in I holds
(union (A /\ B)) . i = union ((A . i) /\ (B . i))
proof end;

theorem :: MBOOLEAN:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A, X being ManySortedSet of I holds
( A in union X iff ex Y being ManySortedSet of I st
( A in Y & Y in X ) )
proof end;

theorem :: MBOOLEAN:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set holds union ([0] I) = [0] I
proof end;

theorem :: MBOOLEAN:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, x being set holds union (I --> x) = I --> (union x)
proof end;

theorem :: MBOOLEAN:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, x being set holds union (I --> {x}) = I --> x
proof end;

theorem :: MBOOLEAN:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, x, y being set holds union (I --> {{x},{y}}) = I --> {x,y}
proof end;

theorem :: MBOOLEAN:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for X, A being ManySortedSet of I st X in A holds
X c= union A
proof end;

theorem :: MBOOLEAN:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A, B being ManySortedSet of I st A c= B holds
union A c= union B
proof end;

theorem :: MBOOLEAN:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A, B being ManySortedSet of I holds union (A \/ B) = (union A) \/ (union B)
proof end;

theorem :: MBOOLEAN:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A, B being ManySortedSet of I holds union (A /\ B) c= (union A) /\ (union B)
proof end;

theorem :: MBOOLEAN:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A being ManySortedSet of I holds union (bool A) = A
proof end;

theorem :: MBOOLEAN:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A being ManySortedSet of I holds A c= bool (union A)
proof end;

theorem :: MBOOLEAN:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for Y, A, X being ManySortedSet of I st union Y c= A & X in Y holds
X c= A
proof end;

theorem :: MBOOLEAN:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for Z being ManySortedSet of I
for A being V3 ManySortedSet of I st ( for X being ManySortedSet of I st X in A holds
X c= Z ) holds
union A c= Z
proof end;

theorem :: MBOOLEAN:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for B being ManySortedSet of I
for A being V3 ManySortedSet of I st ( for X being ManySortedSet of I st X in A holds
X /\ B = [0] I ) holds
(union A) /\ B = [0] I
proof end;

theorem :: MBOOLEAN:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A, B being ManySortedSet of I st A \/ B is non-empty & ( for X, Y being ManySortedSet of I st X <> Y & X in A \/ B & Y in A \/ B holds
X /\ Y = [0] I ) holds
union (A /\ B) = (union A) /\ (union B)
proof end;

theorem :: MBOOLEAN:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A, X being ManySortedSet of I
for B being V3 ManySortedSet of I st X c= union (A \/ B) & ( for Y being ManySortedSet of I st Y in B holds
Y /\ X = [0] I ) holds
X c= union A
proof end;

theorem :: MBOOLEAN:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A being V3 locally-finite ManySortedSet of I st ( for X, Y being ManySortedSet of I st X in A & Y in A & not X c= Y holds
Y c= X ) holds
union A in A
proof end;