:: CONAFFM semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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

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

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

:: deftheorem defines satisfying_3H CONAFFM:def 3 :
for X being OrtAfPl holds
( X is satisfying_3H iff for a, b, c being Element of X st not LIN a,b,c holds
ex d being Element of X st
( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b ) );

:: deftheorem Def4 defines satisfying_ODES CONAFFM:def 4 :
for X being OrtAfPl holds
( X is satisfying_ODES iff for o, a, a1, b, b1, c, c1 being Element of X st o,a _|_ o,a1 & o,b _|_ o,b1 & o,c _|_ o,c1 & a,b _|_ a1,b1 & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b holds
b,c _|_ b1,c1 );

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

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

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

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

theorem :: CONAFFM:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being OrtAfPl st ODES_holds_in X holds
DES_holds_in X
proof end;

theorem :: CONAFFM:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being OrtAfPl st ODES_holds_in X holds
AH_holds_in X
proof end;

theorem Th3: :: CONAFFM:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being OrtAfPl st LIN_holds_in X holds
LIN1_holds_in X
proof end;

theorem :: CONAFFM:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being OrtAfPl st LIN1_holds_in X holds
LIN2_holds_in X
proof end;

theorem :: CONAFFM:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being OrtAfPl st LIN_holds_in X holds
ODES_holds_in X
proof end;

theorem :: CONAFFM:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being OrtAfPl st LIN_holds_in X holds
3H_holds_in X
proof end;