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

::

:: Received June 29, 2018

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

registration

let X, Y be set ;

coherence

for b_{1} being Element of PFuncs (X,Y) holds b_{1} is X -defined
;

coherence

for b_{1} being Element of PFuncs (X,Y) holds b_{1} is Y -valued
;

end;
coherence

for b

coherence

for b

theorem Th1: :: PARTPR_2:1

for X, Y, Z, T being set

for x, y, z being object

for f being Function of [:X,Y,Z:],T st x in X & y in Y & z in Z & T <> {} holds

f . (x,y,z) in T

for x, y, z being object

for f being Function of [:X,Y,Z:],T st x in X & y in Y & z in Z & T <> {} holds

f . (x,y,z) in T

proof end;

registration

existence

ex b_{1} being set st

( not b_{1} is empty & not b_{1} is with_non-empty_elements )

end;
ex b

( not b

proof end;

definition

let A, B, C be set ;

ex b_{1} being Function of [:(PFuncs (A,B)),(PFuncs (B,C)):],(PFuncs (A,C)) st

for f being PartFunc of A,B

for g being PartFunc of B,C holds b_{1} . (f,g) = g * f

for b_{1}, b_{2} being Function of [:(PFuncs (A,B)),(PFuncs (B,C)):],(PFuncs (A,C)) st ( for f being PartFunc of A,B

for g being PartFunc of B,C holds b_{1} . (f,g) = g * f ) & ( for f being PartFunc of A,B

for g being PartFunc of B,C holds b_{2} . (f,g) = g * f ) holds

b_{1} = b_{2}

end;
func PFcompos (A,B,C) -> Function of [:(PFuncs (A,B)),(PFuncs (B,C)):],(PFuncs (A,C)) means :D1: :: PARTPR_2:def 1

for f being PartFunc of A,B

for g being PartFunc of B,C holds it . (f,g) = g * f;

existence for f being PartFunc of A,B

for g being PartFunc of B,C holds it . (f,g) = g * f;

ex b

for f being PartFunc of A,B

for g being PartFunc of B,C holds b

proof end;

uniqueness for b

for g being PartFunc of B,C holds b

for g being PartFunc of B,C holds b

b

proof end;

:: deftheorem D1 defines PFcompos PARTPR_2:def 1 :

for A, B, C being set

for b_{4} being Function of [:(PFuncs (A,B)),(PFuncs (B,C)):],(PFuncs (A,C)) holds

( b_{4} = PFcompos (A,B,C) iff for f being PartFunc of A,B

for g being PartFunc of B,C holds b_{4} . (f,g) = g * f );

for A, B, C being set

for b

( b

for g being PartFunc of B,C holds b

theorem :: PARTPR_2:2

for D being non empty set

for p, q being PartialPredicate of D st q is total holds

dom p c= dom (PP_or (p,q))

for p, q being PartialPredicate of D st q is total holds

dom p c= dom (PP_or (p,q))

proof end;

theorem :: PARTPR_2:3

for D being non empty set

for p, q being PartialPredicate of D st q is total holds

dom p c= dom (PP_and (p,q))

for p, q being PartialPredicate of D st q is total holds

dom p c= dom (PP_and (p,q))

proof end;

theorem :: PARTPR_2:4

for D being non empty set

for p, q being PartialPredicate of D st q is total holds

dom p c= dom (PP_imp (p,q))

for p, q being PartialPredicate of D st q is total holds

dom p c= dom (PP_imp (p,q))

proof end;

theorem :: PARTPR_2:5

for D being non empty set

for f being BinominativeFunction of D holds id (field f) is BinominativeFunction of D

for f being BinominativeFunction of D holds id (field f) is BinominativeFunction of D

proof end;

registration

let D be set ;

let p be PartialPredicate of D;

let F be Function of (Pr D),(Pr D);

coherence

( F . p is Function-like & F . p is Relation-like ) ;

end;
let p be PartialPredicate of D;

let F be Function of (Pr D),(Pr D);

coherence

( F . p is Function-like & F . p is Relation-like ) ;

registration

let D be set ;

let F be Function of (Pr D),(Pr D);

let p be Element of Pr D;

coherence

( F . p is Function-like & F . p is Relation-like ) ;

end;
let F be Function of (Pr D),(Pr D);

let p be Element of Pr D;

coherence

( F . p is Function-like & F . p is Relation-like ) ;

registration

let D be set ;

let p, q be PartialPredicate of D;

let F be Function of [:(Pr D),(Pr D):],(Pr D);

coherence

( F . (p,q) is Function-like & F . (p,q) is Relation-like ) ;

end;
let p, q be PartialPredicate of D;

let F be Function of [:(Pr D),(Pr D):],(Pr D);

coherence

( F . (p,q) is Function-like & F . (p,q) is Relation-like ) ;

registration

let D be set ;

let F be Function of [:(Pr D),(Pr D):],(Pr D);

let p, q be Element of Pr D;

coherence

( F . (p,q) is Function-like & F . (p,q) is Relation-like ) ;

end;
let F be Function of [:(Pr D),(Pr D):],(Pr D);

let p, q be Element of Pr D;

coherence

( F . (p,q) is Function-like & F . (p,q) is Relation-like ) ;

registration

let D be set ;

let F be Function of [:(Pr D),(Pr D):],(Pr D);

let x be Element of [:(Pr D),(Pr D):];

coherence

( F . x is Function-like & F . x is Relation-like ) ;

end;
let F be Function of [:(Pr D),(Pr D):],(Pr D);

let x be Element of [:(Pr D),(Pr D):];

coherence

( F . x is Function-like & F . x is Relation-like ) ;

registration

let D be set ;

let f be BinominativeFunction of D;

let F be Function of (FPrg D),(FPrg D);

coherence

( F . f is Function-like & F . f is Relation-like ) ;

end;
let f be BinominativeFunction of D;

let F be Function of (FPrg D),(FPrg D);

coherence

( F . f is Function-like & F . f is Relation-like ) ;

registration

let D be set ;

let p be PartialPredicate of D;

let f, g be BinominativeFunction of D;

let F be Function of [:(Pr D),(FPrg D),(FPrg D):],(FPrg D);

coherence

( F . (p,f,g) is Function-like & F . (p,f,g) is Relation-like ) ;

coherence

( F . [p,f,g] is Function-like & F . [p,f,g] is Relation-like ) ;

end;
let p be PartialPredicate of D;

let f, g be BinominativeFunction of D;

let F be Function of [:(Pr D),(FPrg D),(FPrg D):],(FPrg D);

coherence

( F . (p,f,g) is Function-like & F . (p,f,g) is Relation-like ) ;

coherence

( F . [p,f,g] is Function-like & F . [p,f,g] is Relation-like ) ;

registration

let D be set ;

let p, q be PartialPredicate of D;

let f be BinominativeFunction of D;

let F be Function of [:(Pr D),(FPrg D),(Pr D):],(Pr D);

coherence

( F . (p,f,q) is Function-like & F . (p,f,q) is Relation-like ) ;

coherence

( F . [p,f,q] is Function-like & F . [p,f,q] is Relation-like ) ;

end;
let p, q be PartialPredicate of D;

let f be BinominativeFunction of D;

let F be Function of [:(Pr D),(FPrg D),(Pr D):],(Pr D);

coherence

( F . (p,f,q) is Function-like & F . (p,f,q) is Relation-like ) ;

coherence

( F . [p,f,q] is Function-like & F . [p,f,q] is Relation-like ) ;

definition

let D be set ;

:: original: PPid

redefine func PPid D -> BinominativeFunction of D;

coherence

PPid D is BinominativeFunction of D

end;
:: original: PPid

redefine func PPid D -> BinominativeFunction of D;

coherence

PPid D is BinominativeFunction of D

proof end;

:: Identity composition

definition
end;

:: deftheorem defines PP_id PARTPR_2:def 3 :

for D being non empty set

for d being Element of D holds PP_id d = (PPid D) . d;

for D being non empty set

for d being Element of D holds PP_id d = (PPid D) . d;

definition

let D be set ;

PFcompos (D,D,D) is Function of [:(FPrg D),(FPrg D):],(FPrg D) ;

end;
func PPcomposition D -> Function of [:(FPrg D),(FPrg D):],(FPrg D) equals :: PARTPR_2:def 4

PFcompos (D,D,D);

coherence PFcompos (D,D,D);

PFcompos (D,D,D) is Function of [:(FPrg D),(FPrg D):],(FPrg D) ;

:: deftheorem defines PPcomposition PARTPR_2:def 4 :

for D being set holds PPcomposition D = PFcompos (D,D,D);

for D being set holds PPcomposition D = PFcompos (D,D,D);

definition

let D be set ;

let f, g be BinominativeFunction of D;

(PPcomposition D) . (f,g) is BinominativeFunction of D

end;
let f, g be BinominativeFunction of D;

func PP_composition (f,g) -> BinominativeFunction of D equals :: PARTPR_2:def 5

(PPcomposition D) . (f,g);

coherence (PPcomposition D) . (f,g);

(PPcomposition D) . (f,g) is BinominativeFunction of D

proof end;

:: deftheorem defines PP_composition PARTPR_2:def 5 :

for D being set

for f, g being BinominativeFunction of D holds PP_composition (f,g) = (PPcomposition D) . (f,g);

for D being set

for f, g being BinominativeFunction of D holds PP_composition (f,g) = (PPcomposition D) . (f,g);

definition

let D be set ;

PFcompos (D,D,BOOLEAN) is Function of [:(FPrg D),(Pr D):],(Pr D) ;

end;
func PPprediction D -> Function of [:(FPrg D),(Pr D):],(Pr D) equals :: PARTPR_2:def 6

PFcompos (D,D,BOOLEAN);

coherence PFcompos (D,D,BOOLEAN);

PFcompos (D,D,BOOLEAN) is Function of [:(FPrg D),(Pr D):],(Pr D) ;

:: deftheorem defines PPprediction PARTPR_2:def 6 :

for D being set holds PPprediction D = PFcompos (D,D,BOOLEAN);

for D being set holds PPprediction D = PFcompos (D,D,BOOLEAN);

definition

let D be set ;

let f be BinominativeFunction of D;

let p be PartialPredicate of D;

coherence

(PPprediction D) . (f,p) is PartialPredicate of D

end;
let f be BinominativeFunction of D;

let p be PartialPredicate of D;

coherence

(PPprediction D) . (f,p) is PartialPredicate of D

proof end;

:: deftheorem defines PP_prediction PARTPR_2:def 7 :

for D being set

for f being BinominativeFunction of D

for p being PartialPredicate of D holds PP_prediction (f,p) = (PPprediction D) . (f,p);

for D being set

for f being BinominativeFunction of D

for p being PartialPredicate of D holds PP_prediction (f,p) = (PPprediction D) . (f,p);

registration

let D be set ;

let F be Function of [:(Pr D),(FPrg D),(FPrg D):],(FPrg D);

let p be PartialPredicate of D;

let f, g be BinominativeFunction of D;

coherence

( F . (p,f,g) is Function-like & F . (p,f,g) is Relation-like ) ;

end;
let F be Function of [:(Pr D),(FPrg D),(FPrg D):],(FPrg D);

let p be PartialPredicate of D;

let f, g be BinominativeFunction of D;

coherence

( F . (p,f,g) is Function-like & F . (p,f,g) is Relation-like ) ;

theorem :: PARTPR_2:6

for x being object

for D being set

for p being PartialPredicate of D

for f being BinominativeFunction of D st x in dom (PP_prediction (f,p)) holds

( x in dom (p * f) & ( (p * f) . x = TRUE or (p * f) . x = FALSE ) )

for D being set

for p being PartialPredicate of D

for f being BinominativeFunction of D st x in dom (PP_prediction (f,p)) holds

( x in dom (p * f) & ( (p * f) . x = TRUE or (p * f) . x = FALSE ) )

proof end;

scheme :: PARTPR_2:sch 2

PredToNomPredUnique{ F_{1}() -> set , F_{2}() -> set , P_{1}[ object ] } :

PredToNomPredUnique{ F

for p, q being PartialPredicate of F_{1}() st dom p = F_{2}() & ( for d being object st d in dom p holds

( ( P_{1}[d] implies p . d = TRUE ) & ( P_{1}[d] implies p . d = FALSE ) ) ) & dom q = F_{2}() & ( for d being object st d in dom q holds

( ( P_{1}[d] implies q . d = TRUE ) & ( P_{1}[d] implies q . d = FALSE ) ) ) holds

p = q

( ( P

( ( P

p = q

proof end;

definition

let D be set ;

defpred S_{1}[ object ] means $1 = {} ;

ex b_{1} being PartialPredicate of D st

( dom b_{1} = D & ( for d being object st d in dom b_{1} holds

( ( d = {} implies b_{1} . d = TRUE ) & ( d <> {} implies b_{1} . d = FALSE ) ) ) )

for b_{1}, b_{2} being PartialPredicate of D st dom b_{1} = D & ( for d being object st d in dom b_{1} holds

( ( d = {} implies b_{1} . d = TRUE ) & ( d <> {} implies b_{1} . d = FALSE ) ) ) & dom b_{2} = D & ( for d being object st d in dom b_{2} holds

( ( d = {} implies b_{2} . d = TRUE ) & ( d <> {} implies b_{2} . d = FALSE ) ) ) holds

b_{1} = b_{2}

end;
defpred S

func PPisEmpty D -> PartialPredicate of D means :: PARTPR_2:def 8

( dom it = D & ( for d being object st d in dom it holds

( ( d = {} implies it . d = TRUE ) & ( d <> {} implies it . d = FALSE ) ) ) );

existence ( dom it = D & ( for d being object st d in dom it holds

( ( d = {} implies it . d = TRUE ) & ( d <> {} implies it . d = FALSE ) ) ) );

ex b

( dom b

( ( d = {} implies b

proof end;

uniqueness for b

( ( d = {} implies b

( ( d = {} implies b

b

proof end;

:: deftheorem defines PPisEmpty PARTPR_2:def 8 :

for D being set

for b_{2} being PartialPredicate of D holds

( b_{2} = PPisEmpty D iff ( dom b_{2} = D & ( for d being object st d in dom b_{2} holds

( ( d = {} implies b_{2} . d = TRUE ) & ( d <> {} implies b_{2} . d = FALSE ) ) ) ) );

for D being set

for b

( b

( ( d = {} implies b

definition

let D be non with_non-empty_elements set ;

coherence

D --> {} is BinominativeFunction of D

end;
coherence

D --> {} is BinominativeFunction of D

proof end;

:: deftheorem defines PPEmpty PARTPR_2:def 9 :

for D being non with_non-empty_elements set holds PPEmpty D = D --> {};

for D being non with_non-empty_elements set holds PPEmpty D = D --> {};

definition

let D be non empty set ;

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

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

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

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

for p being PartialPredicate of D

for f, g being BinominativeFunction of D holds

( dom (b_{1} . (p,f,g)) = { d where d is Element of D : ( ( d in dom p & p . d = TRUE & d in dom f ) or ( d in dom p & p . d = FALSE & d in dom g ) ) } & ( for d being object holds

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

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

for f, g being BinominativeFunction of D holds

( dom (b_{1} . (p,f,g)) = { d where d is Element of D : ( ( d in dom p & p . d = TRUE & d in dom f ) or ( d in dom p & p . d = FALSE & d in dom g ) ) } & ( for d being object holds

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

for f, g being BinominativeFunction of D holds

( dom (b_{2} . (p,f,g)) = { d where d is Element of D : ( ( d in dom p & p . d = TRUE & d in dom f ) or ( d in dom p & p . d = FALSE & d in dom g ) ) } & ( for d being object holds

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

b_{1} = b_{2}

end;
defpred S

defpred S

deffunc H

func PPIF D -> Function of [:(Pr D),(FPrg D),(FPrg D):],(FPrg D) means :Def13: :: PARTPR_2:def 11

for p being PartialPredicate of D

for f, g being BinominativeFunction of D holds

( dom (it . (p,f,g)) = { d where d is Element of D : ( ( d in dom p & p . d = TRUE & d in dom f ) or ( d in dom p & p . d = FALSE & d in dom g ) ) } & ( for d being object holds

( ( d in dom p & p . d = TRUE & d in dom f implies (it . (p,f,g)) . d = f . d ) & ( d in dom p & p . d = FALSE & d in dom g implies (it . (p,f,g)) . d = g . d ) ) ) );

existence for p being PartialPredicate of D

for f, g being BinominativeFunction of D holds

( dom (it . (p,f,g)) = { d where d is Element of D : ( ( d in dom p & p . d = TRUE & d in dom f ) or ( d in dom p & p . d = FALSE & d in dom g ) ) } & ( for d being object holds

( ( d in dom p & p . d = TRUE & d in dom f implies (it . (p,f,g)) . d = f . d ) & ( d in dom p & p . d = FALSE & d in dom g implies (it . (p,f,g)) . d = g . d ) ) ) );

ex b

for p being PartialPredicate of D

for f, g being BinominativeFunction of D holds

( dom (b

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

proof end;

uniqueness for b

for f, g being BinominativeFunction of D holds

( dom (b

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

for f, g being BinominativeFunction of D holds

( dom (b

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

b

proof end;

:: deftheorem Def13 defines PPIF PARTPR_2:def 11 :

for D being non empty set

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

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

for f, g being BinominativeFunction of D holds

( dom (b_{2} . (p,f,g)) = { d where d is Element of D : ( ( d in dom p & p . d = TRUE & d in dom f ) or ( d in dom p & p . d = FALSE & d in dom g ) ) } & ( for d being object holds

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

for D being non empty set

for b

( b

for f, g being BinominativeFunction of D holds

( dom (b

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

definition

let D be non empty set ;

let p be PartialPredicate of D;

let f, g be BinominativeFunction of D;

coherence

(PPIF D) . (p,f,g) is BinominativeFunction of D

end;
let p be PartialPredicate of D;

let f, g be BinominativeFunction of D;

coherence

(PPIF D) . (p,f,g) is BinominativeFunction of D

proof end;

:: deftheorem defines PP_IF PARTPR_2:def 12 :

for D being non empty set

for p being PartialPredicate of D

for f, g being BinominativeFunction of D holds PP_IF (p,f,g) = (PPIF D) . (p,f,g);

for D being non empty set

for p being PartialPredicate of D

for f, g being BinominativeFunction of D holds PP_IF (p,f,g) = (PPIF D) . (p,f,g);

theorem :: PARTPR_2:7

for x being object

for D being non empty set

for p being PartialPredicate of D

for f, g being BinominativeFunction of D holds

( not x in dom (PP_IF (p,f,g)) or ( x in dom p & p . x = TRUE & x in dom f ) or ( x in dom p & p . x = FALSE & x in dom g ) )

for D being non empty set

for p being PartialPredicate of D

for f, g being BinominativeFunction of D holds

( not x in dom (PP_IF (p,f,g)) or ( x in dom p & p . x = TRUE & x in dom f ) or ( x in dom p & p . x = FALSE & x in dom g ) )

proof end;

definition

let D be non empty set ;

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

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

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

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

for p, q being PartialPredicate of D

for f being BinominativeFunction of D holds

( dom (b_{1} . (p,f,q)) = { d where d is Element of D : ( ( d in dom p & p . d = FALSE ) or ( d in dom (q * f) & (q * f) . d = TRUE ) or ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE ) ) } & ( for d being object holds

( ( ( ( d in dom p & p . d = FALSE ) or ( d in dom (q * f) & (q * f) . d = TRUE ) ) implies (b_{1} . (p,f,q)) . d = TRUE ) & ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE implies (b_{1} . (p,f,q)) . d = FALSE ) ) ) )

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

for f being BinominativeFunction of D holds

( dom (b_{1} . (p,f,q)) = { d where d is Element of D : ( ( d in dom p & p . d = FALSE ) or ( d in dom (q * f) & (q * f) . d = TRUE ) or ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE ) ) } & ( for d being object holds

( ( ( ( d in dom p & p . d = FALSE ) or ( d in dom (q * f) & (q * f) . d = TRUE ) ) implies (b_{1} . (p,f,q)) . d = TRUE ) & ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE implies (b_{1} . (p,f,q)) . d = FALSE ) ) ) ) ) & ( for p, q being PartialPredicate of D

for f being BinominativeFunction of D holds

( dom (b_{2} . (p,f,q)) = { d where d is Element of D : ( ( d in dom p & p . d = FALSE ) or ( d in dom (q * f) & (q * f) . d = TRUE ) or ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE ) ) } & ( for d being object holds

( ( ( ( d in dom p & p . d = FALSE ) or ( d in dom (q * f) & (q * f) . d = TRUE ) ) implies (b_{2} . (p,f,q)) . d = TRUE ) & ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE implies (b_{2} . (p,f,q)) . d = FALSE ) ) ) ) ) holds

b_{1} = b_{2}

end;
defpred S

defpred S

deffunc H

func PPFH D -> Function of [:(Pr D),(FPrg D),(Pr D):],(Pr D) means :Def15: :: PARTPR_2:def 13

for p, q being PartialPredicate of D

for f being BinominativeFunction of D holds

( dom (it . (p,f,q)) = { d where d is Element of D : ( ( d in dom p & p . d = FALSE ) or ( d in dom (q * f) & (q * f) . d = TRUE ) or ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE ) ) } & ( for d being object holds

( ( ( ( d in dom p & p . d = FALSE ) or ( d in dom (q * f) & (q * f) . d = TRUE ) ) implies (it . (p,f,q)) . d = TRUE ) & ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE implies (it . (p,f,q)) . d = FALSE ) ) ) );

existence for p, q being PartialPredicate of D

for f being BinominativeFunction of D holds

( dom (it . (p,f,q)) = { d where d is Element of D : ( ( d in dom p & p . d = FALSE ) or ( d in dom (q * f) & (q * f) . d = TRUE ) or ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE ) ) } & ( for d being object holds

( ( ( ( d in dom p & p . d = FALSE ) or ( d in dom (q * f) & (q * f) . d = TRUE ) ) implies (it . (p,f,q)) . d = TRUE ) & ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE implies (it . (p,f,q)) . d = FALSE ) ) ) );

ex b

for p, q being PartialPredicate of D

for f being BinominativeFunction of D holds

( dom (b

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

proof end;

uniqueness for b

for f being BinominativeFunction of D holds

( dom (b

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

for f being BinominativeFunction of D holds

( dom (b

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

b

proof end;

:: deftheorem Def15 defines PPFH PARTPR_2:def 13 :

for D being non empty set

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

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

for f being BinominativeFunction of D holds

( dom (b_{2} . (p,f,q)) = { d where d is Element of D : ( ( d in dom p & p . d = FALSE ) or ( d in dom (q * f) & (q * f) . d = TRUE ) or ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE ) ) } & ( for d being object holds

( ( ( ( d in dom p & p . d = FALSE ) or ( d in dom (q * f) & (q * f) . d = TRUE ) ) implies (b_{2} . (p,f,q)) . d = TRUE ) & ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE implies (b_{2} . (p,f,q)) . d = FALSE ) ) ) ) );

for D being non empty set

for b

( b

for f being BinominativeFunction of D holds

( dom (b

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

definition

let D be non empty set ;

let p, q be PartialPredicate of D;

let f be BinominativeFunction of D;

coherence

(PPFH D) . (p,f,q) is PartialPredicate of D

end;
let p, q be PartialPredicate of D;

let f be BinominativeFunction of D;

coherence

(PPFH D) . (p,f,q) is PartialPredicate of D

proof end;

:: deftheorem defines PP_FH PARTPR_2:def 14 :

for D being non empty set

for p, q being PartialPredicate of D

for f being BinominativeFunction of D holds PP_FH (p,f,q) = (PPFH D) . (p,f,q);

for D being non empty set

for p, q being PartialPredicate of D

for f being BinominativeFunction of D holds PP_FH (p,f,q) = (PPFH D) . (p,f,q);

theorem :: PARTPR_2:8

for x being object

for D being non empty set

for p, q being PartialPredicate of D

for f being BinominativeFunction of D holds

( not x in dom (PP_FH (p,f,q)) or ( x in dom p & p . x = FALSE ) or ( x in dom (q * f) & (q * f) . x = TRUE ) or ( x in dom p & p . x = TRUE & x in dom (q * f) & (q * f) . x = FALSE ) )

for D being non empty set

for p, q being PartialPredicate of D

for f being BinominativeFunction of D holds

( not x in dom (PP_FH (p,f,q)) or ( x in dom p & p . x = FALSE ) or ( x in dom (q * f) & (q * f) . x = TRUE ) or ( x in dom p & p . x = TRUE & x in dom (q * f) & (q * f) . x = FALSE ) )

proof end;

definition

let D be non empty set ;

defpred S_{1}[ object , Function, Function, Nat] means ( ( for i being Nat st i <= $4 - 1 holds

( $1 in dom ($2 * (iter ($3,i))) & ($2 * (iter ($3,i))) . $1 = TRUE ) ) & $1 in dom ($2 * (iter ($3,$4))) & ($2 * (iter ($3,$4))) . $1 = FALSE );

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

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

for p being PartialPredicate of D

for f being BinominativeFunction of D holds

( dom (b_{1} . (p,f)) = { d where d is Element of D : ex n being Nat st

( ( for i being Nat st i <= n - 1 holds

( d in dom (p * (iter (f,i))) & (p * (iter (f,i))) . d = TRUE ) ) & d in dom (p * (iter (f,n))) & (p * (iter (f,n))) . d = FALSE ) } & ( for d being object st d in dom (b_{1} . (p,f)) holds

ex n being Nat st

( ( for i being Nat st i <= n - 1 holds

( d in dom (p * (iter (f,i))) & (p * (iter (f,i))) . d = TRUE ) ) & d in dom (p * (iter (f,n))) & (p * (iter (f,n))) . d = FALSE & (b_{1} . (p,f)) . d = (iter (f,n)) . d ) ) )

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

for f being BinominativeFunction of D holds

( dom (b_{1} . (p,f)) = { d where d is Element of D : ex n being Nat st

( ( for i being Nat st i <= n - 1 holds

( d in dom (p * (iter (f,i))) & (p * (iter (f,i))) . d = TRUE ) ) & d in dom (p * (iter (f,n))) & (p * (iter (f,n))) . d = FALSE ) } & ( for d being object st d in dom (b_{1} . (p,f)) holds

ex n being Nat st

( ( for i being Nat st i <= n - 1 holds

( d in dom (p * (iter (f,i))) & (p * (iter (f,i))) . d = TRUE ) ) & d in dom (p * (iter (f,n))) & (p * (iter (f,n))) . d = FALSE & (b_{1} . (p,f)) . d = (iter (f,n)) . d ) ) ) ) & ( for p being PartialPredicate of D

for f being BinominativeFunction of D holds

( dom (b_{2} . (p,f)) = { d where d is Element of D : ex n being Nat st

( ( for i being Nat st i <= n - 1 holds

( d in dom (p * (iter (f,i))) & (p * (iter (f,i))) . d = TRUE ) ) & d in dom (p * (iter (f,n))) & (p * (iter (f,n))) . d = FALSE ) } & ( for d being object st d in dom (b_{2} . (p,f)) holds

ex n being Nat st

( ( for i being Nat st i <= n - 1 holds

( d in dom (p * (iter (f,i))) & (p * (iter (f,i))) . d = TRUE ) ) & d in dom (p * (iter (f,n))) & (p * (iter (f,n))) . d = FALSE & (b_{2} . (p,f)) . d = (iter (f,n)) . d ) ) ) ) holds

b_{1} = b_{2}

end;
defpred S

( $1 in dom ($2 * (iter ($3,i))) & ($2 * (iter ($3,i))) . $1 = TRUE ) ) & $1 in dom ($2 * (iter ($3,$4))) & ($2 * (iter ($3,$4))) . $1 = FALSE );

deffunc H

func PPwhile D -> Function of [:(Pr D),(FPrg D):],(FPrg D) means :: PARTPR_2:def 15

for p being PartialPredicate of D

for f being BinominativeFunction of D holds

( dom (it . (p,f)) = { d where d is Element of D : ex n being Nat st

( ( for i being Nat st i <= n - 1 holds

( d in dom (p * (iter (f,i))) & (p * (iter (f,i))) . d = TRUE ) ) & d in dom (p * (iter (f,n))) & (p * (iter (f,n))) . d = FALSE ) } & ( for d being object st d in dom (it . (p,f)) holds

ex n being Nat st

( ( for i being Nat st i <= n - 1 holds

( d in dom (p * (iter (f,i))) & (p * (iter (f,i))) . d = TRUE ) ) & d in dom (p * (iter (f,n))) & (p * (iter (f,n))) . d = FALSE & (it . (p,f)) . d = (iter (f,n)) . d ) ) );

existence for p being PartialPredicate of D

for f being BinominativeFunction of D holds

( dom (it . (p,f)) = { d where d is Element of D : ex n being Nat st

( ( for i being Nat st i <= n - 1 holds

( d in dom (p * (iter (f,i))) & (p * (iter (f,i))) . d = TRUE ) ) & d in dom (p * (iter (f,n))) & (p * (iter (f,n))) . d = FALSE ) } & ( for d being object st d in dom (it . (p,f)) holds

ex n being Nat st

( ( for i being Nat st i <= n - 1 holds

( d in dom (p * (iter (f,i))) & (p * (iter (f,i))) . d = TRUE ) ) & d in dom (p * (iter (f,n))) & (p * (iter (f,n))) . d = FALSE & (it . (p,f)) . d = (iter (f,n)) . d ) ) );

ex b

for p being PartialPredicate of D

for f being BinominativeFunction of D holds

( dom (b

( ( for i being Nat st i <= n - 1 holds

( d in dom (p * (iter (f,i))) & (p * (iter (f,i))) . d = TRUE ) ) & d in dom (p * (iter (f,n))) & (p * (iter (f,n))) . d = FALSE ) } & ( for d being object st d in dom (b

ex n being Nat st

( ( for i being Nat st i <= n - 1 holds

( d in dom (p * (iter (f,i))) & (p * (iter (f,i))) . d = TRUE ) ) & d in dom (p * (iter (f,n))) & (p * (iter (f,n))) . d = FALSE & (b

proof end;

uniqueness for b

for f being BinominativeFunction of D holds

( dom (b

( ( for i being Nat st i <= n - 1 holds

( d in dom (p * (iter (f,i))) & (p * (iter (f,i))) . d = TRUE ) ) & d in dom (p * (iter (f,n))) & (p * (iter (f,n))) . d = FALSE ) } & ( for d being object st d in dom (b

ex n being Nat st

( ( for i being Nat st i <= n - 1 holds

( d in dom (p * (iter (f,i))) & (p * (iter (f,i))) . d = TRUE ) ) & d in dom (p * (iter (f,n))) & (p * (iter (f,n))) . d = FALSE & (b

for f being BinominativeFunction of D holds

( dom (b

( ( for i being Nat st i <= n - 1 holds

( d in dom (p * (iter (f,i))) & (p * (iter (f,i))) . d = TRUE ) ) & d in dom (p * (iter (f,n))) & (p * (iter (f,n))) . d = FALSE ) } & ( for d being object st d in dom (b

ex n being Nat st

( ( for i being Nat st i <= n - 1 holds

( d in dom (p * (iter (f,i))) & (p * (iter (f,i))) . d = TRUE ) ) & d in dom (p * (iter (f,n))) & (p * (iter (f,n))) . d = FALSE & (b

b

proof end;

:: deftheorem defines PPwhile PARTPR_2:def 15 :

for D being non empty set

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

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

for f being BinominativeFunction of D holds

( dom (b_{2} . (p,f)) = { d where d is Element of D : ex n being Nat st

( ( for i being Nat st i <= n - 1 holds

( d in dom (p * (iter (f,i))) & (p * (iter (f,i))) . d = TRUE ) ) & d in dom (p * (iter (f,n))) & (p * (iter (f,n))) . d = FALSE ) } & ( for d being object st d in dom (b_{2} . (p,f)) holds

ex n being Nat st

( ( for i being Nat st i <= n - 1 holds

( d in dom (p * (iter (f,i))) & (p * (iter (f,i))) . d = TRUE ) ) & d in dom (p * (iter (f,n))) & (p * (iter (f,n))) . d = FALSE & (b_{2} . (p,f)) . d = (iter (f,n)) . d ) ) ) );

for D being non empty set

for b

( b

for f being BinominativeFunction of D holds

( dom (b

( ( for i being Nat st i <= n - 1 holds

( d in dom (p * (iter (f,i))) & (p * (iter (f,i))) . d = TRUE ) ) & d in dom (p * (iter (f,n))) & (p * (iter (f,n))) . d = FALSE ) } & ( for d being object st d in dom (b

ex n being Nat st

( ( for i being Nat st i <= n - 1 holds

( d in dom (p * (iter (f,i))) & (p * (iter (f,i))) . d = TRUE ) ) & d in dom (p * (iter (f,n))) & (p * (iter (f,n))) . d = FALSE & (b

definition

let D be non empty set ;

let p be PartialPredicate of D;

let f be BinominativeFunction of D;

coherence

(PPwhile D) . (p,f) is BinominativeFunction of D

end;
let p be PartialPredicate of D;

let f be BinominativeFunction of D;

coherence

(PPwhile D) . (p,f) is BinominativeFunction of D

proof end;

:: deftheorem defines PP_while PARTPR_2:def 16 :

for D being non empty set

for p being PartialPredicate of D

for f being BinominativeFunction of D holds PP_while (p,f) = (PPwhile D) . (p,f);

for D being non empty set

for p being PartialPredicate of D

for f being BinominativeFunction of D holds PP_while (p,f) = (PPwhile D) . (p,f);

definition

let D be non empty set ;

defpred S_{1}[ object , Function] means $1 in dom $2;

deffunc H_{1}( Function) -> set = { d where d is Element of D : not d in dom $1 } ;

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

for p being PartialPredicate of D holds

( dom (b_{1} . p) = { d where d is Element of D : not d in dom p } & ( for d being Element of D st not d in dom p holds

(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) = { d where d is Element of D : not d in dom p } & ( for d being Element of D st not d in dom p holds

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

( dom (b_{2} . p) = { d where d is Element of D : not d in dom p } & ( for d being Element of D st not d in dom p holds

(b_{2} . p) . d = TRUE ) ) ) holds

b_{1} = b_{2}

end;
defpred S

deffunc H

func PPinversion D -> Function of (Pr D),(Pr D) means :Def19: :: PARTPR_2:def 17

for p being PartialPredicate of D holds

( dom (it . p) = { d where d is Element of D : not d in dom p } & ( for d being Element of D st not d in dom p holds

(it . p) . d = TRUE ) );

existence for p being PartialPredicate of D holds

( dom (it . p) = { d where d is Element of D : not d in dom p } & ( for d being Element of D st not d in dom p holds

(it . p) . d = TRUE ) );

ex b

for p being PartialPredicate of D holds

( dom (b

(b

proof end;

uniqueness for b

( dom (b

(b

( dom (b

(b

b

proof end;

:: deftheorem Def19 defines PPinversion PARTPR_2:def 17 :

for D being non empty set

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

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

( dom (b_{2} . p) = { d where d is Element of D : not d in dom p } & ( for d being Element of D st not d in dom p holds

(b_{2} . p) . d = TRUE ) ) );

for D being non empty set

for b

( b

( dom (b

(b

definition

let D be non empty set ;

let p be PartialPredicate of D;

coherence

(PPinversion D) . p is PartialPredicate of D

end;
let p be PartialPredicate of D;

coherence

(PPinversion D) . p is PartialPredicate of D

proof end;

:: deftheorem defines PP_inversion PARTPR_2:def 18 :

for D being non empty set

for p being PartialPredicate of D holds PP_inversion p = (PPinversion D) . p;

for D being non empty set

for p being PartialPredicate of D holds PP_inversion p = (PPinversion D) . p;

theorem :: PARTPR_2:9

for D being non empty set

for p being PartialPredicate of D

for d being Element of D holds

( d in dom p iff not d in dom (PP_inversion p) )

for p being PartialPredicate of D

for d being Element of D holds

( d in dom p iff not d in dom (PP_inversion p) )

proof end;

theorem :: PARTPR_2:10

for D being non empty set

for p being PartialPredicate of D st p is total holds

dom (PP_inversion p) = {}

for p being PartialPredicate of D st p is total holds

dom (PP_inversion p) = {}

proof end;