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

theorem Th1: :: PARDEPAP:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for SAS being AffinPlane st SAS satisfies_PAP holds
for a1, a2, a3, b1, b2, b3 being Element of SAS st a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2 holds
a3,b1 // a1,b3
proof end;

theorem Th2: :: PARDEPAP:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for SAS being AffinPlane st SAS satisfies_DES holds
for o, a, a', b, b', c, c' being Element of SAS st not o,a // o,b & not o,a // o,c & o,a // o,a' & o,b // o,b' & o,c // o,c' & a,b // a',b' & a,c // a',c' holds
b,c // b',c'
proof end;

theorem Th3: :: PARDEPAP:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for SAS being AffinPlane st SAS satisfies_des holds
for a, a', b, b', c, c' being Element of SAS st not a,a' // a,b & not a,a' // a,c & a,a' // b,b' & a,a' // c,c' & a,b // a',b' & a,c // a',c' holds
b,c // b',c'
proof end;

theorem :: PARDEPAP:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PARDEPAP:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
ex SAS being AffinPlane st
( ( for o, a, a', b, b', c, c' being Element of SAS st not o,a // o,b & not o,a // o,c & o,a // o,a' & o,b // o,b' & o,c // o,c' & a,b // a',b' & a,c // a',c' holds
b,c // b',c' ) & ( for a, a', b, b', c, c' being Element of SAS st not a,a' // a,b & not a,a' // a,c & a,a' // b,b' & a,a' // c,c' & a,b // a',b' & a,c // a',c' holds
b,c // b',c' ) & ( for a1, a2, a3, b1, b2, b3 being Element of SAS st a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2 holds
a3,b1 // a1,b3 ) & ( for a, b, c, d being Element of SAS st not a,b // a,c & a,b // c,d & a,c // b,d holds
not a,d // b,c ) )
proof end;

theorem :: PARDEPAP:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for SAS being AffinPlane
for o, a being Element of SAS ex p being Element of SAS st
for b, c being Element of SAS holds
( o,a // o,p & ex d being Element of SAS st
( o,p // o,b implies ( o,c // o,d & p,c // b,d ) ) )
proof end;