Simpson's Theorem:
If perpendiculars are dropped on the three sides of a triangle from a point P on the circumcircle of the triangle ABC, prove that the feet of the perpendiculars dropped onto the sides are collinear.

Machine input :

Point order :ABCDEFG

Hypothesis: coll(AGAB) coll(ECEB) coll(AFAC) cyclic(ABCD) perp(DEBC) perp(DFAC) perp(DGAB)

Conclusion: [GFGE]=0

Machine output:

[GFGE]
=   + [GF,GD] - [GE,GD]
        ( because [GF,GE] = [GF,GD] + -1.0[GE,GD])
=   + [FA,DA] - [GE,GD]
        ( because cyclic(G,F,D,A) => [GF,GD] = [FA,DA] )
=   + [FA,DA] - [EB,DB]
        ( because cyclic(G,E,D,B) => -1.0[GE,GD] = -1.0[EB,DB] )
=   - [DA,CA] - [EB,DB]
        ( because parallel(F,A,C,A) => [FA,DA] = -1.0[DA,CA] )
=   - [DA,CA] + [DB,CB]
        ( because parallel(E,B,C,B) => -1.0[EB,DB] = [DB,CB] )
= 0.0
        ( because cyclic(D,B,C,A) => [DB,CB] = [DA,CA] )