:: On algebras of algorithms and specifications over uninterpreted data
:: 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 ;

cluster -> X -defined for Element of PFuncs (X,Y);

coherence
for b₁ being Element of PFuncs (X,Y) holds b₁ is X -defined ;

cluster -> Y -valued for Element of PFuncs (X,Y);

coherence
for b₁ being Element of PFuncs (X,Y) holds b₁ is Y -valued ;

end;

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

proof end;

registration

cluster non empty non with_non-empty_elements for set ;

existence
ex b₁ being set st
( not b₁ is empty & not b₁ is with_non-empty_elements )

proof end;

end;

definition

let A, B, C be set ;

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
ex b₁ 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₁ . (f,g) = g * f

proof end;

uniqueness
for b₁, b₂ 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₁ . (f,g) = g * f ) & ( for f being PartFunc of A,B
for g being PartFunc of B,C holds b₂ . (f,g) = g * f ) holds
b₁ = b₂

proof end;

end;

:: deftheorem D1 defines PFcompos PARTPR_2:def 1 :
for A, B, C being set
for b₄ being Function of [:(PFuncs (A,B)),(PFuncs (B,C)):],(PFuncs (A,C)) holds
( b₄ = PFcompos (A,B,C) iff for f being PartFunc of A,B
for g being PartFunc of B,C holds b₄ . (f,g) = g * f );

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

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

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

proof end;

definition

let D be set ;

func FPrg D -> set equals :: PARTPR_2:def 2
PFuncs (D,D);

coherence
PFuncs (D,D) is set ;

end;

:: deftheorem defines FPrg PARTPR_2:def 2 :
for D being set holds FPrg D = PFuncs (D,D);

registration

let D be set ;

cluster FPrg D -> non empty functional ;

coherence
( not FPrg D is empty & FPrg D is functional ) ;

end;

definition

let D be set ;
mode BinominativeFunction of D is PartFunc of D,D;

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

proof end;

registration

let D be set ;
let p be PartialPredicate of D;
let F be Function of (Pr D),(Pr D);

cluster F . p -> Relation-like Function-like ;

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

end;

registration

let D be set ;
let F be Function of (Pr D),(Pr D);
let p be Element of Pr D;

cluster F . p -> Relation-like Function-like ;

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

end;

registration

let D be set ;
let p, q be PartialPredicate of D;
let F be Function of [:(Pr D),(Pr D):],(Pr D);

cluster F . (p,q) -> Relation-like Function-like ;

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

end;

registration

let D be set ;
let F be Function of [:(Pr D),(Pr D):],(Pr D);
let p, q be Element of Pr D;

cluster F . (p,q) -> Relation-like Function-like ;

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

end;

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

cluster F . x -> Relation-like Function-like ;

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

end;

registration

let D be set ;
let f be BinominativeFunction of D;
let F be Function of (FPrg D),(FPrg D);

cluster F . f -> Relation-like Function-like ;

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

end;

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

cluster F . (p,f,g) -> Relation-like Function-like ;

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

cluster F . [p,f,g] -> Relation-like Function-like ;

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

end;

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

cluster F . (p,f,q) -> Relation-like Function-like ;

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

cluster F . [p,f,q] -> Relation-like Function-like ;

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

end;

notation

let D be set ;
synonym PPid D for id D;

end;

definition

let D be set ;
:: original: PPid
redefine func PPid D -> BinominativeFunction of D;
coherence
PPid D is BinominativeFunction of D

proof end;

end;

:: Identity composition

definition

let D be non empty set ;
let d be Element of D;

func PP_id d -> Element of D equals :: PARTPR_2:def 3
(PPid D) . d;

coherence
(PPid D) . d is Element of D ;

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;

:: Sequential composition

definition

let D be set ;

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) is Function of [:(FPrg D),(FPrg D):],(FPrg D) ;

end;

:: deftheorem defines PPcomposition PARTPR_2:def 4 :
for D being set holds PPcomposition D = PFcompos (D,D,D);

:: Sequential composition

definition

let D be set ;
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) is BinominativeFunction of D

proof end;

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

:: Prediction composition

definition

let D be set ;

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) is Function of [:(FPrg D),(Pr D):],(Pr D) ;

end;

:: deftheorem defines PPprediction PARTPR_2:def 6 :
for D being set holds PPprediction D = PFcompos (D,D,BOOLEAN);

:: Prediction composition

definition

let D be set ;
let f be BinominativeFunction of D;
let p be PartialPredicate of D;

func PP_prediction (f,p) -> PartialPredicate of D equals :: PARTPR_2:def 7
(PPprediction D) . (f,p);

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

proof end;

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

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;

cluster F . (p,f,g) -> Relation-like Function-like ;

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

end;

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

proof end;

scheme :: PARTPR_2:sch 1
PredToNomPredEx{ F₁() -> set , F₂() -> set , P₁[ object ] } :

ex p being PartialPredicate of F₁() st
( dom p = F₂() & ( for d being object st d in dom p holds
( ( P₁[d] implies p . d = TRUE ) & ( P₁[d] implies p . d = FALSE ) ) ) )

provided

A1: F₂() c= F₁()

proof end;

scheme :: PARTPR_2:sch 2
PredToNomPredUnique{ F₁() -> set , F₂() -> set , P₁[ object ] } :

for p, q being PartialPredicate of F₁() st dom p = F₂() & ( for d being object st d in dom p holds
( ( P₁[d] implies p . d = TRUE ) & ( P₁[d] implies p . d = FALSE ) ) ) & dom q = F₂() & ( for d being object st d in dom q holds
( ( P₁[d] implies q . d = TRUE ) & ( P₁[d] implies q . d = FALSE ) ) ) holds
p = q

proof end;

:: Emptiness checking predicate

definition

let D be set ;
defpred S₁[ object ] means $1 = {} ;

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
ex b₁ being PartialPredicate of D st
( dom b₁ = D & ( for d being object st d in dom b₁ holds
( ( d = {} implies b₁ . d = TRUE ) & ( d <> {} implies b₁ . d = FALSE ) ) ) )

proof end;

uniqueness
for b₁, b₂ being PartialPredicate of D st dom b₁ = D & ( for d being object st d in dom b₁ holds
( ( d = {} implies b₁ . d = TRUE ) & ( d <> {} implies b₁ . d = FALSE ) ) ) & dom b₂ = D & ( for d being object st d in dom b₂ holds
( ( d = {} implies b₂ . d = TRUE ) & ( d <> {} implies b₂ . d = FALSE ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines PPisEmpty PARTPR_2:def 8 :
for D being set
for b₂ being PartialPredicate of D holds
( b₂ = PPisEmpty D iff ( dom b₂ = D & ( for d being object st d in dom b₂ holds
( ( d = {} implies b₂ . d = TRUE ) & ( d <> {} implies b₂ . d = FALSE ) ) ) ) );

:: Empty constant function

definition

let D be non with_non-empty_elements set ;

func PPEmpty D -> BinominativeFunction of D equals :: PARTPR_2:def 9
D --> {};

coherence
D --> {} is BinominativeFunction of D

proof end;

end;

:: deftheorem defines PPEmpty PARTPR_2:def 9 :
for D being non with_non-empty_elements set holds PPEmpty D = D --> {};

:: Empty function

definition

let D be set ;

func PPBottomFunc D -> BinominativeFunction of D equals :: PARTPR_2:def 10
{} ;

coherence
{} is BinominativeFunction of D by RELSET_1:12;

end;

:: deftheorem defines PPBottomFunc PARTPR_2:def 10 :
for D being set holds PPBottomFunc D = {} ;

:: Branching composition

definition

let D be non empty set ;
defpred S₁[ object , Function, Function] means ( $1 in dom $2 & $2 . $1 = TRUE & $1 in dom $3 );
defpred S₂[ object , Function, Function] means ( $1 in dom $2 & $2 . $1 = FALSE & $1 in dom $3 );
deffunc H₁( Function, Function, Function) -> set = { d where d is Element of D : ( S₁[d,$1,$2] or S₂[d,$1,$3] ) } ;

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
ex b₁ 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₁ . (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₁ . (p,f,g)) . d = f . d ) & ( d in dom p & p . d = FALSE & d in dom g implies (b₁ . (p,f,g)) . d = g . d ) ) ) )

proof end;

uniqueness
for b₁, b₂ 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₁ . (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₁ . (p,f,g)) . d = f . d ) & ( d in dom p & p . d = FALSE & d in dom g implies (b₁ . (p,f,g)) . d = g . d ) ) ) ) ) & ( for p being PartialPredicate of D
for f, g being BinominativeFunction of D holds
( dom (b₂ . (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₂ . (p,f,g)) . d = f . d ) & ( d in dom p & p . d = FALSE & d in dom g implies (b₂ . (p,f,g)) . d = g . d ) ) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def13 defines PPIF PARTPR_2:def 11 :
for D being non empty set
for b₂ being Function of [:(Pr D),(FPrg D),(FPrg D):],(FPrg D) holds
( b₂ = PPIF D iff for p being PartialPredicate of D
for f, g being BinominativeFunction of D holds
( dom (b₂ . (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₂ . (p,f,g)) . d = f . d ) & ( d in dom p & p . d = FALSE & d in dom g implies (b₂ . (p,f,g)) . d = g . d ) ) ) ) );

:: Branching composition

definition

let D be non empty set ;
let p be PartialPredicate of D;
let f, g be BinominativeFunction of D;

func PP_IF (p,f,g) -> BinominativeFunction of D equals :: PARTPR_2:def 12
(PPIF D) . (p,f,g);

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

proof end;

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

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

proof end;

:: Monotone Floyd-Hoare composition

definition

let D be non empty set ;
defpred S₁[ object , Function, Function, Function] means ( ( $1 in dom $2 & $2 . $1 = FALSE ) or ( $1 in dom ($4 * $3) & ($4 * $3) . $1 = TRUE ) );
defpred S₂[ object , Function, Function, Function] means ( $1 in dom $2 & $2 . $1 = TRUE & $1 in dom ($4 * $3) & ($4 * $3) . $1 = FALSE );
deffunc H₁( Function, Function, Function) -> set = { d where d is Element of D : ( S₁[d,$1,$2,$3] or S₂[d,$1,$2,$3] ) } ;

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
ex b₁ 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₁ . (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₁ . (p,f,q)) . d = TRUE ) & ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE implies (b₁ . (p,f,q)) . d = FALSE ) ) ) )

proof end;

uniqueness
for b₁, b₂ 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₁ . (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₁ . (p,f,q)) . d = TRUE ) & ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE implies (b₁ . (p,f,q)) . d = FALSE ) ) ) ) ) & ( for p, q being PartialPredicate of D
for f being BinominativeFunction of D holds
( dom (b₂ . (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₂ . (p,f,q)) . d = TRUE ) & ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE implies (b₂ . (p,f,q)) . d = FALSE ) ) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def15 defines PPFH PARTPR_2:def 13 :
for D being non empty set
for b₂ being Function of [:(Pr D),(FPrg D),(Pr D):],(Pr D) holds
( b₂ = PPFH D iff for p, q being PartialPredicate of D
for f being BinominativeFunction of D holds
( dom (b₂ . (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₂ . (p,f,q)) . d = TRUE ) & ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE implies (b₂ . (p,f,q)) . d = FALSE ) ) ) ) );

:: Monotone Floyd-Hoare composition

definition

let D be non empty set ;
let p, q be PartialPredicate of D;
let f be BinominativeFunction of D;

func PP_FH (p,f,q) -> PartialPredicate of D equals :: PARTPR_2:def 14
(PPFH D) . (p,f,q);

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

proof end;

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

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

proof end;

:: Cycle composition

definition

let D be non empty set ;
defpred S₁[ 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₁( Function, Function) -> set = { d where d is Element of D : ex n being Nat st S₁[d,$1,$2,n] } ;

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
ex b₁ 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₁ . (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₁ . (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₁ . (p,f)) . d = (iter (f,n)) . d ) ) )

proof end;

uniqueness
for b₁, b₂ 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₁ . (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₁ . (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₁ . (p,f)) . d = (iter (f,n)) . d ) ) ) ) & ( for p being PartialPredicate of D
for f being BinominativeFunction of D holds
( dom (b₂ . (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₂ . (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₂ . (p,f)) . d = (iter (f,n)) . d ) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines PPwhile PARTPR_2:def 15 :
for D being non empty set
for b₂ being Function of [:(Pr D),(FPrg D):],(FPrg D) holds
( b₂ = PPwhile D iff for p being PartialPredicate of D
for f being BinominativeFunction of D holds
( dom (b₂ . (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₂ . (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₂ . (p,f)) . d = (iter (f,n)) . d ) ) ) );

:: Cycle composition

definition

let D be non empty set ;
let p be PartialPredicate of D;
let f be BinominativeFunction of D;

func PP_while (p,f) -> BinominativeFunction of D equals :: PARTPR_2:def 16
(PPwhile D) . (p,f);

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

proof end;

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

definition

let D be non empty set ;
defpred S₁[ object , Function] means $1 in dom $2;
deffunc H₁( Function) -> set = { d where d is Element of D : not d in dom $1 } ;

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
ex b₁ being Function of (Pr D),(Pr D) st
for p being PartialPredicate of D holds
( dom (b₁ . 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₁ . 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) = { 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₁ . p) . d = TRUE ) ) ) & ( for p being PartialPredicate of D holds
( dom (b₂ . 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₂ . p) . d = TRUE ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def19 defines PPinversion PARTPR_2:def 17 :
for D being non empty set
for b₂ being Function of (Pr D),(Pr D) holds
( b₂ = PPinversion D iff for p being PartialPredicate of D holds
( dom (b₂ . 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₂ . p) . d = TRUE ) ) );

definition

let D be non empty set ;
let p be PartialPredicate of D;

func PP_inversion p -> PartialPredicate of D equals :: PARTPR_2:def 18
(PPinversion D) . p;

coherence
(PPinversion D) . p is PartialPredicate of D

proof end;

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;

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

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

proof end;