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