File Search Catalog Content Search
» » » » » core-2.1.1.tgz » Content »

core…  more info»

```************************************************************
README file, for inputs to prover
CORE Library version 1.2
\$Id: README,v 1.1 2006/03/07 04:54:38 exact Exp \$
************************************************************

Simson's Theorem:

Let D be a point on the circumscribed circle
(0) of triangle ABC.  From D three perpendiculars
are drawn to the three sides BC, CA and AB.
Let E, F and G be the three feet, respectively.
Show that E, F and G are collinear.

Setup:  A(0,0), B(u_1,0), C(u_2, u_3), O(x_2, x_1),
D(x_3, u_4), E(x_5, x_4), F(x_7, x_6), G(x_3, 0)
Therefore the hypothesis equations are:

h_1 = 2 u_2 x_2 + 2 u_3 x_1 - u_3^2 - u_2^2 = 0
h_2 = 2 u_1 x_2 - u_1^2 = 0
h_3 = -x_3^2 + 2 x_2 x_3 + 2 u_4 x_1 - u_4^2 = 0
h_4 = u_3 x_5 - u_2 x_4 + u_1 x_4 - u_1 u_3 = 0
h_5 = u_2 x_5 - u_1 x_5 + u_3 x_4 - u_2 x_3 + u_1 x_3 - u_3 u_4 = 0
h_6 = u_3 x_7 - u_2 x_6 = 0
h_7 = u_2 x_7 + u_3 x_6 - u_2 x_3 - u_3 u_4 = 0

The conclusion that points E,F and G are collinear
is equivalent to:

x_4 x_7 - x_5 x_6 + x_3 x_6 - x_3 x_4 = 0

Pascal's Theorem:

Let A, B, C, D, F and E be six points on a circle
(O). Let P intersection of AB and DF, Q intersection
of BC and FE and S intersection of CD and EA.
Show that P, Q and S are collinear.

Let A(0,0), O(u_1,0), B(x_1,u_2), C(x_2,u_3), D(x_3,u_4)
F(x_4,u_5), E(x_5,u_6), P(x_7,x_6), Q(x_9,x_8) and S(x_11,x_10).
Therefore the hypothesis equations are:

h_1 = x_1^2 - 2 u_1 x_1 + u_1^2 = 0
h_2 = x_2^2 - 2 u_1 x_2 + u_3^2 = 0
h_3 = x_3^2 - 2 u_1 x_3 + u_4^2 = 0
h_4 = x_4^2 - 2 u_1 x_4 + u_5^2 = 0
h_5 = x_5^2 - 2 u_1 x_5 + u_6^2 = 0
h_6 = u_5 x_7 - u_4 x_7 - x_4 x_6 + x_3 x_6 + u_4 x_4 - u_5 x_3 = 0
h_7 = u_2 x_7 - x_1 x_6 = 0
h_8 = u_6 x_9 - u_5 x_9 - x_5 x_8 + x_4 x_8 + u_5 x_5 - u_6 x_4 = 0
h_9 = u_3 x_9 - u_2 x_9 - x_2 x_8 + x_1 x_8 + u_2 x_2 - u_3 x_1 = 0
h_10 = u_6 x_11 - x_5 x_10 = 0
h_11 = u_4 x_11 - u_3 x_11 - x_3 x_10 + x_2 x_10 + u_3 x_3 - u_4 x_2 = 0

The conclusion that P, Q and S are collinear is:

x_8 x_11 - x_6 x_11 - x_9 x_10 + x_7 x_10 + x_6 x_9 - x_7 x_8 = 0

Butterfly Theorem:

Let A, B, C, D be four points on a circle (O).
E is the intersection of AC and BD. Through E
draw a line perpendicular to OE, meeting AD at
F and BC at G. Show that FE=GE.

Let E(0,0), O(u_1,0), A(u_2,u_3), B(x_1,u_4),
C(x_3,x_2), D(x_5,x_4), F(0,x_6) and G(0,x_7).

Therefore the hypothesis equations are:

h_1 = x_1^2 - 2 u_1 x_0 + u_3^2 - u_3^2 - u_2^2 + 2u_1 u_2 = 0
h_2 = x_3^2 - 2u_1 x_3 + x_2^2 - u_3^2 - u_2^2 + 2u_1 u_2 = 0
h_3 = -u_3 x_3 + u_2 x_2 = 0
h_4 = x_5^2 - 2u_1 x_5 + x_4^2 - u_3^2 - u_2^2 + 2u_1 u_2 = 0
h_5 = -u_4 x_5 + x_1 x_4 = 0
h_6 = -x_5 x_6 + u_2 x_6 + u_3 x_5 - u_2 x_4 = 0
h_7 = -x_3 x_7 + x_1 x_7 + u_4 x_3 - x_1 x_2 = 0

The conclusion is:

g = x_7 + x_6 = 0

Pappus's Theorem:

Let ABC and EFG be two lines and P be the intersection
of AF and EB, Q the intersection of AG and EC and S the
intersectin of BG and FC. Then P, Q and S are collnear.

Let A(0,0), B(u1,0), C(u_2,0), E(u_2,u_3), F(u_4,u_5),
G(x_1,u_7), P(x_3,x_2), Q(x_5,x_4), S(x_7,x_6).

Therefore the hypothesis equations are:

h_1 = u_5 x_1 - u_3 x_1 - u_2 u_5 - u_4 u_7 +
u_3 u_4 + u_2 u_7 = 0
h_2 = u_4 x_2 - u_5 x_3 = 0
h_3 = u_2 x_2 - u_1 x_2 - u_3 x_3 + u_3 u_1 = 0
h_4 = x_1 x_4 - u_7 x_5 = 0
h_5 = u_2 x_4 - u_6 x_4 - u_3 x_5 + u_3 u_6 = 0
h_6 = u_5 x_6 - u_6 x_6 - u_5 x_7 + u_5 u_6 = 0
h_7 = x_1 x_6 - u_1 x_6 - u_7 x_7 + u_1 u_7 = 0

The conclusion is:

g = x_7 x_4 - x_2 x_7 - x_3 x_4 - x_5 x_6 +
x_3 x_6 + x_2 x_5 - x_2 x_5 = 0

```
Results 1 - 1 of 1
Help - FTP Sites List - Software Dir.
Search over 15 billion files