:: 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 S₁[ 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 b₁ being Function of (Pr D),(Pr D) st
for p being PartialPredicate of D holds
( dom (b₁ . p) = dom p & ( for d being object holds
( ( d in dom p & p . d = TRUE implies (b₁ . p) . d = FALSE ) & ( d in dom p & p . d = FALSE implies (b₁ . p) . d = TRUE ) ) ) )

proof end;

uniqueness
for b₁, b₂ being Function of (Pr D),(Pr D) st ( for p being PartialPredicate of D holds
( dom (b₁ . p) = dom p & ( for d being object holds
( ( d in dom p & p . d = TRUE implies (b₁ . p) . d = FALSE ) & ( d in dom p & p . d = FALSE implies (b₁ . p) . d = TRUE ) ) ) ) ) & ( for p being PartialPredicate of D holds
( dom (b₂ . p) = dom p & ( for d being object holds
( ( d in dom p & p . d = TRUE implies (b₂ . p) . d = FALSE ) & ( d in dom p & p . d = FALSE implies (b₂ . p) . d = TRUE ) ) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines PPnegation PARTPR_1:def 2 :
for D being set
for b₂ being Function of (Pr D),(Pr D) holds
( b₂ = PPnegation D iff for p being PartialPredicate of D holds
( dom (b₂ . p) = dom p & ( for d being object holds
( ( d in dom p & p . d = TRUE implies (b₂ . p) . d = FALSE ) & ( d in dom p & p . d = FALSE implies (b₂ . 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 b₁, b₂ being PartialPredicate of D st b₁ = (PPnegation D) . b₂ holds
b₂ = (PPnegation D) . b₁

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 S₁[ object , Function] means ( $1 in dom $2 & $2 . $1 = TRUE );
defpred S₂[ object , Function, Function] means ( $1 in dom $2 & $2 . $1 = FALSE & $1 in dom $3 & $3 . $1 = FALSE );
deffunc H₁( Function, Function) -> set = { d where d is Element of D : ( S₁[d,$1] or S₁[d,$2] or S₂[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 b₁ being Function of [:(Pr D),(Pr D):],(Pr D) st
for p, q being PartialPredicate of D holds
( dom (b₁ . (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 (b₁ . (p,q)) . d = TRUE ) & ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE implies (b₁ . (p,q)) . d = FALSE ) ) ) )

proof end;

uniqueness
for b₁, b₂ being Function of [:(Pr D),(Pr D):],(Pr D) st ( for p, q being PartialPredicate of D holds
( dom (b₁ . (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 (b₁ . (p,q)) . d = TRUE ) & ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE implies (b₁ . (p,q)) . d = FALSE ) ) ) ) ) & ( for p, q being PartialPredicate of D holds
( dom (b₂ . (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 (b₂ . (p,q)) . d = TRUE ) & ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE implies (b₂ . (p,q)) . d = FALSE ) ) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines PPdisjunction PARTPR_1:def 4 :
for D being non empty set
for b₂ being Function of [:(Pr D),(Pr D):],(Pr D) holds
( b₂ = PPdisjunction D iff for p, q being PartialPredicate of D holds
( dom (b₂ . (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 (b₂ . (p,q)) . d = TRUE ) & ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE implies (b₂ . (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 b₁, p, q being PartialPredicate of D st b₁ = (PPdisjunction D) . (p,q) holds
b₁ = (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;

:: 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 b₁, p, q being PartialPredicate of D st b₁ = PP_not (PP_or ((PP_not p),(PP_not q))) holds
b₁ = 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;

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

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

:: 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 b₁ being BinOp of (Pr D) st
for p, q being PartialPredicate of D holds b₁ . (p,q) = PP_and (p,q)

proof end;

uniqueness
for b₁, b₂ being BinOp of (Pr D) st ( for p, q being PartialPredicate of D holds b₁ . (p,q) = PP_and (p,q) ) & ( for p, q being PartialPredicate of D holds b₂ . (p,q) = PP_and (p,q) ) holds
b₁ = b₂

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 b₁ being BinOp of (Pr D) st
for p, q being PartialPredicate of D holds b₁ . (p,q) = PP_or (p,q)

proof end;

uniqueness
for b₁, b₂ being BinOp of (Pr D) st ( for p, q being PartialPredicate of D holds b₁ . (p,q) = PP_or (p,q) ) & ( for p, q being PartialPredicate of D holds b₂ . (p,q) = PP_or (p,q) ) holds
b₁ = b₂

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 b₁ being UnOp of (Pr D) st
for p being PartialPredicate of D holds b₁ . p = PP_not p

proof end;

uniqueness
for b₁, b₂ being UnOp of (Pr D) st ( for p being PartialPredicate of D holds b₁ . p = PP_not p ) & ( for p being PartialPredicate of D holds b₂ . p = PP_not p ) holds
b₁ = b₂

proof end;

end;

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

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

:: deftheorem Def13 defines PartialPredConnectivesCompl PARTPR_1:def 13 :
for D being non empty set
for b₂ being UnOp of (Pr D) holds
( b₂ = PartialPredConnectivesCompl D iff for p being PartialPredicate of D holds b₂ . 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 b₁ being LattStr st
( not b₁ is empty & b₁ is constituted-Functions )

proof end;

end;

registration

cluster non empty constituted-Functions strict for OrthoLattStr ;

existence
ex b₁ being OrthoLattStr st
( b₁ is strict & not b₁ is empty & b₁ 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 b₁ being non empty constituted-Functions LattStr st b₁ is partially_Boolean holds
( b₁ is bounded & b₁ is partially_complemented & b₁ is distributive ) ;

cluster non empty distributive bounded constituted-Functions partially_complemented -> non empty constituted-Functions partially_Boolean for LattStr ;

coherence
for b₁ being non empty constituted-Functions LattStr st b₁ is bounded & b₁ is partially_complemented & b₁ is distributive holds
b₁ 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;

:: 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 b₁ being non empty meet-commutative meet-absorbing join-absorbing OrthoLattStr st b₁ is Boolean & b₁ is well-complemented holds
b₁ 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 b₁ being non empty constituted-Functions LattStr st
( b₁ is partially_Boolean & b₁ is join-idempotent & b₁ 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 b₁ being non empty OrthoLattStr st
( b₁ is Kleene & b₁ is de_Morgan & b₁ is join-idempotent & b₁ is with_idempotent_element & b₁ is Lattice-like & b₁ 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 b₁ being non empty constituted-Functions OrthoLattStr st
( b₁ is partially_Boolean & b₁ is Kleene & b₁ is de_Morgan & b₁ is join-idempotent & b₁ is with_idempotent_element & b₁ is Lattice-like & b₁ is strict )

proof end;

end;