:: On algebras of algorithms and specifications over uninterpreted data
:: by Ievgen Ivanov , Artur Korni{\l}owicz and Mykola Nikitchenko
::
:: Copyright (c) 2018-2019 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 () 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;

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;

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):];
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);
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
() . (f,g);
coherence
() . (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) = () . (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
() . (f,p);
coherence
() . (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) = () . (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;

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

:: 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
() . (p,f);
coherence
() . (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) = () . (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
() . p;
coherence
() . 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 = () . 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 () )
proof end;

theorem :: PARTPR_2:10
for D being non empty set
for p being PartialPredicate of D st p is total holds
dom () = {}
proof end;