name(pdh).
:- dynamic p/2,l/2,i/2.

%domain elements
dom(a1). dom(b1). dom(c1). dom(a2). dom(b2). dom(c2).
dom(ab). dom(ac). dom(bc). dom(o).
dom(oa). dom(ob). dom(oc). 
dom(a1b1). dom(b1c1). dom(a1c1). dom(a2b2). dom(b2c2). dom(a2c2).

_ axiom goal_normal(U)  : (i(bc,U),i(ac,U),i(ab,U) => goal).
_ axiom hessenberg_gap1 : (i(a1,b2c2) => goal).
_ axiom hessenberg_gap2 : (i(b2,a1c1) => goal).

%Desargues assumptions: points, lines and incidences
%triangles a1b1c1 and a2b2c2
0 axiom ia1b1 : (true => i(a1,a1b1)).
0 axiom ib1a1 : (true => i(b1,a1b1)).
0 axiom ia2b2 : (true => i(a2,a2b2)).
0 axiom ib2a2 : (true => i(b2,a2b2)).
0 axiom ia1c1 : (true => i(a1,a1c1)).
0 axiom ic1a1 : (true => i(c1,a1c1)).
0 axiom ia2c2 : (true => i(a2,a2c2)).
0 axiom ic2a2 : (true => i(c2,a2c2)).
0 axiom ic1b1 : (true => i(c1,b1c1)).
0 axiom ib1c1 : (true => i(b1,b1c1)).
0 axiom ic2b2 : (true => i(c2,b2c2)).
0 axiom ib2c2 : (true => i(b2,b2c2)).
% lines through perspectivity point o and corresponding vertices
0 axiom iooa  : (true => i(o,oa)).
0 axiom ioob  : (true => i(o,ob)).
0 axiom iooc  : (true => i(o,oc)).
0 axiom ia1oa : (true => i(a1,oa)).
0 axiom ia2oa : (true => i(a2,oa)).
0 axiom ib1ob : (true => i(b1,ob)).
0 axiom ib2ob : (true => i(b2,ob)).
0 axiom ic1oc : (true => i(c1,oc)).
0 axiom ic2oc : (true => i(c2,oc)).
% cross b1c1,b2c2 in point bc
0 axiom ibc1 : (true => i(bc,b1c1)).
0 axiom ibc2 : (true => i(bc,b2c2)).
% cross a1c1, a2c2 in point ac
0 axiom iac1 : (true => i(ac,a1c1)).
0 axiom iac2 : (true => i(ac,a2c2)).
% cross a1b1,a2b2 in point ab
0 axiom iab1 : (true => i(ab,a1b1)).
1 axiom iab2 : (true => i(ab,a2b2)).
%to prove: points ab,bc,ac on (perspectivity) line 

%triangle1 non-degenerate
_ axiom triangle1(L) : (i(a1,L),i(b1,L),i(c1,L) => false).

%triangle2 non-degenerate
_ axiom triangle2(L) : (i(a2,L),i(b2,L),i(c2,L) => false).

%no corresponding vertices in common
_ axiom notaa : (p(a2,a1)=>false). 
_ axiom notbb : (p(b2,b1)=>false). 
_ axiom notcc : (p(c2,c1)=>false).

%no corresponding edges in common
_ axiom notbc : (l(b1c1,b2c2)=>false). 
_ axiom notac : (l(a1c1,a2c2)=>false). 
_ axiom notab : (l(a1b1,a2b2)=>false).


%pequality for points
_ axiom pref(P,L)   : (i(P,L) => p(P,P)).     %sorted incidence
_ axiom psym(P,Q)   : (p(P,Q) => p(Q,P)).
_ axiom ptra(P,Q,R) : (p(P,Q),p(Q,R) => p(P,R)).

%pequality for lines
_ axiom lref(P,L)   : (i(P,L) => l(L,L)).     %sorted incidence
_ axiom lsym(L,M)   : (l(L,M) => l(M,L)).
_ axiom ltra(L,M,N) : (l(L,M),l(M,N) => l(L,N)).

%congruence
_ axiom pcon(P,Q,L) : (p(P,Q),i(Q,L) => i(P,L)).
_ axiom lcon(P,L,M) : (i(P,L),l(L,M) => i(P,M)).


%projective uniqueness
_ axiom unique(P,Q,L,M) : (i(P,L),i(P,M),i(Q,L),i(Q,M) => p(P,Q);l(L,M)).

%projective geometry
line(P,Q,L) axiom line(P,Q) : (p(P,P),p(Q,Q) => dom(L),i(P,L),i(Q,L)).
point(L,M,P) axiom point(L,M) : (l(L,L),l(M,M) => dom(P),i(P,L),i(P,M)).


%Pappus: A,B,C on L, D,E,F on M, then ... or N=O;P=Q;R=S
pappus(G,H,I) axiom papp(A,B,C,D,E,F,G,H,I,L,M,N,O,P,Q,R,S) : (
i(A,L),i(B,L),i(C,L),i(D,M),i(E,M),i(F,M),          % ABC on L, DEF on M
i(B,N),i(F,N),i(G,N),i(C,O),i(E,O),i(G,O),          % cross BF,CE in G
i(B,P),i(D,P),i(H,P),i(A,Q),i(E,Q),i(H,Q),          % cross BD,AE in H
i(C,R),i(D,R),i(I,R),i(A,S),i(F,S),i(I,S)           % cross CD,AF in I
=> l(N,O);l(P,Q);l(R,S);                            % degenerations         
   dom(T),l(T,T),i(G,T),i(H,T),i(I,T)).             % G,H,I on line T
                       
 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%proof script%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

next(0,[],[]).
next(1,[],[
line(a1,b2,L0),
point(L0,oc,P1),
line(P1,ac,L2),
point(L2,a2b2,P3),
line(P3,o,L4),
point(L4,a1c1,P5),
pappus(b2,c2,P5),
point(L4,a1b1,P6),
pappus(P1,P6,bc),
pappus(ab,bc,ac)
]).
next(H,[H|T],T).

enabled(0,[]).
enabled(1,[]).
enabled(H,[H|T]):-write(H),nl.

