:: CONMETR 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_OPAP means :Def1: :: CONMETR:def 1
for o, a1, a2, a3, b1, b2, b3 being Element of X
for M, N being Subset of X st o in M & a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N & M _|_ N & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 holds
a1,b2 // a2,b3;
attr X is satisfying_PAP means :: CONMETR:def 2
for o, a1, a2, a3, b1, b2, b3 being Element of X
for M, N being Subset of X st M is_line & N is_line & o in M & a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 holds
a1,b2 // a2,b3;
attr X is satisfying_MH1 means :Def3: :: CONMETR:def 3
for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X
for M, N being Subset of X st M _|_ N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a2 in M & not a4 in M & a1,a2 _|_ b1,b2 & a2,a3 _|_ b2,b3 & a3,a4 _|_ b3,b4 holds
a1,a4 _|_ b1,b4;
attr X is satisfying_MH2 means :Def4: :: CONMETR:def 4
for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X
for M, N being Subset of X st M _|_ N & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a2 in M & not a4 in M & a1,a2 _|_ b1,b2 & a2,a3 _|_ b2,b3 & a3,a4 _|_ b3,b4 holds
a1,a4 _|_ b1,b4;
attr X is satisfying_TDES means :Def5: :: CONMETR: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 & not LIN b,b1,a & not LIN b,b1,c & LIN o,a,a1 & LIN o,b,b1 & LIN o,c,c1 & a,b // a1,b1 & a,b // o,c & b,c // b1,c1 holds
a,c // a1,c1;
attr X is satisfying_SCH means :: CONMETR:def 6
for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X
for M, N being Subset of X st M is_line & N is_line & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds
a3,a4 // b3,b4;
attr X is satisfying_OSCH means :Def7: :: CONMETR:def 7
for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X
for M, N being Subset of X st M _|_ N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds
a3,a4 // b3,b4;
attr X is satisfying_des means :Def8: :: CONMETR:def 8
for a, a1, b, b1, c, c1 being Element of X st not LIN a,a1,b & not LIN a,a1,c & a,a1 // b,b1 & a,a1 // c,c1 & a,b // a1,b1 & a,c // a1,c1 holds
b,c // b1,c1;
end;

:: deftheorem Def1 defines satisfying_OPAP CONMETR:def 1 :
for X being OrtAfPl holds
( X is satisfying_OPAP iff for o, a1, a2, a3, b1, b2, b3 being Element of X
for M, N being Subset of X st o in M & a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N & M _|_ N & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 holds
a1,b2 // a2,b3 );

:: deftheorem defines satisfying_PAP CONMETR:def 2 :
for X being OrtAfPl holds
( X is satisfying_PAP iff for o, a1, a2, a3, b1, b2, b3 being Element of X
for M, N being Subset of X st M is_line & N is_line & o in M & a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 holds
a1,b2 // a2,b3 );

:: deftheorem Def3 defines satisfying_MH1 CONMETR:def 3 :
for X being OrtAfPl holds
( X is satisfying_MH1 iff for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X
for M, N being Subset of X st M _|_ N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a2 in M & not a4 in M & a1,a2 _|_ b1,b2 & a2,a3 _|_ b2,b3 & a3,a4 _|_ b3,b4 holds
a1,a4 _|_ b1,b4 );

:: deftheorem Def4 defines satisfying_MH2 CONMETR:def 4 :
for X being OrtAfPl holds
( X is satisfying_MH2 iff for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X
for M, N being Subset of X st M _|_ N & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a2 in M & not a4 in M & a1,a2 _|_ b1,b2 & a2,a3 _|_ b2,b3 & a3,a4 _|_ b3,b4 holds
a1,a4 _|_ b1,b4 );

:: deftheorem Def5 defines satisfying_TDES CONMETR:def 5 :
for X being OrtAfPl holds
( X is satisfying_TDES 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 b,b1,c & LIN o,a,a1 & LIN o,b,b1 & LIN o,c,c1 & a,b // a1,b1 & a,b // o,c & b,c // b1,c1 holds
a,c // a1,c1 );

:: deftheorem defines satisfying_SCH CONMETR:def 6 :
for X being OrtAfPl holds
( X is satisfying_SCH iff for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X
for M, N being Subset of X st M is_line & N is_line & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds
a3,a4 // b3,b4 );

:: deftheorem Def7 defines satisfying_OSCH CONMETR:def 7 :
for X being OrtAfPl holds
( X is satisfying_OSCH iff for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X
for M, N being Subset of X st M _|_ N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds
a3,a4 // b3,b4 );

:: deftheorem Def8 defines satisfying_des CONMETR:def 8 :
for X being OrtAfPl holds
( X is satisfying_des iff for a, a1, b, b1, c, c1 being Element of X st not LIN a,a1,b & not LIN a,a1,c & a,a1 // b,b1 & a,a1 // c,c1 & a,b // a1,b1 & a,c // a1,c1 holds
b,c // b1,c1 );

notation
let X be OrtAfPl;
synonym OPAP_holds_in X for satisfying_OPAP X;
synonym PAP_holds_in X for satisfying_PAP X;
synonym MH1_holds_in X for satisfying_MH1 X;
synonym MH2_holds_in X for satisfying_MH2 X;
synonym TDES_holds_in X for satisfying_TDES X;
synonym SCH_holds_in X for satisfying_SCH X;
synonym OSCH_holds_in X for satisfying_OSCH X;
synonym des_holds_in X for satisfying_des X;
end;

theorem Th1: :: CONMETR: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 ex a, b, c being Element of X st
( LIN a,b,c & a <> b & b <> c & c <> a )
proof end;

theorem Th2: :: CONMETR: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
for a, b being Element of X st a <> b holds
ex c being Element of X st
( LIN a,b,c & a <> c & b <> c )
proof end;

theorem Th3: :: CONMETR: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
for A being Subset of X
for a being Element of X st A is_line holds
ex K being Subset of X st
( a in K & A _|_ K )
proof end;

theorem Th4: :: CONMETR: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
for a, b, c being Element of X
for A being Subset of X st A is_line & a in A & b in A & c in A holds
LIN a,b,c
proof end;

theorem Th5: :: CONMETR: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
for a, b being Element of X
for A, M being Subset of X st A is_line & M is_line & a in A & b in A & a in M & b in M & not a = b holds
A = M
proof end;

theorem Th6: :: CONMETR: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
for a, b, c, d being Element of X
for M being Subset of X
for M' being Subset of (Af X)
for c', d' being Element of (Af X) st c = c' & d = d' & M = M' & a in M & b in M & c',d' // M' holds
c,d // a,b
proof end;

theorem Th7: :: CONMETR:7  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 TDES_holds_in X holds
Af X satisfies_TDES
proof end;

theorem Th8: :: CONMETR:8  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 Af X satisfies_des holds
des_holds_in X
proof end;

theorem :: CONMETR:9  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 MH1_holds_in X holds
OSCH_holds_in X
proof end;

theorem :: CONMETR:10  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 MH2_holds_in X holds
OSCH_holds_in X
proof end;

theorem :: CONMETR:11  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 AH_holds_in X holds
TDES_holds_in X
proof end;

theorem :: CONMETR:12  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 OSCH_holds_in X & TDES_holds_in X holds
SCH_holds_in X
proof end;

theorem :: CONMETR:13  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 OPAP_holds_in X & DES_holds_in X holds
PAP_holds_in X
proof end;

theorem :: CONMETR:14  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 MH1_holds_in X & MH2_holds_in X holds
OPAP_holds_in X
proof end;

theorem :: CONMETR:15  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 3H_holds_in X holds
OPAP_holds_in X
proof end;