:: by Artur Korni{\l}owicz , Ievgen Ivanov and Mykola Nikitchenko

::

:: Received March 27, 2018

:: Copyright (c) 2018-2019 Association of Mizar Users

theorem :: PARTPR_1:1

theorem :: PARTPR_1:2

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 )

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_{1}[ object , Function, object ] means ( $1 in dom $2 & $2 . $1 = $3 );

ex b_{1} being Function of (Pr D),(Pr D) st

for p being PartialPredicate of D holds

( dom (b_{1} . p) = dom p & ( for d being object holds

( ( d in dom p & p . d = TRUE implies (b_{1} . p) . d = FALSE ) & ( d in dom p & p . d = FALSE implies (b_{1} . p) . d = TRUE ) ) ) )

for b_{1}, b_{2} being Function of (Pr D),(Pr D) st ( for p being PartialPredicate of D holds

( dom (b_{1} . p) = dom p & ( for d being object holds

( ( d in dom p & p . d = TRUE implies (b_{1} . p) . d = FALSE ) & ( d in dom p & p . d = FALSE implies (b_{1} . p) . d = TRUE ) ) ) ) ) & ( for p being PartialPredicate of D holds

( dom (b_{2} . p) = dom p & ( for d being object holds

( ( d in dom p & p . d = TRUE implies (b_{2} . p) . d = FALSE ) & ( d in dom p & p . d = FALSE implies (b_{2} . p) . d = TRUE ) ) ) ) ) holds

b_{1} = b_{2}

end;
defpred S

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

ex b

for p being PartialPredicate of D holds

( dom (b

( ( d in dom p & p . d = TRUE implies (b

proof end;

uniqueness for b

( dom (b

( ( d in dom p & p . d = TRUE implies (b

( dom (b

( ( d in dom p & p . d = TRUE implies (b

b

proof end;

:: deftheorem Def2 defines PPnegation PARTPR_1:def 2 :

for D being set

for b_{2} being Function of (Pr D),(Pr D) holds

( b_{2} = PPnegation D iff for p being PartialPredicate of D holds

( dom (b_{2} . p) = dom p & ( for d being object holds

( ( d in dom p & p . d = TRUE implies (b_{2} . p) . d = FALSE ) & ( d in dom p & p . d = FALSE implies (b_{2} . p) . d = TRUE ) ) ) ) );

for D being set

for b

( b

( dom (b

( ( d in dom p & p . d = TRUE implies (b

definition

let D be set ;

let p be PartialPredicate of D;

coherence

(PPnegation D) . p is PartialPredicate of D

for b_{1}, b_{2} being PartialPredicate of D st b_{1} = (PPnegation D) . b_{2} holds

b_{2} = (PPnegation D) . b_{1}

end;
let p be PartialPredicate of D;

coherence

(PPnegation D) . p is PartialPredicate of D

proof end;

involutiveness for b

b

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

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

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

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 )

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 )

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_{1}[ object , Function] means ( $1 in dom $2 & $2 . $1 = TRUE );

defpred S_{2}[ object , Function, Function] means ( $1 in dom $2 & $2 . $1 = FALSE & $1 in dom $3 & $3 . $1 = FALSE );

deffunc H_{1}( Function, Function) -> set = { d where d is Element of D : ( S_{1}[d,$1] or S_{1}[d,$2] or S_{2}[d,$1,$2] ) } ;

ex b_{1} being Function of [:(Pr D),(Pr D):],(Pr D) st

for p, q being PartialPredicate of D holds

( dom (b_{1} . (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_{1} . (p,q)) . d = TRUE ) & ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE implies (b_{1} . (p,q)) . d = FALSE ) ) ) )

for b_{1}, b_{2} being Function of [:(Pr D),(Pr D):],(Pr D) st ( for p, q being PartialPredicate of D holds

( dom (b_{1} . (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_{1} . (p,q)) . d = TRUE ) & ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE implies (b_{1} . (p,q)) . d = FALSE ) ) ) ) ) & ( for p, q being PartialPredicate of D holds

( dom (b_{2} . (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_{2} . (p,q)) . d = TRUE ) & ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE implies (b_{2} . (p,q)) . d = FALSE ) ) ) ) ) holds

b_{1} = b_{2}

end;
defpred S

defpred S

deffunc H

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

ex b

for p, q being PartialPredicate of D holds

( dom (b

( ( ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) ) implies (b

proof end;

uniqueness for b

( dom (b

( ( ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) ) implies (b

( dom (b

( ( ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) ) implies (b

b

proof end;

:: deftheorem Def4 defines PPdisjunction PARTPR_1:def 4 :

for D being non empty set

for b_{2} being Function of [:(Pr D),(Pr D):],(Pr D) holds

( b_{2} = PPdisjunction D iff for p, q being PartialPredicate of D holds

( dom (b_{2} . (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_{2} . (p,q)) . d = TRUE ) & ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE implies (b_{2} . (p,q)) . d = FALSE ) ) ) ) );

for D being non empty set

for b

( b

( dom (b

( ( ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) ) implies (b

definition

let D be non empty set ;

let p, q be PartialPredicate of D;

coherence

(PPdisjunction D) . (p,q) is PartialPredicate of D

for b_{1}, p, q being PartialPredicate of D st b_{1} = (PPdisjunction D) . (p,q) holds

b_{1} = (PPdisjunction D) . (q,p)

for p being PartialPredicate of D holds p = (PPdisjunction D) . (p,p)

end;
let p, q be PartialPredicate of D;

coherence

(PPdisjunction D) . (p,q) is PartialPredicate of D

proof end;

commutativity for b

b

proof end;

idempotence for p being PartialPredicate of D holds p = (PPdisjunction D) . (p,p)

proof 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);

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 ) )

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

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 )

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

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

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 )

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)

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)

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;

PP_not (PP_or ((PP_not p),(PP_not q))) is PartialPredicate of D ;

commutativity

for b_{1}, p, q being PartialPredicate of D st b_{1} = PP_not (PP_or ((PP_not p),(PP_not q))) holds

b_{1} = 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))) ;

coherence

PP_or ((PP_not p),q) is PartialPredicate of D ;

end;
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)));

PP_not (PP_or ((PP_not p),(PP_not q))) is PartialPredicate of D ;

commutativity

for b

b

idempotence

for p being PartialPredicate of D holds p = PP_not (PP_or ((PP_not p),(PP_not p))) ;

coherence

PP_or ((PP_not p),q) is PartialPredicate of D ;

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

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

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 ) ) }

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 ) )

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

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

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

theorem :: PARTPR_1:21

theorem :: PARTPR_1:22

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 )

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

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 )

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;

theorem :: PARTPR_1:26

theorem :: PARTPR_1:27

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)))

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 ) ) }

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 ) )

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

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

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

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

theorem :: PARTPR_1:38

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 )

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 )

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)

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)

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;

theorem :: PARTPR_1:46

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

for p being PartialPredicate of D holds PP_and (p,(PP_False D)) = PP_False D

proof end;

theorem :: PARTPR_1:48

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)

for p being PartialPredicate of D holds PP_or (p,(PP_not p)) = (PP_True D) | (dom p)

proof end;

theorem :: PARTPR_1:50

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)

for p being PartialPredicate of D holds PP_and (p,(PP_not p)) = (PP_False D) | (dom p)

proof end;

theorem :: PARTPR_1:52

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

for p being PartialPredicate of D holds PP_imp ((PP_False D),p) = PP_True D

proof end;

theorem :: PARTPR_1:54

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)

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;

definition

let D be non empty set ;

ex b_{1} being BinOp of (Pr D) st

for p, q being PartialPredicate of D holds b_{1} . (p,q) = PP_and (p,q)

for b_{1}, b_{2} being BinOp of (Pr D) st ( for p, q being PartialPredicate of D holds b_{1} . (p,q) = PP_and (p,q) ) & ( for p, q being PartialPredicate of D holds b_{2} . (p,q) = PP_and (p,q) ) holds

b_{1} = b_{2}

ex b_{1} being BinOp of (Pr D) st

for p, q being PartialPredicate of D holds b_{1} . (p,q) = PP_or (p,q)

for b_{1}, b_{2} being BinOp of (Pr D) st ( for p, q being PartialPredicate of D holds b_{1} . (p,q) = PP_or (p,q) ) & ( for p, q being PartialPredicate of D holds b_{2} . (p,q) = PP_or (p,q) ) holds

b_{1} = b_{2}

ex b_{1} being UnOp of (Pr D) st

for p being PartialPredicate of D holds b_{1} . p = PP_not p

for b_{1}, b_{2} being UnOp of (Pr D) st ( for p being PartialPredicate of D holds b_{1} . p = PP_not p ) & ( for p being PartialPredicate of D holds b_{2} . p = PP_not p ) holds

b_{1} = b_{2}

end;
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 for p, q being PartialPredicate of D holds it . (p,q) = PP_and (p,q);

ex b

for p, q being PartialPredicate of D holds b

proof end;

uniqueness for 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 for p, q being PartialPredicate of D holds it . (p,q) = PP_or (p,q);

ex b

for p, q being PartialPredicate of D holds b

proof end;

uniqueness for 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 for p being PartialPredicate of D holds it . p = PP_not p;

ex b

for p being PartialPredicate of D holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def11 defines PartialPredConnectivesMeet PARTPR_1:def 11 :

for D being non empty set

for b_{2} being BinOp of (Pr D) holds

( b_{2} = PartialPredConnectivesMeet D iff for p, q being PartialPredicate of D holds b_{2} . (p,q) = PP_and (p,q) );

for D being non empty set

for b

( b

:: deftheorem Def12 defines PartialPredConnectivesJoin PARTPR_1:def 12 :

for D being non empty set

for b_{2} being BinOp of (Pr D) holds

( b_{2} = PartialPredConnectivesJoin D iff for p, q being PartialPredicate of D holds b_{2} . (p,q) = PP_or (p,q) );

for D being non empty set

for b

( b

:: deftheorem Def13 defines PartialPredConnectivesCompl PARTPR_1:def 13 :

for D being non empty set

for b_{2} being UnOp of (Pr D) holds

( b_{2} = PartialPredConnectivesCompl D iff for p being PartialPredicate of D holds b_{2} . p = PP_not p );

for D being non empty set

for b

( b

definition

let D be non empty set ;

OrthoLattStr(# (Pr D),(PartialPredConnectivesJoin D),(PartialPredConnectivesMeet D),(PartialPredConnectivesCompl D) #) is strict OrthoLattStr ;

end;
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) #);

OrthoLattStr(# (Pr D),(PartialPredConnectivesJoin D),(PartialPredConnectivesMeet D),(PartialPredConnectivesCompl D) #) is strict OrthoLattStr ;

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

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;

coherence

not OrthoLattStr(# D,f,g,h #) is empty

end;
let f, g be BinOp of D;

let h be UnOp of D;

coherence

not OrthoLattStr(# D,f,g,h #) is empty

proof end;

registration

let D be non empty set ;

coherence

( not PartialPredConnectivesLatt D is empty & PartialPredConnectivesLatt D is constituted-Functions ) ;

end;
coherence

( not PartialPredConnectivesLatt D is empty & PartialPredConnectivesLatt D is constituted-Functions ) ;

registration

existence

ex b_{1} being LattStr st

( not b_{1} is empty & b_{1} is constituted-Functions )

end;
ex b

( not b

proof end;

registration

existence

ex b_{1} being OrthoLattStr st

( b_{1} is strict & not b_{1} is empty & b_{1} is constituted-Functions )

end;
ex b

( b

proof end;

registration

let D be non empty set ;

coherence

PartialPredConnectivesLatt D is Lattice-like

PartialPredConnectivesLatt D is bounded

( PartialPredConnectivesLatt D is de_Morgan & PartialPredConnectivesLatt D is join-idempotent & PartialPredConnectivesLatt D is with_idempotent_element )

end;
coherence

PartialPredConnectivesLatt D is Lattice-like

proof end;

coherence PartialPredConnectivesLatt D is bounded

proof end;

coherence ( PartialPredConnectivesLatt D is de_Morgan & PartialPredConnectivesLatt D is join-idempotent & PartialPredConnectivesLatt D is with_idempotent_element )

proof 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) ) );

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 ;

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

for b being Element of L ex a being Element of L st a is_a_partial_complement_of b;

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

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 ;

end;
attr IT is partially_Boolean means :: PARTPR_1:def 17

( IT is bounded & IT is partially_complemented & IT is distributive );

( IT is bounded & IT is partially_complemented & IT is distributive );

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

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

for b_{1} being non empty constituted-Functions LattStr st b_{1} is partially_Boolean holds

( b_{1} is bounded & b_{1} is partially_complemented & b_{1} is distributive )
;

for b_{1} being non empty constituted-Functions LattStr st b_{1} is bounded & b_{1} is partially_complemented & b_{1} is distributive holds

b_{1} is partially_Boolean
;

end;

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

coherence for b

( b

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

coherence for b

b

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

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

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)))

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;

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

for L being non empty OrthoLattStr holds

( L is Kleene iff for x, y being Element of L holds x "/\" (x `) [= y "\/" (y `) );

registration

for b_{1} being non empty meet-commutative meet-absorbing join-absorbing OrthoLattStr st b_{1} is Boolean & b_{1} is well-complemented holds

b_{1} is Kleene
end;

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

b

proof end;

registration
end;

registration

ex b_{1} being non empty constituted-Functions LattStr st

( b_{1} is partially_Boolean & b_{1} is join-idempotent & b_{1} is Lattice-like )
end;

cluster non empty Lattice-like constituted-Functions join-idempotent partially_Boolean for LattStr ;

existence ex b

( b

proof end;

registration

ex b_{1} being non empty OrthoLattStr st

( b_{1} is Kleene & b_{1} is de_Morgan & b_{1} is join-idempotent & b_{1} is with_idempotent_element & b_{1} is Lattice-like & b_{1} is strict )
end;

cluster non empty Lattice-like strict join-idempotent with_idempotent_element de_Morgan Kleene for OrthoLattStr ;

existence ex b

( b

proof end;

registration

ex b_{1} being non empty constituted-Functions OrthoLattStr st

( b_{1} is partially_Boolean & b_{1} is Kleene & b_{1} is de_Morgan & b_{1} is join-idempotent & b_{1} is with_idempotent_element & b_{1} is Lattice-like & b_{1} is strict )
end;

cluster non empty Lattice-like constituted-Functions strict join-idempotent with_idempotent_element de_Morgan partially_Boolean Kleene for OrthoLattStr ;

existence ex b

( b

proof end;