:: 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 b1 being Element of PFuncs (X,Y) holds b1 is X -defined
;
cluster -> Y -valued for Element of PFuncs (X,Y);
coherence
for b1 being Element of PFuncs (X,Y) holds b1 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 b1 being set st
( not b1 is empty & not b1 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 b1 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 b1 . (f,g) = g * f
proof end;
uniqueness
for b1, b2 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 b1 . (f,g) = g * f ) & ( for f being PartFunc of A,B
for g being PartFunc of B,C holds b2 . (f,g) = g * f ) holds
b1 = b2
proof end;
end;

:: deftheorem D1 defines PFcompos PARTPR_2:def 1 :
for A, B, C being set
for b4 being Function of [:(PFuncs (A,B)),(PFuncs (B,C)):],(PFuncs (A,C)) holds
( b4 = PFcompos (A,B,C) iff for f being PartFunc of A,B
for g being PartFunc of B,C holds b4 . (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;

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

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

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

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

:: WP: 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{ F1() -> set , F2() -> set , P1[ object ] } :
ex p being PartialPredicate of F1() st
( dom p = F2() & ( for d being object st d in dom p holds
( ( P1[d] implies p . d = TRUE ) & ( P1[d] implies p . d = FALSE ) ) ) )
provided
A1: F2() c= F1()
proof end;

scheme :: PARTPR_2:sch 2
PredToNomPredUnique{ F1() -> set , F2() -> set , P1[ object ] } :
for p, q being PartialPredicate of F1() st dom p = F2() & ( for d being object st d in dom p holds
( ( P1[d] implies p . d = TRUE ) & ( P1[d] implies p . d = FALSE ) ) ) & dom q = F2() & ( for d being object st d in dom q holds
( ( P1[d] implies q . d = TRUE ) & ( P1[d] implies q . d = FALSE ) ) ) holds
p = q
proof end;

:: WP: Emptiness checking predicate
definition
let D be set ;
defpred S1[ 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 b1 being PartialPredicate of D st
( dom b1 = D & ( for d being object st d in dom b1 holds
( ( d = {} implies b1 . d = TRUE ) & ( d <> {} implies b1 . d = FALSE ) ) ) )
proof end;
uniqueness
for b1, b2 being PartialPredicate of D st dom b1 = D & ( for d being object st d in dom b1 holds
( ( d = {} implies b1 . d = TRUE ) & ( d <> {} implies b1 . d = FALSE ) ) ) & dom b2 = D & ( for d being object st d in dom b2 holds
( ( d = {} implies b2 . d = TRUE ) & ( d <> {} implies b2 . d = FALSE ) ) ) holds
b1 = b2
proof end;
end;

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

:: WP: 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 --> {};

:: WP: 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 = {} ;

:: WP: Branching composition
definition
let D be non empty set ;
defpred S1[ object , Function, Function] means ( $1 in dom $2 & $2 . $1 = TRUE & $1 in dom $3 );
defpred S2[ object , Function, Function] means ( $1 in dom $2 & $2 . $1 = FALSE & $1 in dom $3 );
deffunc H1( Function, Function, Function) -> set = { d where d is Element of D : ( S1[d,$1,$2] or S2[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 b1 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 (b1 . (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 (b1 . (p,f,g)) . d = f . d ) & ( d in dom p & p . d = FALSE & d in dom g implies (b1 . (p,f,g)) . d = g . d ) ) ) )
proof end;
uniqueness
for b1, b2 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 (b1 . (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 (b1 . (p,f,g)) . d = f . d ) & ( d in dom p & p . d = FALSE & d in dom g implies (b1 . (p,f,g)) . d = g . d ) ) ) ) ) & ( for p being PartialPredicate of D
for f, g being BinominativeFunction of D holds
( dom (b2 . (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 (b2 . (p,f,g)) . d = f . d ) & ( d in dom p & p . d = FALSE & d in dom g implies (b2 . (p,f,g)) . d = g . d ) ) ) ) ) holds
b1 = b2
proof end;
end;

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

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

:: WP: Monotone Floyd-Hoare composition
definition
let D be non empty set ;
defpred S1[ object , Function, Function, Function] means ( ( $1 in dom $2 & $2 . $1 = FALSE ) or ( $1 in dom ($4 * $3) & ($4 * $3) . $1 = TRUE ) );
defpred S2[ object , Function, Function, Function] means ( $1 in dom $2 & $2 . $1 = TRUE & $1 in dom ($4 * $3) & ($4 * $3) . $1 = FALSE );
deffunc H1( Function, Function, Function) -> set = { d where d is Element of D : ( S1[d,$1,$2,$3] or S2[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 b1 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 (b1 . (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 (b1 . (p,f,q)) . d = TRUE ) & ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE implies (b1 . (p,f,q)) . d = FALSE ) ) ) )
proof end;
uniqueness
for b1, b2 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 (b1 . (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 (b1 . (p,f,q)) . d = TRUE ) & ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE implies (b1 . (p,f,q)) . d = FALSE ) ) ) ) ) & ( for p, q being PartialPredicate of D
for f being BinominativeFunction of D holds
( dom (b2 . (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 (b2 . (p,f,q)) . d = TRUE ) & ( d in dom p & p . d = TRUE & d in dom (q * f) & (q * f) . d = FALSE implies (b2 . (p,f,q)) . d = FALSE ) ) ) ) ) holds
b1 = b2
proof end;
end;

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

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

:: WP: Cycle composition
definition
let D be non empty set ;
defpred S1[ 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 H1( Function, Function) -> set = { d where d is Element of D : ex n being Nat st S1[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 b1 being Function of [:(Pr D),(FPrg D):],(FPrg D) st
for p being PartialPredicate of D
for f being BinominativeFunction of D holds
( dom (b1 . (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 (b1 . (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 & (b1 . (p,f)) . d = (iter (f,n)) . d ) ) )
proof end;
uniqueness
for b1, b2 being Function of [:(Pr D),(FPrg D):],(FPrg D) st ( for p being PartialPredicate of D
for f being BinominativeFunction of D holds
( dom (b1 . (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 (b1 . (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 & (b1 . (p,f)) . d = (iter (f,n)) . d ) ) ) ) & ( for p being PartialPredicate of D
for f being BinominativeFunction of D holds
( dom (b2 . (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 (b2 . (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 & (b2 . (p,f)) . d = (iter (f,n)) . d ) ) ) ) holds
b1 = b2
proof end;
end;

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

:: WP: 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 S1[ object , Function] means $1 in dom $2;
deffunc H1( 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 b1 being Function of (Pr D),(Pr D) st
for p being PartialPredicate of D holds
( dom (b1 . 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
(b1 . p) . d = TRUE ) )
proof end;
uniqueness
for b1, b2 being Function of (Pr D),(Pr D) st ( for p being PartialPredicate of D holds
( dom (b1 . p) = { 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
(b1 . p) . d = TRUE ) ) ) & ( for p being PartialPredicate of D holds
( dom (b2 . 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
(b2 . p) . d = TRUE ) ) ) holds
b1 = b2
proof end;
end;

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