:: CONAFFM semantic presentation

definition
let c1 be OrtAfPl;
attr a1 is satisfying_DES means :: CONAFFM:def 1
for b1, b2, b3, b4, b5, b6, b7 being Element of a1 st b1 <> b2 & b1 <> b3 & b1 <> b4 & b1 <> b5 & b1 <> b6 & b1 <> b7 & not LIN b4,b5,b2 & not LIN b2,b3,b6 & LIN b1,b2,b3 & LIN b1,b4,b5 & LIN b1,b6,b7 & b2,b4 // b3,b5 & b2,b6 // b3,b7 holds
b4,b6 // b5,b7;
attr a1 is satisfying_AH means :: CONAFFM:def 2
for b1, b2, b3, b4, b5, b6, b7 being Element of a1 st b1,b2 _|_ b1,b3 & b1,b4 _|_ b1,b5 & b1,b6 _|_ b1,b7 & b2,b4 _|_ b3,b5 & b1,b2 // b4,b6 & b2,b6 _|_ b3,b7 & not b1,b6 // b1,b2 & not b1,b2 // b1,b4 holds
b4,b6 _|_ b5,b7;
attr a1 is satisfying_3H means :: CONAFFM:def 3
for b1, b2, b3 being Element of a1 st not LIN b1,b2,b3 holds
ex b4 being Element of a1 st
( b4,b1 _|_ b2,b3 & b4,b2 _|_ b1,b3 & b4,b3 _|_ b1,b2 );
attr a1 is satisfying_ODES means :Def4: :: CONAFFM:def 4
for b1, b2, b3, b4, b5, b6, b7 being Element of a1 st b1,b2 _|_ b1,b3 & b1,b4 _|_ b1,b5 & b1,b6 _|_ b1,b7 & b2,b4 _|_ b3,b5 & b2,b6 _|_ b3,b7 & not b1,b6 // b1,b2 & not b1,b2 // b1,b4 holds
b4,b6 _|_ b5,b7;
attr a1 is satisfying_LIN means :Def5: :: CONAFFM:def 5
for b1, b2, b3, b4, b5, b6, b7 being Element of a1 st b1 <> b2 & b1 <> b3 & b1 <> b4 & b1 <> b5 & b1 <> b6 & b1 <> b7 & b2 <> b4 & b1,b6 _|_ b1,b7 & b1,b2 _|_ b1,b3 & b1,b4 _|_ b1,b5 & not LIN b1,b6,b2 & LIN b1,b2,b4 & LIN b1,b3,b5 & b2,b6 _|_ b3,b7 & b4,b6 _|_ b5,b7 holds
b2,b3 // b4,b5;
attr a1 is satisfying_LIN1 means :Def6: :: CONAFFM:def 6
for b1, b2, b3, b4, b5, b6, b7 being Element of a1 st b1 <> b2 & b1 <> b3 & b1 <> b4 & b1 <> b5 & b1 <> b6 & b1 <> b7 & b2 <> b4 & b1,b6 _|_ b1,b7 & b1,b2 _|_ b1,b3 & b1,b4 _|_ b1,b5 & not LIN b1,b6,b2 & LIN b1,b2,b4 & LIN b1,b3,b5 & b2,b6 _|_ b3,b7 & b2,b3 // b4,b5 holds
b4,b6 _|_ b5,b7;
attr a1 is satisfying_LIN2 means :: CONAFFM:def 7
for b1, b2, b3, b4, b5, b6, b7 being Element of a1 st b1 <> b2 & b1 <> b3 & b1 <> b4 & b1 <> b5 & b1 <> b6 & b1 <> b7 & b2 <> b4 & b2,b3 // b4,b5 & b1,b2 _|_ b1,b3 & b1,b4 _|_ b1,b5 & not LIN b1,b6,b2 & LIN b1,b2,b4 & LIN b1,b3,b5 & b2,b6 _|_ b3,b7 & b4,b6 _|_ b5,b7 holds
b1,b6 _|_ b1,b7;
end;

:: deftheorem Def1 defines satisfying_DES CONAFFM:def 1 :
for b1 being OrtAfPl holds
( b1 is satisfying_DES iff for b2, b3, b4, b5, b6, b7, b8 being Element of b1 st b2 <> b3 & b2 <> b4 & b2 <> b5 & b2 <> b6 & b2 <> b7 & b2 <> b8 & not LIN b5,b6,b3 & not LIN b3,b4,b7 & LIN b2,b3,b4 & LIN b2,b5,b6 & LIN b2,b7,b8 & b3,b5 // b4,b6 & b3,b7 // b4,b8 holds
b5,b7 // b6,b8 );

:: deftheorem Def2 defines satisfying_AH CONAFFM:def 2 :
for b1 being OrtAfPl holds
( b1 is satisfying_AH iff for b2, b3, b4, b5, b6, b7, b8 being Element of b1 st b2,b3 _|_ b2,b4 & b2,b5 _|_ b2,b6 & b2,b7 _|_ b2,b8 & b3,b5 _|_ b4,b6 & b2,b3 // b5,b7 & b3,b7 _|_ b4,b8 & not b2,b7 // b2,b3 & not b2,b3 // b2,b5 holds
b5,b7 _|_ b6,b8 );

:: deftheorem Def3 defines satisfying_3H CONAFFM:def 3 :
for b1 being OrtAfPl holds
( b1 is satisfying_3H iff for b2, b3, b4 being Element of b1 st not LIN b2,b3,b4 holds
ex b5 being Element of b1 st
( b5,b2 _|_ b3,b4 & b5,b3 _|_ b2,b4 & b5,b4 _|_ b2,b3 ) );

:: deftheorem Def4 defines satisfying_ODES CONAFFM:def 4 :
for b1 being OrtAfPl holds
( b1 is satisfying_ODES iff for b2, b3, b4, b5, b6, b7, b8 being Element of b1 st b2,b3 _|_ b2,b4 & b2,b5 _|_ b2,b6 & b2,b7 _|_ b2,b8 & b3,b5 _|_ b4,b6 & b3,b7 _|_ b4,b8 & not b2,b7 // b2,b3 & not b2,b3 // b2,b5 holds
b5,b7 _|_ b6,b8 );

:: deftheorem Def5 defines satisfying_LIN CONAFFM:def 5 :
for b1 being OrtAfPl holds
( b1 is satisfying_LIN iff for b2, b3, b4, b5, b6, b7, b8 being Element of b1 st b2 <> b3 & b2 <> b4 & b2 <> b5 & b2 <> b6 & b2 <> b7 & b2 <> b8 & b3 <> b5 & b2,b7 _|_ b2,b8 & b2,b3 _|_ b2,b4 & b2,b5 _|_ b2,b6 & not LIN b2,b7,b3 & LIN b2,b3,b5 & LIN b2,b4,b6 & b3,b7 _|_ b4,b8 & b5,b7 _|_ b6,b8 holds
b3,b4 // b5,b6 );

:: deftheorem Def6 defines satisfying_LIN1 CONAFFM:def 6 :
for b1 being OrtAfPl holds
( b1 is satisfying_LIN1 iff for b2, b3, b4, b5, b6, b7, b8 being Element of b1 st b2 <> b3 & b2 <> b4 & b2 <> b5 & b2 <> b6 & b2 <> b7 & b2 <> b8 & b3 <> b5 & b2,b7 _|_ b2,b8 & b2,b3 _|_ b2,b4 & b2,b5 _|_ b2,b6 & not LIN b2,b7,b3 & LIN b2,b3,b5 & LIN b2,b4,b6 & b3,b7 _|_ b4,b8 & b3,b4 // b5,b6 holds
b5,b7 _|_ b6,b8 );

:: deftheorem Def7 defines satisfying_LIN2 CONAFFM:def 7 :
for b1 being OrtAfPl holds
( b1 is satisfying_LIN2 iff for b2, b3, b4, b5, b6, b7, b8 being Element of b1 st b2 <> b3 & b2 <> b4 & b2 <> b5 & b2 <> b6 & b2 <> b7 & b2 <> b8 & b3 <> b5 & b3,b4 // b5,b6 & b2,b3 _|_ b2,b4 & b2,b5 _|_ b2,b6 & not LIN b2,b7,b3 & LIN b2,b3,b5 & LIN b2,b4,b6 & b3,b7 _|_ b4,b8 & b5,b7 _|_ b6,b8 holds
b2,b7 _|_ b2,b8 );

notation
let c1 be OrtAfPl;
synonym DES_holds_in c1 for satisfying_DES c1;
synonym AH_holds_in c1 for satisfying_AH c1;
synonym 3H_holds_in c1 for satisfying_3H c1;
synonym ODES_holds_in c1 for satisfying_ODES c1;
synonym LIN_holds_in c1 for satisfying_LIN c1;
synonym LIN1_holds_in c1 for satisfying_LIN1 c1;
synonym LIN2_holds_in c1 for satisfying_LIN2 c1;
end;

theorem Th1: :: CONAFFM:1
for b1 being OrtAfPl st ODES_holds_in b1 holds
DES_holds_in b1
proof end;

theorem Th2: :: CONAFFM:2
for b1 being OrtAfPl st ODES_holds_in b1 holds
AH_holds_in b1
proof end;

theorem Th3: :: CONAFFM:3
for b1 being OrtAfPl st LIN_holds_in b1 holds
LIN1_holds_in b1
proof end;

theorem Th4: :: CONAFFM:4
for b1 being OrtAfPl st LIN1_holds_in b1 holds
LIN2_holds_in b1
proof end;

theorem Th5: :: CONAFFM:5
for b1 being OrtAfPl st LIN_holds_in b1 holds
ODES_holds_in b1
proof end;

theorem Th6: :: CONAFFM:6
for b1 being OrtAfPl st LIN_holds_in b1 holds
3H_holds_in b1
proof end;