CONAFFM

definition

let X be ( ( V41() OrtAfPl-like ) ( V41() OrtAfSp-like OrtAfPl-like ) OrtAfPl) ;

attr X is satisfying_DES means :: CONAFFM:def 1
for o, a, a1, b, b1, c, c1 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> b1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> c1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & not LIN b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & not LIN a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & LIN o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & LIN o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & LIN o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) // a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) // a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) // b1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;

attr X is satisfying_AH means :: CONAFFM:def 2
for o, a, a1, b, b1, c, c1 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) _|_ o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) _|_ o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) _|_ o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) _|_ a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) _|_ a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & not o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & not o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) _|_ b1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;

attr X is satisfying_3H means :: CONAFFM:def 3
for a, b, c being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st not LIN a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
ex d being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) _|_ b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) _|_ a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & d : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) _|_ a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) );

attr X is satisfying_ODES means :: CONAFFM:def 4
for o, a, a1, b, b1, c, c1 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) _|_ o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) _|_ o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) _|_ o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) _|_ a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) _|_ a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & not o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & not o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) // o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) _|_ b1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;

attr X is satisfying_LIN means :: CONAFFM:def 5
for o, a, a1, b, b1, c, c1 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> b1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> c1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) _|_ o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) _|_ o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) _|_ o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & not LIN o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & LIN o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & LIN o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) _|_ a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) _|_ b1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;

attr X is satisfying_LIN1 means :: CONAFFM:def 6
for o, a, a1, b, b1, c, c1 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> b1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> c1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) _|_ o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) _|_ o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) _|_ o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & not LIN o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & LIN o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & LIN o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) _|_ a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) _|_ b1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;

attr X is satisfying_LIN2 means :: CONAFFM:def 7
for o, a, a1, b, b1, c, c1 being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> b1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> c1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) // b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) _|_ o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) _|_ o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & not LIN o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & LIN o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & LIN o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,b1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) _|_ a1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) _|_ b1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( ) set ) ) _|_ o : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ,c1 : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;

end;