:: ABIAN semantic presentation

definition
let c1 be number ;
attr a1 is even means :E1: :: ABIAN:def 1
ex b1 being Integer st a1 = 2 * b1;
end;

:: deftheorem E1 defines even ABIAN:def 1 :
for b1 being number holds
( b1 is even iff ex b2 being Integer st b1 = 2 * b2 );

notation
let c1 be number ;
end;

notation
let c1 be Nat;
end;

definition
let c1 be Nat;
means :: ABIAN:def 2
ex b1 being Nat st a1 = 2 * b1;
compatibility
( c1 is even iff ex b1 being Nat st c1 = 2 * b1 )
proof
hereby
assume c1 is even ;
then consider c2 being Integer such that
E2: c1 = 2 * c2 by E1;
0 <= c1 by NAT_1:18;
then 0 <= c2 by E2, SQUARE_1:25;
then reconsider c3 = c2 as Nat by INT_1:16;
take c4 = c3;
thus c1 = 2 * c4 by E2;
end; assume ex b1 being Nat st c1 = 2 * b1 ;
hence c1 is even by E1;
end;
end;

:: deftheorem defines even ABIAN:def 2 :
for b1 being Nat holds
( b1 is even iff ex b2 being Nat st b1 = 2 * b2 );

registration
cluster even Element of NAT ;
existence
ex b1 being Nat st b1 is even
proof
take 0 ;
take 0 ; :: uses ABIAN:def 2
thus 0 = 2 * 0 ;
end;
cluster odd Element of NAT ;
existence
not for b1 being Nat holds b1 is even
proof
take 1 ;
let c1 be Nat; :: uses ABIAN:def 2
assume 1 = 2 * c1 ;
hence not verum by NAT_1:40;
end;
cluster even set ;
existence
ex b1 being Integer st b1 is even
proof
take 0 ;
take 0 ; :: uses ABIAN:def 2
thus 0 = 2 * 0 ;
end;
cluster odd set ;
existence
not for b1 being Integer holds b1 is even
proof
take 1 ;
assume 1 is even ;
then consider c1 being Integer such that
E2: 1 = 2 * c1 by E1;
thus not verum by E2, INT_1:22;
end;
end;

theorem E2: :: ABIAN:1
for b1 being Integer holds
( not ( not b1 is even & for b2 being Integer holds
not b1 = (2 * b2) + 1 ) & not ( ex b2 being Integer st b1 = (2 * b2) + 1 & b1 is even ) )
proof
let c1 be Integer;
hereby
assume E3: not c1 is even ;
assume E4: for b1 being Integer holds
c1 <> (2 * b1) + 1 ;
consider c2 being Nat such that
E5: ( c1 = c2 or c1 = - c2 ) by INT_1:8;
consider c3 being Nat such that
E6: ( c2 = 2 * c3 or c2 = (2 * c3) + 1 ) by SCHEME1:1;
per cases not ( not ( c1 = c2 & c2 = 2 * c3 ) & not ( c1 = - c2 & c2 = 2 * c3 ) & not ( c1 = c2 & c2 = (2 * c3) + 1 ) & not ( c1 = - c2 & c2 = (2 * c3) + 1 ) ) by E5, E6;
suppose ( c1 = c2 & c2 = 2 * c3 ) ;
hence not verum by E3, E1;
end;
suppose ( c1 = - c2 & c2 = 2 * c3 ) ;
then c1 = 2 * (- c3) ;
hence not verum by E3, E1;
end;
suppose ( c1 = c2 & c2 = (2 * c3) + 1 ) ;
hence not verum by E4;
end;
suppose ( c1 = - c2 & c2 = (2 * c3) + 1 ) ;
then c1 = (2 * (- (c3 + 1))) + 1 ;
hence not verum by E4;
end;
end;
end; given c2 being Integer such that E3: c1 = (2 * c2) + 1 ;
given c3 being Integer such that E4: c1 = 2 * c3 ; :: uses ABIAN:def 1
1 = (2 * c3) - (2 * c2) by E3, E4;
then 1 = 2 * (c3 - c2) ;
hence not verum by INT_1:22;
end;

registration
let c1 be Integer;
cluster 2 * a1 -> even ;
coherence
2 * c1 is even by E1;
end;

registration
let c1 be even Integer;
cluster a1 + 1 -> odd ;
coherence
not c1 + 1 is even
proof
consider c2 being Integer such that
E3: c1 = 2 * c2 by E1;
thus not c1 + 1 is even by E3, E2;
end;
end;

registration
let c1 be odd Integer;
cluster a1 + 1 -> even ;
coherence
c1 + 1 is even
proof
consider c2 being Integer such that
E3: c1 = (2 * c2) + 1 by E2;
c1 + 1 = 2 * (c2 + 1) by E3;
hence c1 + 1 is even ;
end;
end;

registration
let c1 be even Integer;
cluster a1 - 1 -> odd ;
coherence
not c1 - 1 is even
proof
consider c2 being Integer such that
E3: c1 = 2 * c2 by E1;
c1 - 1 = (2 * (c2 - 1)) + 1 by E3;
hence not c1 - 1 is even ;
end;
end;

registration
let c1 be odd Integer;
cluster a1 - 1 -> even ;
coherence
c1 - 1 is even
proof
consider c2 being Integer such that
E3: c1 = (2 * c2) + 1 by E2;
thus c1 - 1 is even by E3;
end;
end;

registration
let c1 be even Integer;
let c2 be Integer;
cluster a1 * a2 -> even ;
coherence
c1 * c2 is even
proof
consider c3 being Integer such that
E3: c1 = 2 * c3 by E1;
c1 * c2 = 2 * (c3 * c2) by E3;
hence c1 * c2 is even ;
end;
cluster a2 * a1 -> even ;
coherence
c2 * c1 is even
proof
consider c3 being Integer such that
E3: c1 = 2 * c3 by E1;
c1 * c2 = 2 * (c3 * c2) by E3;
hence c2 * c1 is even ;
end;
end;

registration
let c1, c2 be odd Integer;
cluster a1 * a2 -> odd ;
coherence
not c1 * c2 is even
proof
consider c3 being Integer such that
E3: c1 = (2 * c3) + 1 by E2;
consider c4 being Integer such that
E4: c2 = (2 * c4) + 1 by E2;
c1 * c2 = (2 * (((c3 * (2 * c4)) + (c3 * 1)) + (c4 * 1))) + 1 by E3, E4;
hence not c1 * c2 is even ;
end;
end;

registration
let c1, c2 be even Integer;
cluster a1 + a2 -> even ;
coherence
c1 + c2 is even
proof
consider c3 being Integer such that
E3: c1 = 2 * c3 by E1;
consider c4 being Integer such that
E4: c2 = 2 * c4 by E1;
c1 + c2 = 2 * (c3 + c4) by E3, E4;
hence c1 + c2 is even ;
end;
end;

registration
let c1 be even Integer;
let c2 be odd Integer;
cluster a1 + a2 -> odd ;
coherence
not c1 + c2 is even
proof
consider c3 being Integer such that
E3: c1 = 2 * c3 by E1;
consider c4 being Integer such that
E4: c2 = (2 * c4) + 1 by E2;
c1 + c2 = (2 * (c3 + c4)) + 1 by E3, E4;
hence not c1 + c2 is even ;
end;
cluster a2 + a1 -> odd ;
coherence
not c2 + c1 is even
proof
consider c3 being Integer such that
E3: c1 = 2 * c3 by E1;
consider c4 being Integer such that
E4: c2 = (2 * c4) + 1 by E2;
c2 + c1 = (2 * (c3 + c4)) + 1 by E3, E4;
hence not c2 + c1 is even ;
end;
end;

registration
let c1, c2 be odd Integer;
cluster a1 + a2 -> even ;
coherence
c1 + c2 is even
proof
consider c3 being Integer such that
E3: c1 = (2 * c3) + 1 by E2;
consider c4 being Integer such that
E4: c2 = (2 * c4) + 1 by E2;
c2 + c1 = 2 * ((c3 + c4) + 1) by E3, E4;
hence c1 + c2 is even ;
end;
end;

registration
let c1 be even Integer;
let c2 be odd Integer;
cluster a1 - a2 -> odd ;
coherence
not c1 - c2 is even
proof
consider c3 being Integer such that
E3: c1 = 2 * c3 by E1;
consider c4 being Integer such that
E4: c2 = (2 * c4) + 1 by E2;
c1 - c2 = (2 * (c3 - c4)) - 1 by E3, E4;
hence not c1 - c2 is even ;
end;
cluster a2 - a1 -> odd ;
coherence
not c2 - c1 is even
proof
consider c3 being Integer such that
E3: c1 = 2 * c3 by E1;
consider c4 being Integer such that
E4: c2 = (2 * c4) + 1 by E2;
c2 - c1 = (2 * (c4 - c3)) + 1 by E3, E4;
hence not c2 - c1 is even ;
end;
end;

registration
let c1, c2 be odd Integer;
cluster a1 - a2 -> even ;
coherence
c1 - c2 is even
proof
consider c3 being Integer such that
E3: c1 = (2 * c3) + 1 by E2;
consider c4 being Integer such that
E4: c2 = (2 * c4) + 1 by E2;
c1 - c2 = 2 * (c3 - c4) by E3, E4;
hence c1 - c2 is even ;
end;
end;

definition
let c1 be set ;
let c2 be Function of c1,c1;
let c3 be Nat;
redefine func iter as iter a2,a3 -> Function of a1,a1;
coherence
iter c2,c3 is Function of c1,c1 by FUNCT_7:85;
end;

theorem E3: :: ABIAN:2
for b1 being non empty Subset of NAT holds
( 0 in b1 implies min b1 = 0 )
proof
let c1 be non empty Subset of NAT ;
assume 0 in c1 ;
then E4: min c1 <= 0 by CQC_SIM1:def 8;
assume min c1 <> 0 ;
hence not verum by E4, NAT_1:19;
end;

theorem E4: :: ABIAN:3
for b1 being non empty set
for b2 being Function of b1,b1
for b3 being Element of b1 holds (iter b2,0) . b3 = b3
proof
let c1 be non empty set ;
let c2 be Function of c1,c1;
let c3 be Element of c1;
dom c2 = c1 by FUNCT_2:def 1;
then E5: c3 in (dom c2) \/ (rng c2) by XBOOLE_0:def 2;
thus (iter c2,0) . c3 = (id ((dom c2) \/ (rng c2))) . c3 by FUNCT_7:70
.= c3 by E5, FUNCT_1:34 ;
end;

definition
let c1 be set ;
let c2 be Function;
pred a1 is_a_fixpoint_of a2 means :E5: :: ABIAN:def 3
( a1 in dom a2 & a1 = a2 . a1 );
end;

:: deftheorem E5 defines is_a_fixpoint_of ABIAN:def 3 :
for b1 being set
for b2 being Function holds
( b1 is_a_fixpoint_of b2 iff ( b1 in dom b2 & b1 = b2 . b1 ) );

definition
let c1 be non empty set ;
let c2 be Element of c1;
let c3 be Function of c1,c1;
redefine pred is_a_fixpoint_of as a2 is_a_fixpoint_of a3 means :E6: :: ABIAN:def 4
a2 = a3 . a2;
compatibility
( c2 is_a_fixpoint_of c3 iff c2 = c3 . c2 )
proof
thus ( c2 is_a_fixpoint_of c3 implies c2 = c3 . c2 ) by E5;
assume E6: c2 = c3 . c2 ;
c2 in c1 ;
hence c2 in dom c3 by FUNCT_2:67; :: uses ABIAN:def 3
thus c2 = c3 . c2 by E6;
end;
end;

:: deftheorem E6 defines is_a_fixpoint_of ABIAN:def 4 :
for b1 being non empty set
for b2 being Element of b1
for b3 being Function of b1,b1 holds
( b2 is_a_fixpoint_of b3 iff b2 = b3 . b2 );

definition
let c1 be Function;
pred a1 has_a_fixpoint means :E7: :: ABIAN:def 5
ex b1 being set st b1 is_a_fixpoint_of a1;
end;

:: deftheorem E7 defines has_a_fixpoint ABIAN:def 5 :
for b1 being Function holds
( b1 has_a_fixpoint iff ex b2 being set st b2 is_a_fixpoint_of b1 );

notation
let c1 be Function;
end;

definition
let c1 be set ;
let c2 be Element of c1;
attr a2 is covering means :E8: :: ABIAN:def 6
 union a2 = union (union a1);
end;

:: deftheorem E8 defines covering ABIAN:def 6 :
for b1 being set
for b2 being Element of b1 holds
( b2 is covering iff union b2 = union (union b1) );

theorem E9: :: ABIAN:4
for b1 being set
for b2 being Subset-Family of b1 holds
( b2 is covering iff union b2 = b1 )
proof
let c1 be set ;
let c2 be Subset-Family of c1;
union (union (bool (bool c1))) = union (bool c1) by ZFMISC_1:99
.= c1 by ZFMISC_1:99 ;
hence ( c2 is covering iff union c2 = c1 ) by E8;
end;

registration
let c1 be set ;
cluster non empty finite covering Element of bool (bool a1);
existence
ex b1 being Subset-Family of c1 st
( not b1 is empty & b1 is finite & b1 is covering )
proof
{c1} c= bool c1 by ZFMISC_1:80;
then reconsider c2 = {c1} as Subset-Family of c1 ;
take c2 ;
thus ( not c2 is empty & c2 is finite ) ;
union c2 = c1 by ZFMISC_1:31;
hence c2 is covering by E9;
end;
end;

theorem :: ABIAN:5
for b1 being set
for b2 being Function of b1,b1
for b3 being non empty covering Subset-Family of b1 holds
not ( for b4 being Element of b3 holds b4 misses b2 .: b4 & not b2 has_no_fixpoint )
proof
let c1 be set ;
let c2 be Function of c1,c1;
let c3 be non empty covering Subset-Family of c1;
assume E10: for b1 being Element of c3 holds b1 misses c2 .: b1 ;
given c4 being set such that E11: c4 is_a_fixpoint_of c2 ; :: uses ABIAN:def 5
E12: ( c4 in dom c2 & c2 . c4 = c4 ) by E11, E5;
dom c2 = c1 by FUNCT_2:67;
then c4 in union c3 by E12, E9;
then consider c5 being set such that
E13: ( c4 in c5 & c5 in c3 ) by TARSKI:def 4;
c2 . c4 in c2 .: c5 by E12, E13, FUNCT_1:def 12;
then c5 meets c2 .: c5 by E12, E13, XBOOLE_0:3;
hence not verum by E10, E13;
end;

definition
let c1 be set ;
let c2 be Function of c1,c1;
func =_ a2 -> Equivalence_Relation of a1 means :E10: :: ABIAN:def 7
for b1, b2 being set holds
( ( b1 in a1 & b2 in a1 ) implies ( ( [b1,b2] in a3 iff ex b3, b4 being Nat st (iter a2,b3) . b1 = (iter a2,b4) . b2 ) ) );
existence
ex b1 being Equivalence_Relation of c1 st
for b2, b3 being set holds
( ( b2 in c1 & b3 in c1 ) implies ( ( [b2,b3] in b1 iff ex b4, b5 being Nat st (iter c2,b4) . b2 = (iter c2,b5) . b3 ) ) )
proof
defpred S1[ set , set ] means ( a1 in c1 & a2 in c1 & ex b1, b2 being Nat st (iter c2,b1) . a1 = (iter c2,b2) . a2 );
E10: now
let c3 be set ;
assume E11: c3 in c1 ;
(iter c2,0) . c3 = (iter c2,0) . c3 ;
hence S1[c3,c3] by E11;
end;
E11: for b1, b2 being set holds
( S1[b1,b2] implies S1[b2,b1] ) ;
E12: now
let c3, c4, c5 be set ;
assume E13: ( S1[c3,c4] & S1[c4,c5] ) ;
then consider c6, c7 being Nat such that
E14: (iter c2,c6) . c3 = (iter c2,c7) . c4 ;
consider c8, c9 being Nat such that
E15: (iter c2,c8) . c4 = (iter c2,c9) . c5 by E13;
E16: dom (iter c2,c6) = c1 by FUNCT_2:67;
E17: dom (iter c2,c7) = c1 by FUNCT_2:67;
E18: dom (iter c2,c8) = c1 by FUNCT_2:67;
E19: dom (iter c2,c9) = c1 by FUNCT_2:67;
(iter c2,(c6 + c8)) . c3 = ((iter c2,c8) * (iter c2,c6)) . c3 by FUNCT_7:79
.= (iter c2,c8) . ((iter c2,c7) . c4) by E13, E14, E16, FUNCT_1:23
.= ((iter c2,c8) * (iter c2,c7)) . c4 by E13, E17, FUNCT_1:23
.= (iter c2,(c8 + c7)) . c4 by FUNCT_7:79
.= ((iter c2,c7) * (iter c2,c8)) . c4 by FUNCT_7:79
.= (iter c2,c7) . ((iter c2,c9) . c5) by E13, E15, E18, FUNCT_1:23
.= ((iter c2,c7) * (iter c2,c9)) . c5 by E13, E19, FUNCT_1:23
.= (iter c2,(c7 + c9)) . c5 by FUNCT_7:79 ;
hence S1[c3,c5] by E13;
end;
consider c3 being Equivalence_Relation of c1 such that
E13: for b1, b2 being set holds
( [b1,b2] in c3 iff ( b1 in c1 & b2 in c1 & S1[b1,b2] ) ) from EQREL_1:sch 1(E10, E11, E12);
 take c3 ;
let c4, c5 be set ;
assume ( c4 in c1 & c5 in c1 ) ;
hence ( [c4,c5] in c3 iff ex b1, b2 being Nat st (iter c2,b1) . c4 = (iter c2,b2) . c5 ) by E13;
end;
uniqueness
for b1, b2 being Equivalence_Relation of c1 holds
( ( for b3, b4 being set holds
( ( b3 in c1 & b4 in c1 ) implies ( ( [b3,b4] in b1 iff ex b5, b6 being Nat st (iter c2,b5) . b3 = (iter c2,b6) . b4 ) ) ) & for b3, b4 being set holds
( ( b3 in c1 & b4 in c1 ) implies ( ( [b3,b4] in b2 iff ex b5, b6 being Nat st (iter c2,b5) . b3 = (iter c2,b6) . b4 ) ) ) ) implies ( b1 = b2 ) )
proof
let c3, c4 be Equivalence_Relation of c1;
assume that E10: for b1, b2 being set holds
( ( b1 in c1 & b2 in c1 ) implies ( ( [b1,b2] in c3 iff ex b3, b4 being Nat st (iter c2,b3) . b1 = (iter c2,b4) . b2 ) ) )
and E11: for b1, b2 being set holds
( ( b1 in c1 & b2 in c1 ) implies ( ( [b1,b2] in c4 iff ex b3, b4 being Nat st (iter c2,b3) . b1 = (iter c2,b4) . b2 ) ) ) ;
let c5, c6 be set ; :: uses RELAT_1:def 2
hereby
assume E12: [c5,c6] in c3 ;
then E13: ( c5 in c1 & c6 in c1 ) by ZFMISC_1:106;
then ex b1, b2 being Nat st (iter c2,b1) . c5 = (iter c2,b2) . c6 by E10, E12;
hence [c5,c6] in c4 by E11, E13;
end; assume E12: [c5,c6] in c4 ;
then E13: ( c5 in c1 & c6 in c1 ) by ZFMISC_1:106;
then ex b1, b2 being Nat st (iter c2,b1) . c5 = (iter c2,b2) . c6 by E11, E12;
hence [c5,c6] in c3 by E10, E13;
end;
end;

:: deftheorem E10 defines =_ ABIAN:def 7 :
for b1 being set
for b2 being Function of b1,b1
for b3 being Equivalence_Relation of b1 holds
( b3 = =_ b2 iff for b4, b5 being set holds
( ( b4 in b1 & b5 in b1 ) implies ( ( [b4,b5] in b3 iff ex b6, b7 being Nat st (iter b2,b6) . b4 = (iter b2,b7) . b5 ) ) ) );

theorem E11: :: ABIAN:6
for b1 being non empty set
for b2 being Function of b1,b1
for b3 being Element of Class (=_ b2)
for b4 being Element of b3 holds b2 . b4 in b3
proof
let c1 be non empty set ;
let c2 be Function of c1,c1;
let c3 be Element of Class (=_ c2);
let c4 be Element of c3;
( dom c2 = c1 & rng c2 c= c1 ) by FUNCT_2:def 1, RELSET_1:12;
then E12: c2 . c4 in (dom c2) \/ (rng c2) by XBOOLE_0:def 2;
consider c5 being set such that
E13: ( c5 in c1 & c3 = Class (=_ c2),c5 ) by EQREL_1:def 5;
E14: c3 = Class (=_ c2),c4 by E13, EQREL_1:31;
(iter c2,1) . c4 = c2 . c4 by FUNCT_7:72
.= (id ((dom c2) \/ (rng c2))) . (c2 . c4) by E12, FUNCT_1:34
.= (iter c2,0) . (c2 . c4) by FUNCT_7:70 ;
then [(c2 . c4),c4] in =_ c2 by E10;
hence c2 . c4 in c3 by E14, EQREL_1:27;
end;

theorem E12: :: ABIAN:7
for b1 being non empty set
for b2 being Function of b1,b1
for b3 being Element of Class (=_ b2)
for b4 being Element of b3
for b5 being Nat holds (iter b2,b5) . b4 in b3
proof
let c1 be non empty set ;
let c2 be Function of c1,c1;
let c3 be Element of Class (=_ c2);
let c4 be Element of c3;
let c5 be Nat;
( dom c2 = c1 & rng c2 c= c1 ) by FUNCT_2:def 1, RELSET_1:12;
then E13: (iter c2,c5) . c4 in (dom c2) \/ (rng c2) by XBOOLE_0:def 2;
consider c6 being set such that
E14: ( c6 in c1 & c3 = Class (=_ c2),c6 ) by EQREL_1:def 5;
E15: c3 = Class (=_ c2),c4 by E14, EQREL_1:31;
(iter c2,c5) . c4 = (id ((dom c2) \/ (rng c2))) . ((iter c2,c5) . c4) by E13, FUNCT_1:34
.= (iter c2,0) . ((iter c2,c5) . c4) by FUNCT_7:70 ;
then [((iter c2,c5) . c4),c4] in =_ c2 by E10;
hence (iter c2,c5) . c4 in c3 by E15, EQREL_1:27;
end;

registration
cluster empty-membered -> trivial set ;
coherence
for b1 being set holds
( b1 is empty-membered implies b1 is trivial )
proof
let c1 be set ;
assume E13: c1 is empty-membered ;
assume not c1 is empty ; :: uses REALSET1:def 4
then consider c2 being set such that
E14: c2 in c1 by XBOOLE_0:def 1;
E15: c2 is empty by E14, SETFAM_1:def 11, E13;
take c2 ;
thus c1 c= {c2} :: uses XBOOLE_0:def 10
proof
let c3 be set ; :: uses TARSKI:def 3
assume c3 in c1 ;
then c3 is empty by E13, SETFAM_1:def 11;
then c2 = c3 by E15;
hence c3 in {c2} by TARSKI:def 1;
end;
thus {c2} c= c1 by E14, ZFMISC_1:37;
end;
end;

registration
let c1 be set ;
let c2 be with_non-empty_element set ;
cluster non-empty M4(a1,a2);
existence
ex b1 being Function of c1,c2 st b1 is non-empty
proof
consider c3 being non empty set such that
E13: c3 in c2 by SETFAM_1:def 11;
reconsider c4 = c1 --> c3 as Function of c1,c2 by E13, FUNCOP_1:57;
take c4 ;
let c5 be set ; :: uses FUNCT_1:def 15
assume c5 in dom c4 ;
then c5 in c1 by FUNCOP_1:19;
hence not c4 . c5 is empty by FUNCOP_1:13;
end;
end;

registration
let c1 be non empty set ;
let c2 be with_non-empty_element set ;
let c3 be non-empty Function of c1,c2;
let c4 be Element of c1;
cluster a3 . a4 -> non empty ;
coherence
not c3 . c4 is empty
proof
dom c3 = c1 by FUNCT_2:def 1;
then c3 . c4 in rng c3 by FUNCT_1:def 5;
hence not c3 . c4 is empty by SETFAM_1:def 9;
end;
end;

registration
let c1 be non empty set ;
cluster bool a1 -> with_non-empty_element ;
coherence
not bool c1 is empty-membered
proof
take c1 ; :: uses SETFAM_1:def 11
thus c1 in bool c1 by ZFMISC_1:def 1;
end;
end;

theorem :: ABIAN:8
for b1 being non empty set
for b2 being Function of b1,b1 holds
not ( b2 has_no_fixpoint & for b3, b4, b5 being set holds
not ( (b3 \/ b4) \/ b5 = b1 & b2 .: b3 misses b3 & b2 .: b4 misses b4 & b2 .: b5 misses b5 ) )
proof
let c1 be non empty set ;
let c2 be Function of c1,c1;
assume E13: c2 has_no_fixpoint ;
defpred S1[ Element of Class (=_ c2), Element of [:(bool c1),(bool c1),(bool c1):]] means ( ((a2 `1 ) \/ (a2 `2 )) \/ (a2 `3 ) = a1 & c2 .: (a2 `1 ) misses a2 `1 & c2 .: (a2 `2 ) misses a2 `2 & c2 .: (a2 `3 ) misses a2 `3 );
deffunc H1( Nat) -> Function of c1,c1 = iter c2,a1;
E14: for b1 being Element of Class (=_ c2) holds
ex b2 being Element of [:(bool c1),(bool c1),(bool c1):] st
S1[b1,b2]
proof
let c3 be Element of Class (=_ c2);
consider c4 being set such that
E15: ( c4 in c1 & c3 = Class (=_ c2),c4 ) by EQREL_1:def 5;
reconsider c5 = c4 as Element of c3 by E15, EQREL_1:28;
defpred S2[ set ] means ex b1, b2 being Nat st
( H1(b1) . a1 = H1(b2) . c5 & b1 is even & b2 is even );
set c6 = { b1 where B is Element of c3 : S2[b1] } ;
{ b1 where B is Element of c3 : S2[b1] } is Subset of c3 from DOMAIN_1:sch 7();
 then reconsider c7 = { b1 where B is Element of c3 : S2[b1] } as Subset of c1 by XBOOLE_1:1;
defpred S3[ set ] means ex b1, b2 being Nat st
( H1(b1) . a1 = H1(b2) . c5 & not b1 is even & b2 is even );
set c8 = { b1 where B is Element of c3 : S3[b1] } ;
{ b1 where B is Element of c3 : S3[b1] } is Subset of c3 from DOMAIN_1:sch 7();
 then reconsider c9 = { b1 where B is Element of c3 : S3[b1] } as Subset of c1 by XBOOLE_1:1;
reconsider c10 = {} as Subset of c1 by XBOOLE_1:2;
per cases not ( not c7 misses c9 & not c7 meets c9 ) ;
suppose E16: c7 misses c9 ;
take c11 = [c7,c9,c10];
E17: ( c11 `1 = c7 & c11 `2 = c9 & c11 `3 = c10 ) by MCART_1:47;
thus ((c11 `1 ) \/ (c11 `2 )) \/ (c11 `3 ) = c3
proof
hereby :: uses TARSKI:def 3,XBOOLE_0:def 10
let c12 be set ;
assume E18: c12 in ((c11 `1 ) \/ (c11 `2 )) \/ (c11 `3 ) ;
per cases not ( not c12 in c7 & not c12 in c9 & not c12 in c10 ) by E17, E18, XBOOLE_0:def 2;
suppose c12 in c7 ;
then consider c13 being Element of c3 such that
E19: ( c12 = c13 & ex b1, b2 being Nat st
( H1(b1) . c13 = H1(b2) . c5 & b1 is even & b2 is even ) ) ;
thus c12 in c3 by E19;
end;
suppose c12 in c9 ;
then consider c13 being Element of c3 such that
E19: ( c12 = c13 & ex b1, b2 being Nat st
( H1(b1) . c13 = H1(b2) . c5 & not b1 is even & b2 is even ) ) ;
thus c12 in c3 by E19;
end;
suppose c12 in c10 ;
hence c12 in c3 ;
end;
end;
end; let c12 be set ; :: uses TARSKI:def 3
assume c12 in c3 ;
then reconsider c13 = c12 as Element of c3 ;
[c13,c5] in =_ c2 by E15, EQREL_1:27;
then consider c14, c15 being Nat such that
E18: H1(c14) . c13 = H1(c15) . c5 by E10;
E19: ( dom H1(c14) = c1 & dom H1(c15) = c1 ) by FUNCT_2:def 1;
per cases not ( not c14 is even & c14 is even ) ;
suppose E20: c14 is even ;
then reconsider c16 = c14 as even Nat ;
thus c12 in ((c11 `1 ) \/ (c11 `2 )) \/ (c11 `3 )
proof
per cases not ( not c15 is even & c15 is even ) ;
suppose c15 is even ;
then c13 in c7 by E18, E20;
hence c12 in ((c11 `1 ) \/ (c11 `2 )) \/ (c11 `3 ) by E17, XBOOLE_0:def 2;
end;
suppose not c15 is even ;
then reconsider c17 = c15 as odd Nat ;
H1(c16 + 1) . c13 = (c2 * H1(c16)) . c13 by FUNCT_7:73
.= c2 . (H1(c17) . c5) by E18, E19, FUNCT_1:23
.= (c2 * H1(c17)) . c5 by E19, FUNCT_1:23
.= H1(c17 + 1) . c5 by FUNCT_7:73 ;
then c13 in c9 ;
hence c12 in ((c11 `1 ) \/ (c11 `2 )) \/ (c11 `3 ) by E17, XBOOLE_0:def 2;
end;
end;
end;
end;
suppose E20: not c14 is even ;
then reconsider c16 = c14 as odd Nat ;
thus c12 in ((c11 `1 ) \/ (c11 `2 )) \/ (c11 `3 )
proof
per cases not ( not c15 is even & c15 is even ) ;
suppose c15 is even ;
then c13 in c9 by E18, E20;
hence c12 in ((c11 `1 ) \/ (c11 `2 )) \/ (c11 `3 ) by E17, XBOOLE_0:def 2;
end;
suppose not c15 is even ;
then reconsider c17 = c15 as odd Nat ;
H1(c16 + 1) . c13 = (c2 * H1(c16)) . c13 by FUNCT_7:73
.= c2 . (H1(c17) . c5) by E18, E19, FUNCT_1:23
.= (c2 * H1(c17)) . c5 by E19, FUNCT_1:23
.= H1(c17 + 1) . c5 by FUNCT_7:73 ;
then c13 in c7 ;
hence c12 in ((c11 `1 ) \/ (c11 `2 )) \/ (c11 `3 ) by E17, XBOOLE_0:def 2;
end;
end;
end;
end;
end;
end;
thus c2 .: (c11 `1 ) misses c11 `1
proof
c2 .: c7 c= c9
proof
let c12 be set ; :: uses TARSKI:def 3
assume c12 in c2 .: c7 ;
then consider c13 being set such that
E18: ( c13 in dom c2 & c13 in c7 & c12 = c2 . c13 ) by FUNCT_1:def 12;
consider c14 being Element of c3 such that
E19: ( c13 = c14 & ex b1, b2 being Nat st
( H1(b1) . c14 = H1(b2) . c5 & b1 is even & b2 is even ) ) by E18;
reconsider c15 = c12 as Element of c3 by E18, E19, E11;
consider c16, c17 being Nat such that
E20: ( H1(c16) . c14 = H1(c17) . c5 & c16 is even & c17 is even ) by E19;
reconsider c18 = c16, c19 = c17 as even Nat by E20;
reconsider c20 = c18 + 1 as odd Nat ;
reconsider c21 = c19 + 1 as odd Nat ;
reconsider c22 = c21 + 1 as even Nat ;
E21: ( dom c2 = c1 & dom H1(c18) = c1 & dom H1(c19) = c1 & dom H1(c20) = c1 & dom H1(c21) = c1 ) by FUNCT_2:def 1;
E22: H1(c20 + 1) . c14 = (H1(c20) * c2) . c14 by FUNCT_7:71
.= H1(c20) . (c2 . c14) by E21, FUNCT_1:23 ;
H1(c20 + 1) . c14 = (c2 * H1(c20)) . c14 by FUNCT_7:73
.= c2 . (H1(c20) . c14) by E21, FUNCT_1:23
.= c2 . ((c2 * H1(c18)) . c14) by FUNCT_7:73
.= c2 . (c2 . (H1(c19) . c5)) by E20, E21, FUNCT_1:23
.= c2 . ((c2 * H1(c19)) . c5) by E21, FUNCT_1:23
.= c2 . (H1(c21) . c5) by FUNCT_7:73
.= (c2 * H1(c21)) . c5 by E21, FUNCT_1:23
.= H1(c22) . c5 by FUNCT_7:73 ;
then c15 in c9 by E18, E19, E22;
hence c12 in c9 ;
end;
hence c2 .: (c11 `1 ) misses c11 `1 by E16, E17, XBOOLE_1:63;
end;
thus c2 .: (c11 `2 ) misses c11 `2
proof
c2 .: c9 c= c7
proof
let c12 be set ; :: uses TARSKI:def 3
assume c12 in c2 .: c9 ;
then consider c13 being set such that
E18: ( c13 in dom c2 & c13 in c9 & c12 = c2 . c13 ) by FUNCT_1:def 12;
consider c14 being Element of c3 such that
E19: ( c13 = c14 & ex b1, b2 being Nat st
( H1(b1) . c14 = H1(b2) . c5 & not b1 is even & b2 is even ) ) by E18;
reconsider c15 = c12 as Element of c3 by E18, E19, E11;
consider c16, c17 being Nat such that
E20: ( H1(c16) . c14 = H1(c17) . c5 & not c16 is even & c17 is even ) by E19;
reconsider c18 = c16 as odd Nat by E20;
reconsider c19 = c17 as even Nat by E20;
reconsider c20 = c18 + 1 as even Nat ;
reconsider c21 = c19 + 1 as odd Nat ;
reconsider c22 = c21 + 1 as even Nat ;
E21: ( dom c2 = c1 & dom H1(c18) = c1 & dom H1(c19) = c1 & dom H1(c20) = c1 & dom H1(c21) = c1 ) by FUNCT_2:def 1;
E22: H1(c20 + 1) . c14 = (H1(c20) * c2) . c14 by FUNCT_7:71
.= H1(c20) . (c2 . c14) by E21, FUNCT_1:23 ;
H1(c20 + 1) . c14 = (c2 * H1(c20)) . c14 by FUNCT_7:73
.= c2 . (H1(c20) . c14) by E21, FUNCT_1:23
.= c2 . ((c2 * H1(c18)) . c14) by FUNCT_7:73
.= c2 . (c2 . (H1(c19) . c5)) by E20, E21, FUNCT_1:23
.= c2 . ((c2 * H1(c19)) . c5) by E21, FUNCT_1:23
.= c2 .