:: Kleene Algebra of Partial Predicates
:: by Artur Korni{\l}owicz , Ievgen Ivanov and Mykola Nikitchenko
::
:: Received March 27, 2018
:: Copyright (c) 2018-2021 Association of Mizar Users


definition
let D be set ;
func Pr D -> set equals :: PARTPR_1:def 1
PFuncs (D,BOOLEAN);
coherence
PFuncs (D,BOOLEAN) is set
;
end;

:: deftheorem defines Pr PARTPR_1:def 1 :
for D being set holds Pr D = PFuncs (D,BOOLEAN);

registration
let D be set ;
cluster Pr D -> functional non empty ;
coherence
( not Pr D is empty & Pr D is functional )
;
end;

definition
let D be set ;
mode PartialPredicate of D is PartFunc of D,BOOLEAN;
end;

theorem :: PARTPR_1:1
for x being object
for D being set st x in Pr D holds
x is PartialPredicate of D by PARTFUN1:46;

theorem :: PARTPR_1:2
for D being set
for p being PartialPredicate of D holds p in Pr D by PARTFUN1:45;

theorem Th3: :: PARTPR_1:3
for x being object
for D being set
for p being PartialPredicate of D holds
( not x in dom p or p . x = TRUE or p . x = FALSE )
proof end;

definition
let D be set ;
defpred S1[ object , Function, object ] means ( $1 in dom $2 & $2 . $1 = $3 );
func PPnegation D -> Function of (Pr D),(Pr D) means :Def2: :: PARTPR_1:def 2
for p being PartialPredicate of D holds
( dom (it . p) = dom p & ( for d being object holds
( ( d in dom p & p . d = TRUE implies (it . p) . d = FALSE ) & ( d in dom p & p . d = FALSE implies (it . p) . d = TRUE ) ) ) );
existence
ex b1 being Function of (Pr D),(Pr D) st
for p being PartialPredicate of D holds
( dom (b1 . p) = dom p & ( for d being object holds
( ( d in dom p & p . d = TRUE implies (b1 . p) . d = FALSE ) & ( d in dom p & p . d = FALSE implies (b1 . p) . d = TRUE ) ) ) )
proof end;
uniqueness
for b1, b2 being Function of (Pr D),(Pr D) st ( for p being PartialPredicate of D holds
( dom (b1 . p) = dom p & ( for d being object holds
( ( d in dom p & p . d = TRUE implies (b1 . p) . d = FALSE ) & ( d in dom p & p . d = FALSE implies (b1 . p) . d = TRUE ) ) ) ) ) & ( for p being PartialPredicate of D holds
( dom (b2 . p) = dom p & ( for d being object holds
( ( d in dom p & p . d = TRUE implies (b2 . p) . d = FALSE ) & ( d in dom p & p . d = FALSE implies (b2 . p) . d = TRUE ) ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines PPnegation PARTPR_1:def 2 :
for D being set
for b2 being Function of (Pr D),(Pr D) holds
( b2 = PPnegation D iff for p being PartialPredicate of D holds
( dom (b2 . p) = dom p & ( for d being object holds
( ( d in dom p & p . d = TRUE implies (b2 . p) . d = FALSE ) & ( d in dom p & p . d = FALSE implies (b2 . p) . d = TRUE ) ) ) ) );

definition
let D be set ;
let p be PartialPredicate of D;
func PP_not p -> PartialPredicate of D equals :: PARTPR_1:def 3
(PPnegation D) . p;
coherence
(PPnegation D) . p is PartialPredicate of D
proof end;
involutiveness
for b1, b2 being PartialPredicate of D st b1 = (PPnegation D) . b2 holds
b2 = (PPnegation D) . b1
proof end;
end;

:: deftheorem defines PP_not PARTPR_1:def 3 :
for D being set
for p being PartialPredicate of D holds PP_not p = (PPnegation D) . p;

theorem Th4: :: PARTPR_1:4
for x being object
for D being set
for p being PartialPredicate of D st x in dom p & (PP_not p) . x = FALSE holds
p . x = TRUE
proof end;

theorem Th5: :: PARTPR_1:5
for x being object
for D being set
for p being PartialPredicate of D st x in dom p & (PP_not p) . x = TRUE holds
p . x = FALSE
proof end;

theorem :: PARTPR_1:6
for x being object
for D being set
for p being PartialPredicate of D st x in dom (PP_not p) & (PP_not p) . x = FALSE holds
( x in dom p & p . x = TRUE )
proof end;

theorem :: PARTPR_1:7
for x being object
for D being set
for p being PartialPredicate of D st x in dom (PP_not p) & (PP_not p) . x = TRUE holds
( x in dom p & p . x = FALSE )
proof end;

definition
let D be non empty set ;
defpred S1[ object , Function] means ( $1 in dom $2 & $2 . $1 = TRUE );
defpred S2[ object , Function, Function] means ( $1 in dom $2 & $2 . $1 = FALSE & $1 in dom $3 & $3 . $1 = FALSE );
deffunc H1( Function, Function) -> set = { d where d is Element of D : ( S1[d,$1] or S1[d,$2] or S2[d,$1,$2] ) } ;
func PPdisjunction D -> Function of [:(Pr D),(Pr D):],(Pr D) means :Def4: :: PARTPR_1:def 4
for p, q being PartialPredicate of D holds
( dom (it . (p,q)) = { d where d is Element of D : ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE ) ) } & ( for d being object holds
( ( ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) ) implies (it . (p,q)) . d = TRUE ) & ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE implies (it . (p,q)) . d = FALSE ) ) ) );
existence
ex b1 being Function of [:(Pr D),(Pr D):],(Pr D) st
for p, q being PartialPredicate of D holds
( dom (b1 . (p,q)) = { d where d is Element of D : ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE ) ) } & ( for d being object holds
( ( ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) ) implies (b1 . (p,q)) . d = TRUE ) & ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE implies (b1 . (p,q)) . d = FALSE ) ) ) )
proof end;
uniqueness
for b1, b2 being Function of [:(Pr D),(Pr D):],(Pr D) st ( for p, q being PartialPredicate of D holds
( dom (b1 . (p,q)) = { d where d is Element of D : ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE ) ) } & ( for d being object holds
( ( ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) ) implies (b1 . (p,q)) . d = TRUE ) & ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE implies (b1 . (p,q)) . d = FALSE ) ) ) ) ) & ( for p, q being PartialPredicate of D holds
( dom (b2 . (p,q)) = { d where d is Element of D : ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE ) ) } & ( for d being object holds
( ( ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) ) implies (b2 . (p,q)) . d = TRUE ) & ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE implies (b2 . (p,q)) . d = FALSE ) ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines PPdisjunction PARTPR_1:def 4 :
for D being non empty set
for b2 being Function of [:(Pr D),(Pr D):],(Pr D) holds
( b2 = PPdisjunction D iff for p, q being PartialPredicate of D holds
( dom (b2 . (p,q)) = { d where d is Element of D : ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE ) ) } & ( for d being object holds
( ( ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) ) implies (b2 . (p,q)) . d = TRUE ) & ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE implies (b2 . (p,q)) . d = FALSE ) ) ) ) );

definition
let D be non empty set ;
let p, q be PartialPredicate of D;
func PP_or (p,q) -> PartialPredicate of D equals :: PARTPR_1:def 5
(PPdisjunction D) . (p,q);
coherence
(PPdisjunction D) . (p,q) is PartialPredicate of D
proof end;
commutativity
for b1, p, q being PartialPredicate of D st b1 = (PPdisjunction D) . (p,q) holds
b1 = (PPdisjunction D) . (q,p)
proof end;
idempotence
for p being PartialPredicate of D holds p = (PPdisjunction D) . (p,p)
proof end;
end;

:: deftheorem defines PP_or PARTPR_1:def 5 :
for D being non empty set
for p, q being PartialPredicate of D holds PP_or (p,q) = (PPdisjunction D) . (p,q);

theorem Th8: :: PARTPR_1:8
for x being object
for D being non empty set
for p, q being PartialPredicate of D holds
( not x in dom (PP_or (p,q)) or ( x in dom p & p . x = TRUE ) or ( x in dom q & q . x = TRUE ) or ( x in dom p & p . x = FALSE & x in dom q & q . x = FALSE ) )
proof end;

theorem Th9: :: PARTPR_1:9
for x being object
for D being non empty set
for p, q being PartialPredicate of D st x in dom p & x in dom q & (PP_or (p,q)) . x = TRUE & not p . x = TRUE holds
q . x = TRUE
proof end;

theorem Th10: :: PARTPR_1:10
for x being object
for D being non empty set
for p, q being PartialPredicate of D st x in dom (PP_or (p,q)) & (PP_or (p,q)) . x = TRUE & not ( x in dom p & p . x = TRUE ) holds
( x in dom q & q . x = TRUE )
proof end;

theorem Th11: :: PARTPR_1:11
for x being object
for D being non empty set
for p, q being PartialPredicate of D st x in dom p & (PP_or (p,q)) . x = FALSE holds
p . x = FALSE
proof end;

theorem Th12: :: PARTPR_1:12
for x being object
for D being non empty set
for p, q being PartialPredicate of D st x in dom q & (PP_or (p,q)) . x = FALSE holds
q . x = FALSE
proof end;

theorem Th13: :: PARTPR_1:13
for x being object
for D being non empty set
for p, q being PartialPredicate of D st x in dom (PP_or (p,q)) & (PP_or (p,q)) . x = FALSE holds
( x in dom p & p . x = FALSE & x in dom q & q . x = FALSE )
proof end;

:: WP: Associativity law
theorem Th14: :: PARTPR_1:14
for D being non empty set
for p, q, r being PartialPredicate of D holds PP_or (p,(PP_or (q,r))) = PP_or ((PP_or (p,q)),r)
proof end;

theorem Th15: :: PARTPR_1:15
for D being non empty set
for p, q, r being PartialPredicate of D holds PP_or ((PP_or (p,q)),(PP_or (p,r))) = PP_or ((PP_or (p,q)),r)
proof end;

definition
let D be non empty set ;
let p, q be PartialPredicate of D;
func PP_and (p,q) -> PartialPredicate of D equals :: PARTPR_1:def 6
PP_not (PP_or ((PP_not p),(PP_not q)));
coherence
PP_not (PP_or ((PP_not p),(PP_not q))) is PartialPredicate of D
;
commutativity
for b1, p, q being PartialPredicate of D st b1 = PP_not (PP_or ((PP_not p),(PP_not q))) holds
b1 = PP_not (PP_or ((PP_not q),(PP_not p)))
;
idempotence
for p being PartialPredicate of D holds p = PP_not (PP_or ((PP_not p),(PP_not p)))
;
func PP_imp (p,q) -> PartialPredicate of D equals :: PARTPR_1:def 7
PP_or ((PP_not p),q);
coherence
PP_or ((PP_not p),q) is PartialPredicate of D
;
end;

:: deftheorem defines PP_and PARTPR_1:def 6 :
for D being non empty set
for p, q being PartialPredicate of D holds PP_and (p,q) = PP_not (PP_or ((PP_not p),(PP_not q)));

:: deftheorem defines PP_imp PARTPR_1:def 7 :
for D being non empty set
for p, q being PartialPredicate of D holds PP_imp (p,q) = PP_or ((PP_not p),q);

theorem Th16: :: PARTPR_1:16
for D being non empty set
for p, q being PartialPredicate of D holds dom (PP_and (p,q)) = { d where d is Element of D : ( ( d in dom p & p . d = FALSE ) or ( d in dom q & q . d = FALSE ) or ( d in dom p & p . d = TRUE & d in dom q & q . d = TRUE ) ) }
proof end;

theorem Th17: :: PARTPR_1:17
for x being object
for D being non empty set
for p, q being PartialPredicate of D holds
( not x in dom (PP_and (p,q)) or ( x in dom p & p . x = FALSE ) or ( x in dom q & q . x = FALSE ) or ( x in dom p & p . x = TRUE & x in dom q & q . x = TRUE ) )
proof end;

theorem Th18: :: PARTPR_1:18
for x being object
for D being non empty set
for p, q being PartialPredicate of D st x in dom p & p . x = TRUE & x in dom q & q . x = TRUE holds
(PP_and (p,q)) . x = TRUE
proof end;

theorem Th19: :: PARTPR_1:19
for x being object
for D being non empty set
for p, q being PartialPredicate of D st x in dom p & p . x = FALSE holds
(PP_and (p,q)) . x = FALSE
proof end;

theorem :: PARTPR_1:20
for x being object
for D being non empty set
for p, q being PartialPredicate of D st x in dom q & q . x = FALSE holds
(PP_and (p,q)) . x = FALSE by Th19;

theorem :: PARTPR_1:21
for x being object
for D being non empty set
for p, q being PartialPredicate of D st x in dom p & (PP_and (p,q)) . x = TRUE holds
p . x = TRUE by Th3, Th19;

theorem :: PARTPR_1:22
for x being object
for D being non empty set
for p, q being PartialPredicate of D st x in dom q & (PP_and (p,q)) . x = TRUE holds
q . x = TRUE by Th3, Th19;

theorem Th23: :: PARTPR_1:23
for x being object
for D being non empty set
for p, q being PartialPredicate of D st x in dom (PP_and (p,q)) & (PP_and (p,q)) . x = TRUE holds
( x in dom p & p . x = TRUE & x in dom q & q . x = TRUE )
proof end;

theorem Th24: :: PARTPR_1:24
for x being object
for D being non empty set
for p, q being PartialPredicate of D st x in dom p & x in dom q & (PP_and (p,q)) . x = FALSE & not p . x = FALSE holds
q . x = FALSE
proof end;

theorem Th25: :: PARTPR_1:25
for x being object
for D being non empty set
for p, q being PartialPredicate of D st x in dom (PP_and (p,q)) & (PP_and (p,q)) . x = FALSE & not ( x in dom p & p . x = FALSE ) holds
( x in dom q & q . x = FALSE )
proof end;

:: WP: Associativity law
theorem :: PARTPR_1:26
for D being non empty set
for p, q, r being PartialPredicate of D holds PP_and (p,(PP_and (q,r))) = PP_and ((PP_and (p,q)),r) by Th14;

theorem :: PARTPR_1:27
for D being non empty set
for p, q, r being PartialPredicate of D holds PP_and ((PP_and (p,q)),(PP_and (p,r))) = PP_and ((PP_and (p,q)),r) by Th15;

:: WP: Meet-absorbing law
theorem Th28: :: PARTPR_1:28
for D being non empty set
for p, q being PartialPredicate of D holds PP_or ((PP_and (p,q)),q) = q
proof end;

:: WP: Join-absorbing law
theorem Th29: :: PARTPR_1:29
for D being non empty set
for p, q being PartialPredicate of D holds PP_and (p,(PP_or (p,q))) = p
proof end;

:: WP: Distributivity law
theorem Th30: :: PARTPR_1:30
for D being non empty set
for p, q, r being PartialPredicate of D holds PP_and (p,(PP_or (q,r))) = PP_or ((PP_and (p,q)),(PP_and (p,r)))
proof end;

theorem Th31: :: PARTPR_1:31
for D being non empty set
for p, q being PartialPredicate of D holds dom (PP_imp (p,q)) = { d where d is Element of D : ( ( d in dom p & p . d = FALSE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = TRUE & d in dom q & q . d = FALSE ) ) }
proof end;

theorem Th32: :: PARTPR_1:32
for x being object
for D being non empty set
for p, q being PartialPredicate of D holds
( not x in dom (PP_imp (p,q)) or ( x in dom p & p . x = FALSE ) or ( x in dom q & q . x = TRUE ) or ( x in dom p & p . x = TRUE & x in dom q & q . x = FALSE ) )
proof end;

theorem Th33: :: PARTPR_1:33
for x being object
for D being non empty set
for p, q being PartialPredicate of D st x in dom p & p . x = FALSE holds
(PP_imp (p,q)) . x = TRUE
proof end;

theorem Th34: :: PARTPR_1:34
for x being object
for D being non empty set
for p, q being PartialPredicate of D st x in dom q & q . x = TRUE holds
(PP_imp (p,q)) . x = TRUE by Def4;

theorem Th35: :: PARTPR_1:35
for x being object
for D being non empty set
for p, q being PartialPredicate of D st x in dom p & p . x = TRUE & x in dom q & q . x = FALSE holds
(PP_imp (p,q)) . x = FALSE
proof end;

theorem :: PARTPR_1:36
for x being object
for D being non empty set
for p, q being PartialPredicate of D st x in dom p & x in dom q & (PP_imp (p,q)) . x = TRUE & not p . x = FALSE holds
q . x = TRUE
proof end;

theorem :: PARTPR_1:37
for x being object
for D being non empty set
for p, q being PartialPredicate of D st x in dom p & (PP_imp (p,q)) . x = FALSE holds
p . x = TRUE by Th3, Th33;

theorem :: PARTPR_1:38
for x being object
for D being non empty set
for p, q being PartialPredicate of D st x in dom q & (PP_imp (p,q)) . x = FALSE holds
q . x = FALSE by Th3, Th34;

theorem :: PARTPR_1:39
for x being object
for D being non empty set
for p, q being PartialPredicate of D st x in dom (PP_imp (p,q)) & (PP_imp (p,q)) . x = FALSE holds
( x in dom p & p . x = TRUE & x in dom q & q . x = FALSE )
proof end;

theorem :: PARTPR_1:40
for x being object
for D being non empty set
for p, q being PartialPredicate of D st x in dom (PP_imp (p,q)) & (PP_imp (p,q)) . x = TRUE & not ( x in dom p & p . x = FALSE ) holds
( x in dom q & q . x = TRUE )
proof end;

theorem :: PARTPR_1:41
for D being non empty set
for p, q, r being PartialPredicate of D holds PP_and ((PP_imp (p,r)),(PP_imp (q,r))) = PP_imp ((PP_or (p,q)),r)
proof end;

theorem :: PARTPR_1:42
for D being non empty set
for p, q, r being PartialPredicate of D holds PP_or ((PP_imp (p,r)),(PP_imp (q,r))) = PP_imp ((PP_and (p,q)),r)
proof end;

:: WP: True constant predicate
definition
let D be set ;
func PP_True D -> PartialPredicate of D equals :: PARTPR_1:def 8
D --> TRUE;
coherence
D --> TRUE is PartialPredicate of D
proof end;
end;

:: deftheorem defines PP_True PARTPR_1:def 8 :
for D being set holds PP_True D = D --> TRUE;

:: WP: False constant predicate
definition
let D be set ;
func PP_False D -> PartialPredicate of D equals :: PARTPR_1:def 9
D --> FALSE;
coherence
D --> FALSE is PartialPredicate of D
proof end;
end;

:: deftheorem defines PP_False PARTPR_1:def 9 :
for D being set holds PP_False D = D --> FALSE;

theorem Th43: :: PARTPR_1:43
for D being set holds PP_not (PP_False D) = PP_True D
proof end;

theorem :: PARTPR_1:44
for D being set holds PP_not (PP_True D) = PP_False D
proof end;

theorem Th45: :: PARTPR_1:45
for D being non empty set
for p being PartialPredicate of D holds PP_or (p,(PP_True D)) = PP_True D
proof end;

theorem :: PARTPR_1:46
for D being non empty set
for p being PartialPredicate of D holds PP_or ((PP_True D),p) = PP_True D by Th45;

theorem Th47: :: PARTPR_1:47
for D being non empty set
for p being PartialPredicate of D holds PP_and (p,(PP_False D)) = PP_False D
proof end;

theorem :: PARTPR_1:48
for D being non empty set
for p being PartialPredicate of D holds PP_and ((PP_False D),p) = PP_False D by Th47;

theorem Th49: :: PARTPR_1:49
for D being non empty set
for p being PartialPredicate of D holds PP_or (p,(PP_not p)) = (PP_True D) | (dom p)
proof end;

theorem :: PARTPR_1:50
for D being non empty set
for p being PartialPredicate of D holds PP_or ((PP_not p),p) = (PP_True D) | (dom p) by Th49;

theorem Th51: :: PARTPR_1:51
for D being non empty set
for p being PartialPredicate of D holds PP_and (p,(PP_not p)) = (PP_False D) | (dom p)
proof end;

theorem :: PARTPR_1:52
for D being non empty set
for p being PartialPredicate of D holds PP_and ((PP_not p),p) = (PP_False D) | (dom p) by Th51;

theorem :: PARTPR_1:53
for D being non empty set
for p being PartialPredicate of D holds PP_imp ((PP_False D),p) = PP_True D
proof end;

theorem :: PARTPR_1:54
for D being non empty set
for p being PartialPredicate of D holds PP_imp (p,(PP_True D)) = PP_True D by Th45;

theorem Th55: :: PARTPR_1:55
for D being non empty set
for p, q being PartialPredicate of D holds PP_or (((PP_False D) | (dom p)),((PP_True D) | (dom q))) = (PP_True D) | (dom q)
proof end;

:: WP: Empty predicate
definition
let D be set ;
func PP_BottomPred D -> PartialPredicate of D equals :: PARTPR_1:def 10
{} ;
coherence
{} is PartialPredicate of D
by RELSET_1:12;
end;

:: deftheorem defines PP_BottomPred PARTPR_1:def 10 :
for D being set holds PP_BottomPred D = {} ;

theorem Th56: :: PARTPR_1:56
for D being set holds PP_not (PP_BottomPred D) = PP_BottomPred D
proof end;

theorem Th57: :: PARTPR_1:57
for D being non empty set holds PP_or ((PP_BottomPred D),(PP_True D)) = PP_True D
proof end;

theorem :: PARTPR_1:58
for D being non empty set holds PP_and ((PP_BottomPred D),(PP_False D)) = PP_False D
proof end;

theorem :: PARTPR_1:59
for D being non empty set holds PP_imp ((PP_BottomPred D),(PP_True D)) = PP_True D
proof end;

definition
let D be non empty set ;
func PartialPredConnectivesMeet D -> BinOp of (Pr D) means :Def11: :: PARTPR_1:def 11
for p, q being PartialPredicate of D holds it . (p,q) = PP_and (p,q);
existence
ex b1 being BinOp of (Pr D) st
for p, q being PartialPredicate of D holds b1 . (p,q) = PP_and (p,q)
proof end;
uniqueness
for b1, b2 being BinOp of (Pr D) st ( for p, q being PartialPredicate of D holds b1 . (p,q) = PP_and (p,q) ) & ( for p, q being PartialPredicate of D holds b2 . (p,q) = PP_and (p,q) ) holds
b1 = b2
proof end;
func PartialPredConnectivesJoin D -> BinOp of (Pr D) means :Def12: :: PARTPR_1:def 12
for p, q being PartialPredicate of D holds it . (p,q) = PP_or (p,q);
existence
ex b1 being BinOp of (Pr D) st
for p, q being PartialPredicate of D holds b1 . (p,q) = PP_or (p,q)
proof end;
uniqueness
for b1, b2 being BinOp of (Pr D) st ( for p, q being PartialPredicate of D holds b1 . (p,q) = PP_or (p,q) ) & ( for p, q being PartialPredicate of D holds b2 . (p,q) = PP_or (p,q) ) holds
b1 = b2
proof end;
func PartialPredConnectivesCompl D -> UnOp of (Pr D) means :Def13: :: PARTPR_1:def 13
for p being PartialPredicate of D holds it . p = PP_not p;
existence
ex b1 being UnOp of (Pr D) st
for p being PartialPredicate of D holds b1 . p = PP_not p
proof end;
uniqueness
for b1, b2 being UnOp of (Pr D) st ( for p being PartialPredicate of D holds b1 . p = PP_not p ) & ( for p being PartialPredicate of D holds b2 . p = PP_not p ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines PartialPredConnectivesMeet PARTPR_1:def 11 :
for D being non empty set
for b2 being BinOp of (Pr D) holds
( b2 = PartialPredConnectivesMeet D iff for p, q being PartialPredicate of D holds b2 . (p,q) = PP_and (p,q) );

:: deftheorem Def12 defines PartialPredConnectivesJoin PARTPR_1:def 12 :
for D being non empty set
for b2 being BinOp of (Pr D) holds
( b2 = PartialPredConnectivesJoin D iff for p, q being PartialPredicate of D holds b2 . (p,q) = PP_or (p,q) );

:: deftheorem Def13 defines PartialPredConnectivesCompl PARTPR_1:def 13 :
for D being non empty set
for b2 being UnOp of (Pr D) holds
( b2 = PartialPredConnectivesCompl D iff for p being PartialPredicate of D holds b2 . p = PP_not p );

definition
let D be non empty set ;
func PartialPredConnectivesLatt D -> strict OrthoLattStr equals :: PARTPR_1:def 14
OrthoLattStr(# (Pr D),(PartialPredConnectivesJoin D),(PartialPredConnectivesMeet D),(PartialPredConnectivesCompl D) #);
coherence
OrthoLattStr(# (Pr D),(PartialPredConnectivesJoin D),(PartialPredConnectivesMeet D),(PartialPredConnectivesCompl D) #) is strict OrthoLattStr
;
end;

:: deftheorem defines PartialPredConnectivesLatt PARTPR_1:def 14 :
for D being non empty set holds PartialPredConnectivesLatt D = OrthoLattStr(# (Pr D),(PartialPredConnectivesJoin D),(PartialPredConnectivesMeet D),(PartialPredConnectivesCompl D) #);

registration
let D be non empty set ;
let f, g be BinOp of D;
let h be UnOp of D;
cluster OrthoLattStr(# D,f,g,h #) -> non empty ;
coherence
not OrthoLattStr(# D,f,g,h #) is empty
proof end;
end;

registration
let D be non empty set ;
cluster PartialPredConnectivesLatt D -> non empty constituted-Functions strict ;
coherence
( not PartialPredConnectivesLatt D is empty & PartialPredConnectivesLatt D is constituted-Functions )
;
end;

registration
cluster non empty constituted-Functions for LattStr ;
existence
ex b1 being LattStr st
( not b1 is empty & b1 is constituted-Functions )
proof end;
end;

registration
cluster non empty constituted-Functions strict for OrthoLattStr ;
existence
ex b1 being OrthoLattStr st
( b1 is strict & not b1 is empty & b1 is constituted-Functions )
proof end;
end;

registration
let D be non empty set ;
cluster PartialPredConnectivesLatt D -> Lattice-like strict ;
coherence
PartialPredConnectivesLatt D is Lattice-like
proof end;
cluster PartialPredConnectivesLatt D -> bounded strict ;
coherence
PartialPredConnectivesLatt D is bounded
proof end;
cluster PartialPredConnectivesLatt D -> strict join-idempotent with_idempotent_element de_Morgan ;
coherence
( PartialPredConnectivesLatt D is de_Morgan & PartialPredConnectivesLatt D is join-idempotent & PartialPredConnectivesLatt D is with_idempotent_element )
proof end;
end;

theorem Th60: :: PARTPR_1:60
for D being non empty set holds Top (PartialPredConnectivesLatt D) = PP_True D
proof end;

theorem Th61: :: PARTPR_1:61
for D being non empty set holds Bottom (PartialPredConnectivesLatt D) = PP_False D
proof end;

definition
let L be non empty constituted-Functions LattStr ;
let a, b be Element of L;
pred a is_a_partial_complement_of b means :: PARTPR_1:def 15
( a "\/" b = (Top L) | (dom b) & b "\/" a = (Top L) | (dom b) & a "/\" b = (Bottom L) | (dom b) & b "/\" a = (Bottom L) | (dom b) );
end;

:: deftheorem defines is_a_partial_complement_of PARTPR_1:def 15 :
for L being non empty constituted-Functions LattStr
for a, b being Element of L holds
( a is_a_partial_complement_of b iff ( a "\/" b = (Top L) | (dom b) & b "\/" a = (Top L) | (dom b) & a "/\" b = (Bottom L) | (dom b) & b "/\" a = (Bottom L) | (dom b) ) );

definition
let L be non empty constituted-Functions LattStr ;
attr L is partially_complemented means :: PARTPR_1:def 16
for b being Element of L ex a being Element of L st a is_a_partial_complement_of b;
end;

:: deftheorem defines partially_complemented PARTPR_1:def 16 :
for L being non empty constituted-Functions LattStr holds
( L is partially_complemented iff for b being Element of L ex a being Element of L st a is_a_partial_complement_of b );

definition
let IT be non empty constituted-Functions LattStr ;
attr IT is partially_Boolean means :: PARTPR_1:def 17
( IT is bounded & IT is partially_complemented & IT is distributive );
end;

:: deftheorem defines partially_Boolean PARTPR_1:def 17 :
for IT being non empty constituted-Functions LattStr holds
( IT is partially_Boolean iff ( IT is bounded & IT is partially_complemented & IT is distributive ) );

registration
cluster non empty constituted-Functions partially_Boolean -> non empty distributive bounded constituted-Functions partially_complemented for LattStr ;
coherence
for b1 being non empty constituted-Functions LattStr st b1 is partially_Boolean holds
( b1 is bounded & b1 is partially_complemented & b1 is distributive )
;
cluster non empty distributive bounded constituted-Functions partially_complemented -> non empty constituted-Functions partially_Boolean for LattStr ;
coherence
for b1 being non empty constituted-Functions LattStr st b1 is bounded & b1 is partially_complemented & b1 is distributive holds
b1 is partially_Boolean
;
end;

theorem Th62: :: PARTPR_1:62
for D being non empty set
for p being PartialPredicate of D
for a, b being Element of (PartialPredConnectivesLatt D) st a = p & b = PP_not p holds
b is_a_partial_complement_of a
proof end;

registration
let D be non empty set ;
cluster PartialPredConnectivesLatt D -> strict partially_Boolean ;
coherence
PartialPredConnectivesLatt D is partially_Boolean
proof end;
end;

:: WP: Distributivity law
theorem :: PARTPR_1:63
for D being non empty set
for p, q, r being PartialPredicate of D holds PP_or (p,(PP_and (q,r))) = PP_and ((PP_or (p,q)),(PP_or (p,r)))
proof end;

definition
let L be non empty OrthoLattStr ;
attr L is Kleene means :: PARTPR_1:def 18
for x, y being Element of L holds x "/\" (x `) [= y "\/" (y `);
end;

:: deftheorem defines Kleene PARTPR_1:def 18 :
for L being non empty OrthoLattStr holds
( L is Kleene iff for x, y being Element of L holds x "/\" (x `) [= y "\/" (y `) );

registration
cluster non empty meet-commutative meet-absorbing join-absorbing Boolean well-complemented -> non empty meet-commutative meet-absorbing join-absorbing Kleene for OrthoLattStr ;
coherence
for b1 being non empty meet-commutative meet-absorbing join-absorbing OrthoLattStr st b1 is Boolean & b1 is well-complemented holds
b1 is Kleene
proof end;
end;

registration
let D be non empty set ;
cluster PartialPredConnectivesLatt D -> strict Kleene ;
coherence
PartialPredConnectivesLatt D is Kleene
proof end;
end;

registration
cluster non empty Lattice-like constituted-Functions join-idempotent partially_Boolean for LattStr ;
existence
ex b1 being non empty constituted-Functions LattStr st
( b1 is partially_Boolean & b1 is join-idempotent & b1 is Lattice-like )
proof end;
end;

registration
cluster non empty Lattice-like strict join-idempotent with_idempotent_element de_Morgan Kleene for OrthoLattStr ;
existence
ex b1 being non empty OrthoLattStr st
( b1 is Kleene & b1 is de_Morgan & b1 is join-idempotent & b1 is with_idempotent_element & b1 is Lattice-like & b1 is strict )
proof end;
end;

registration
cluster non empty Lattice-like constituted-Functions strict join-idempotent with_idempotent_element de_Morgan partially_Boolean Kleene for OrthoLattStr ;
existence
ex b1 being non empty constituted-Functions OrthoLattStr st
( b1 is partially_Boolean & b1 is Kleene & b1 is de_Morgan & b1 is join-idempotent & b1 is with_idempotent_element & b1 is Lattice-like & b1 is strict )
proof end;
end;