:: Kleene Algebra of Partial Predicates
:: by Artur Korni{\l}owicz , Ievgen Ivanov and Mykola Nikitchenko
::
:: Copyright (c) 2018 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
( 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 () . p; coherence () . p is PartialPredicate of D proof end; involutiveness for b1, b2 being PartialPredicate of D st b1 = () . b2 holds b2 = () . 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 = () . 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 & () . 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 & () . 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 () & () . 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 () & () . 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
() . (p,q);
coherence
() . (p,q) is PartialPredicate of D
proof end;
commutativity
for b1, p, q being PartialPredicate of D st b1 = () . (p,q) holds
b1 = () . (q,p)
proof end;
idempotence
for p being PartialPredicate of D holds p = () . (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) = () . (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;

:: 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 ((),()));
coherence
PP_not (PP_or ((),())) is PartialPredicate of D
;
commutativity
for b1, p, q being PartialPredicate of D st b1 = PP_not (PP_or ((),())) holds
b1 = PP_not (PP_or ((),()))
;
idempotence
for p being PartialPredicate of D holds p = PP_not (PP_or ((),()))
;
func PP_imp (p,q) -> PartialPredicate of D equals :: PARTPR_1:def 7
PP_or ((),q);
coherence
PP_or ((),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 ((),()));

:: 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 ((),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 ;

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 ;

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;

:: 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;

:: 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;

:: 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;

:: 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 ;

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 ;

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;

:: 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;

:: 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_True D
proof end;

theorem :: PARTPR_1:44
for D being set holds PP_not () = 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
proof end;

theorem :: PARTPR_1:46
for D being non empty set
for p being PartialPredicate of D holds PP_or ((),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
proof end;

theorem :: PARTPR_1:48
for D being non empty set
for p being PartialPredicate of D holds PP_and ((),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,()) = () | (dom p)
proof end;

theorem :: PARTPR_1:50
for D being non empty set
for p being PartialPredicate of D holds PP_or ((),p) = () | (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,()) = () | (dom p)
proof end;

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

theorem :: PARTPR_1:53
for D being non empty set
for p being PartialPredicate of D holds PP_imp ((),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 by Th45;

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

:: Empty predicate
definition
let D be set ;
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
proof end;

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

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

theorem :: PARTPR_1:59
for D being non empty set holds PP_imp ((),()) = 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 ;
coherence ;
end;

:: deftheorem defines PartialPredConnectivesLatt PARTPR_1:def 14 :
for D being non empty set holds PartialPredConnectivesLatt D = OrthoLattStr(# (Pr 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 ;
coherence ;
end;

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

registration
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 ;
coherence
proof end;
coherence
proof end;
coherence
proof end;
end;

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

theorem Th61: :: PARTPR_1:61
for D being non empty set holds Bottom = 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 = () | (dom b) & b "/\" a = () | (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 = () | (dom b) & b "/\" a = () | (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
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 )
;
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 st a = p & b = PP_not p holds
b is_a_partial_complement_of a
proof end;

registration
let D be non empty set ;
coherence
proof end;
end;

:: 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
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 ;
coherence
proof end;
end;

registration
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
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
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;