begin
:: deftheorem Def1 defines even ABIAN:def 1 :
:: deftheorem defines even ABIAN:def 2 :
theorem Th1:
theorem Th2:
theorem Th3:
:: deftheorem Def3 defines is_a_fixpoint_of ABIAN:def 3 :
:: deftheorem Def4 defines is_a_fixpoint_of ABIAN:def 4 :
:: deftheorem Def5 defines has_a_fixpoint ABIAN:def 5 :
:: deftheorem Def6 defines covering ABIAN:def 6 :
theorem Th4:
theorem
definition
let E be
set ;
let f be
Function of
E,
E;
func =_ f -> Equivalence_Relation of
means :
Def7:
for
x,
y being
set st
x in E &
y in E holds
(
[x,y] in it iff ex
k,
l being
Element of
NAT st
(iter f,k) . x = (iter f,l) . y );
existence
ex b1 being Equivalence_Relation of st
for x, y being set st x in E & y in E holds
( [x,y] in b1 iff ex k, l being Element of NAT st (iter f,k) . x = (iter f,l) . y )
uniqueness
for b1, b2 being Equivalence_Relation of st ( for x, y being set st x in E & y in E holds
( [x,y] in b1 iff ex k, l being Element of NAT st (iter f,k) . x = (iter f,l) . y ) ) & ( for x, y being set st x in E & y in E holds
( [x,y] in b2 iff ex k, l being Element of NAT st (iter f,k) . x = (iter f,l) . y ) ) holds
b1 = b2
end;
:: deftheorem Def7 defines =_ ABIAN:def 7 :
theorem Th6:
theorem Th7:
theorem
begin
theorem
theorem