15a16,17
> % this can be implemented with [distinct from...], page 21 Avigads paper 
> 
28c30,32
< 
---
> %Avigad mentions oposite = diffside, but does not use it in axiom
> %fof(ax_points6, axiom, (! [L,A] : ((line(L) & point(A) & non(A,L)) => (? [B] : (point(B) & non(B,L) & diffside(A,B,L)))))).
>    
33c37
< %Sana: Da li koristimo outside<=>ninside&nonc ili pisemo ovako?
---
> %avigad says that we can use outside<=>ninside&nonc and that definition can be added as an axiom
35c39,40
< 
---
> %fof(ax_points9, axiom, (! [C] : ((circle(C)) => (? [A] : (point(A) & outside(A,C)))))).   
>    
50c55,57
< %Sana: Da li mi treba obratna aksioma od ove? Kako da zakljucimo da se L i M seku?
---
> %Avigad: they are using the word intersect to refer to transversal intersection
>    
> %this is oposite to ax_rule1 u intersection rules u diagrammatic_infereces
56a64,65
> %intersection circle and line closer to D
> % use ninside(D,C) & nonc(D,C) instead of outside(D,C) for now
58a68
> %intersection circle and line further to D
66a77
> %Avigad does not use diffside in this axiom
68a80,81
> %fof(ax_intersections9, axiom, (! [C1,C2,D1,D2,B,L] : ((circle(C1) & circle(C2) & point(D1) & point(D2) & point(B) & line(L) & intersectscc(C1,C2) & center(D1,C1) & center(D2,C2) & on(D1,L) & on(D2,L) & non(B,L)) => (? [A] : (point(A) & onc(A,C1) & onc(A,C2) & diffside(A,B,L)))))).
> 
74,90d86
< fof(ax_branch_on, axiom, (! [L,A] : ((line(L) & point(A)) => (on(A,L) | non(A,L))))).
< 
< fof(ax_false_on, axiom, (! [L,A] : ((line(L) & point(A) & on(A,L) & non(A,L)) => $false))).
< 
< fof(ax_branch_sameside, axiom, (! [L,A,B] : ((line(L) & point(A) & point(B)) => (sameside(A,B,L) | nsameside(A,B,L))))).
< 
< fof(ax_false_sameside, axiom, (! [L,A,B] : ((line(L) & point(A) & point(B) & sameside(A,B,L) & nsameside(A,B,L)) => $false))).
< 
< fof(ax_branch_inside, axiom, (! [C,A] : ((point(A) & circle(C)) => (inside(A,C) | ninside(A,C))))).
< 
< fof(ax_false_inside, axiom, (! [C,A] : ((point(A) & circle(C) & inside(A,C) & ninside(A,C)) => $false))).
< 
< fof(ax_branch_onc, axiom, (! [C,A] : ((circle(C) & point(A)) => (onc(A,C) | nonc(A,C))))).
< 
< fof(ax_false_onc, axiom, (! [C,A] : ((circle(C) & point(A) & onc(A,C) & nonc(A,C)) => $false))).
< 
< 
108,111d103
< fof(ax_branch_bet, axiom, (! [A,B,C] : ((point(A) & point(B) & point(C)) => (bet(A,B,C) | nbet(A,B,C))))).
< 
< fof(ax_false_bet, axiom, (! [A,B,C] : ((point(A) & point(B) & point(C) & bet(A,B,C) & nbet(A,B,C)) => $false))).
< 
120d111
< %Sana: Otkud ovaj komentar?
127,128c118
< %Avigad: This axiom is, in fact, a first-order consequence of the others;
< %Sana: Avigad je ne koristi ali Northorp je koristi
---
> %Avigad: This axiom is, in fact, a first-order consequence of the others but is useful in more restrictive notions of consequence - section 3.8
145c135,138
< 
---
> %the following lemmas can be added to the system when proving more complex theorems
> %if we decide to include diffside
> %fof(ax_samesideAux1,axiom, (![A,B,C,L] : ((point(A) & point(B) & point(C) & line(L) & non(A,L) & non(B,L) & non(C,L) & diffside(A,B,L) & diffside(A,C,L)) => (sameside(B,C,L))))).
> %fof(ax_samesideAux2,axiom, (![A,B,C,L] : ((point(A) & point(B) & point(C) & line(L) & non(A,L) & non(B,L) & non(C,L) & sameside(A,B,L) & diffside(A,C,L)) => (diffside(B,C,L))))).
150a144,146
> %they relate the between relation and the sameside relation
> %the name for the group is chosen to indicate that they provide an analysis of the usual Pasch axiom into more basic diagrammatic rules - page 21 Avigad paper on Elements
> 
162a159,160
> %these axioms explain how three lines intersecting in a point divide space into regions
>    
175c173
< %Sana: aksioma glasi, ako su A i B unutar ili na krugu, pa je moramo razbiti na 4 slucaja
---
> %axiom states ...each inside or on circle... for two points, so we get 4 combinations, i.e. 4 axioms
184c182
< %Sana: aksioma glasi, ako je A unutar ili na krugu, pa je moramo razbiti na 2 slucaja
---
> %axiom states ...inside or on circle... for one point, so we get 2 combinations, i.e. 2 axioms
189,191c187,188
< %Sana: Da li je u redu Avigadovu recenicu "P1 i P2 su dva razlicita kruga koja se seku u razlicitim tackama C i D" zapisati ovako?
< fof(ax_circle4, axiom, (! [P1,P2,C,D,A,B,L] : ((circle(P1) & circle(P2) & point(C) & point(D) & point(A) & point(B) & line(L) & P1 != P2 & intersectscc(P1,P2) & C != D & onc(C,P1) & onc(C,P2) & onc(D,P1) & onc(D,P2) & center(A,P1) & center(B,P2) & on(A,L) & on(B,L)) => (nsameside(C,D,L))))).
< 
---
> fof(ax_circle4, axiom, (! [P1,P2,C,D,A,B,L] : ((circle(P1) & circle(P2) & point(C) & point(D) & point(A) & point(B) & line(L) & P1 != P2 & intersectscc(P1,P2) & C != D & onc(C,P1) & onc(C,P2) & onc(D,P1) & onc(D,P2) & center(A,P1) & center(B,P2) & A!=B & on(A,L) & on(B,L)) => (nsameside(C,D,L))))).
>    
196c193,195
< %Sana: da li koristiti novi predikat diffside(A,B,L) (ne postoji u Avigadovom fajlu) umesto "non(A,L) & non(B,L) & nsameside(A,B,L)"?
---
> %intersection means transversal intersection
>    
> %we can later use new predicate diffside(A,B,L) which stands for "non(A,L) & non(B,L) & nsameside(A,B,L)" 
199,200c198,199
< %Sana: Aksioma glasi: A is on or inside C, B is on or inside C pa delimo aksiomu na 4
< %Sana: diffside(A,B,L) ili raspisano?
---
> %A is on or inside C, B is on or inside C, we formulate 4 cases
> %we can later use diffside(A,B,L)
211,215c210,214
< %Sana: Mislim da postoji greska u Avigadovom sistemu!
< %Kod njega stoji da je "A on or inside C1" ali ako je "A inside C1" onda aksioma ne mora da bude tacna.
< %"B is on or inside C1" pa delimo aksiomu na dve
< %outside(B,C2) ili "nonc(B,C2) & ninside(B,C2)"?
< fof(ax_rule4, axiom, (! [A,B,C1,C2] : ((point(A) & point(B) & circle(C1) & circle(C2) & onc(A,C1) & onc(B,C1) & inside(A,C2) & nonc(B,C2) & ninside(B,C2)) => (intersectscc(C1,C2))))).
---
> %"B is on or inside C1" thus we formulate 2 axioms
> % we can use predicate outside(B,C2) if we define it as "nonc(B,C2) & ninside(B,C2)" later
> fof(ax_rule4_1, axiom, (! [A,B,C1,C2] : ((point(A) & point(B) & circle(C1) & circle(C2) & onc(A,C1) & onc(B,C1) & inside(A,C2) & nonc(B,C2) & ninside(B,C2)) => (intersectscc(C1,C2))))).
> 
> fof(ax_rule4_2, axiom, (! [A,B,C1,C2] : ((point(A) & point(B) & circle(C1) & circle(C2) & onc(A,C1) & inside(B,C1) & inside(A,C2) & nonc(B,C2) & ninside(B,C2)) => (intersectscc(C1,C2))))).
218a218,220
> % EQUALITY AXIOMS are naturally part of the coherent logic prover and atp
>    
>    
220c222
< %       ADDITIONAL AXIOMS               %
---
> %       METRIC INFERENCES               %
223,241c225
< %Sana: Posto kod nas nema funkcija moramo dodati dodatne aksiome koje ce da ih simuliraju. Aksiome su uglavnom identicne kao kod Tarskog
< 
< fof(ax_cong_eq1, axiom, (! [A,B,C] : ((point(A) & point(B) & point(C) & cong(A,A,B,C)) => (B=C)))).
< 
< %fof(ax_cong_eq2, axiom, (! [A,C] : ((point(A) & point(C)) => (cong(A,A,C,C))))).
< 
< fof(ax_cong_reflexivity, axiom, (! [A,B] : ((point(A) & point(B)) => (cong(A,B,A,B))))).
< 
< fof(ax_cong_symmetry, axiom, (! [A,B,C,D] : ((point(A) & point(B) & point(C) & point(D) & cong(A,B,C,D)) => (cong(C,D,A,B))))).
< 
< fof(ax_cong_transitivity, axiom, (! [A,B,P,Q,R,S] : ((point(A) & point(B) & point(P) & point(Q) & point(R) & point(S) & cong(A,B,P,Q) & cong(A,B,R,S)) => (cong(P,Q,R,S))))).
< 
< 
< %DEFINISEMO DUZINU DUZI AA = 0, uvodimo novi predikat cong_zero
< 
< %proveriti da nemamo redundantnost
< fof(ax_cong_zero1, axiom, (! [A,B,C] : ((point(A) & point(B) & point(C) & cong(A,B,C,C)) => cong_zero(A,B)))).
< 
< fof(ax_cong_zero2, axiom, (! [A,B,C] : ((point(A) & point(B) & point(C) & cong_zero(A,B)) => cong(A,B,C,C)))).
---
> %Avigad: the following axioms Euclid seems to take to be clear form the definitions. They include 0 as a magnitude.
242a227,228
> %axiom is equivalence, thus we have two
> fof(ax_metric1_1, axiom, (! [A,B] : ((point(A) & point(B) & cong_zero(A,B)) => (A=B)))).
244,258c230
< %DEFINISEMO SABIRANJE DUZI 
< 
< %Osnovna definicija krece od ax_segment1: (! [A,B,C] : ((point(A) & point(B) & point(C) & bet(A,B,C)) => (segment_add(A,B,B,C,A,C))).
< 
< %AB + CD = PQ, AB = A1B1 => A1B1 + CD = PQ
< fof(ax_segment_add1, axiom, (! [A1,A2,B1,B2,C1,C2,P,Q] : ((point(A1) & point(A2) & point(B1) & point(B2) & point(C1) & point(C2) & point(P) & point(Q) & segment_add(A1,A2,B1,B2,C1,C2) & cong(A1,A2,P,Q)) => (segment_add(P,Q,B1,B2,C1,C2))))).
< 
< %AB + CD = PQ, CD = C1D1 => AB + C1D1 = PQ
< fof(ax_segment_add2, axiom, (! [A1,A2,B1,B2,C1,C2,P,Q] : ((point(A1) & point(A2) & point(B1) & point(B2) & point(C1) & point(C2) & point(P) & point(Q) & segment_add(A1,A2,B1,B2,C1,C2) & cong(B1,B2,P,Q)) => (segment_add(A1,A2,P,Q,C1,C2))))).
< 
< %AB + CD = PQ, PQ = P1Q1 => AB + CD = P1Q1
< fof(ax_segment_add3, axiom, (! [A1,A2,B1,B2,C1,C2,P,Q] : ((point(A1) & point(A2) & point(B1) & point(B2) & point(C1) & point(C2) & point(P) & point(Q) & segment_add(A1,A2,B1,B2,C1,C2) & cong(C1,C2,P,Q)) => (segment_add(A1,A2,B1,B2,P,Q))))).
< 
< %AB + CD = PQ => CD + AB = PQ
< fof(ax_segment_add4, axiom, (! [A1,A2,B1,B2,C1,C2,P,Q] : ((point(A1) & point(A2) & point(B1) & point(B2) & point(C1) & point(C2) & point(P) & point(Q) & segment_add(A1,A2,B1,B2,C1,C2)) => (segment_add(B1,B2,A1,A2,C1,C2))))).
---
> fof(ax_metric1_2, axiom, (! [A,B] : ((point(A) & point(B) & A=B) => (cong_zero(A,B))))).
260,261c232,234
< %AB + 0 = AB, 0 + AB = AB
< fof(ax_segment_add5, axiom, (! [A,B,C,D] : ((point(A) & point(B) & point(C) & point(D) & cong_zero(C,D)) => (segment_add(A,B,C,D,A,B) & segment_add(C,D,A,B,A,B))))).
---
> %the following lemma is using a predicate that will later be defined cong_leq
>    
> fof(ax_metric2, axiom, (! [A,B,C] : ((point(A) & point(B) & point(C)) => (cong_leq(C,C,A,B))))).
263,264c236
< %AB + CD = PQ, A1B1 + C1D1 = P1Q1, AB = A1B1, CD = C1D1 => PQ = P1Q1
< fof(ax_segment_add6, axiom, (! [A,B,C,D,P,Q,A1,B1,C1,D1,P1,Q1] : ((point(A) & point(B) & point(C) & point(D) & point(P) & point(Q) & segment_add(A,B,C,D,P,Q) & segment_add(A1,B1,C1,D1,P1,Q1) & cong(A,B,A1,B1) & cong(C,D,C1,D1)) => (cong(P,Q,P1,Q1))))).
---
> fof(ax_metric3, axiom, (! [A,B] : ((point(A) & point(B)) => (cong(A,B,B,A))))).
266,267c238
< %AB + CD = PQ, A1B1 + C1D1 = P1Q1, AB = A1B1, PQ = P1Q1 => CD = C1D1
< fof(ax_segment_add7, axiom, (! [A,B,C,D,P,Q,A1,B1,C1,D1,P1,Q1] : ((point(A) & point(B) & point(C) & point(D) & point(P) & point(Q) & segment_add(A,B,C,D,P,Q) & segment_add(A1,B1,C1,D1,P1,Q1) & cong(A,B,A1,B1) & cong(P,Q,P1,Q1)) => (cong(C,D,C1,D1))))).
---
> fof(ax_metric4, axiom, (! [A,B,C] : ((point(A) & point(B) & point(C) & A != B & A != C) => (cong_angle(A,B,C,C,B,A))))).
269,270c240
< %AB + CD = PQ, A1B1 + C1D1 = P1Q1, CD = C1D1, PQ = P1Q1 => AB = A1B1 
< fof(ax_segment_add8, axiom, (! [A,B,C,D,P,Q,A1,B1,C1,D1,P1,Q1] : ((point(A) & point(B) & point(C) & point(D) & point(P) & point(Q) & segment_add(A,B,C,D,P,Q) & segment_add(A1,B1,C1,D1,P1,Q1) & cong(C,D,C1,D1)& cong(P,Q,P1,Q1)) => (cong(A,B,A1,B1))))).
---
> %define a predicate cong_angle_zero - in avigad_additional_definitions.p
271a242
> %define a predicate cong_angle_leq
273c244
< %DEFINISEMO POREDJENJE DUZI, predikati cong_less i cong_leq (strogo manje i manje ili jednako)
---
> fof(ax_metric5_1, axiom, (! [A,B,C,D,E,F] : ((point(A) & point(B) & point(C) & point(D) & point(E) & point(F) & cong_angle_zero(A,B,C)) => (cong_angle_leq(A,B,C,D,E,F))))).
275,276c246
< %A1A2 + B1B2 = C1C2 => A1A2 < C1C2 & B1B2 < C1C2
< fof(ax_cong_less1, axiom, (![A1,A2,B1,B2,C1,C2] : ((point(A1) & point(A2) & point(B1) & point(B2) & point(C1) & point(C2) & segment_add(A1,A2,B1,B2,C1,C2)) => (cong_less(A1,A2,C1,C2) & cong_less(B1,B2,C1,C2))))).
---
> fof(ax_metric5_2, axiom, (! [A,B,C,R1,R2,R3,P1,P2,P3,Q1,Q2,Q3] : ((point(A) & point(B) & point(C) & point(R1) & point(R2) & point(R3) & point(P1) & point(P2) & point(P3) & point(Q1) & point(Q2) & point(Q3) & right_angle(R1,R2,R3) & right_angle(P1,P2,P3) & angle_add(R1,R2,R3,P1,P2,P3,Q1,Q2,Q3)) => (cong_angle_leq(A,B,C,Q1,Q2,Q3))))).
278,280c248,249
< %AB < CD => AB + EF < CD + EF;
< %AB + EF = GH; CD + EF = KL
< fof(ax_cong_less2, axiom, (! [A,B,C,D,E,F,G,H,K,L] : ((point(A) & point(B) & point(C) & point(D) & point(E) & point(F) & point(G) & point(H) & point(K) & point(L) & cong_less(A,B,C,D) & segment_add(A,B,E,F,G,H) & segment_add(C,D,E,F,K,L)) => (cong_less(G,H,K,L))))).
---
> %area(AAB) = 0
> fof(ax_metric6, axiom, (! [A,B] : ((point(A) & point(B)) => (cong_area_zero(A,A,B))))).
282,283c251,252
< %AB < CD, AB = A1B1 => A1B1 < CD
< fof(ax_cong_less3, axiom, (! [A,B,C,D,A1,B1] : ((point(A) & point(B) & point(C) & point(D) & point(A1) & point(B1) & cong_less(A,B,C,D) & cong(A,B,A1,B1)) => (cong_less(A1,B1,C,D))))).
---
> %povrsina(A,B,C) >= 0
> fof(ax_metric7, axiom, (! [A,B,C,D,E,F] : ((point(A) & point(B) & point(C) & point(D) & point(E) & point(F) & cong_area_zero(A,B,C)) => (cong_area_leq(A,B,C,D,E,F))))).
285,286c254
< %AB < CD, CD = C1D1 => AB < C1D1
< fof(ax_cong_less4, axiom, (! [A,B,C,D,C1,D1] : ((point(A) & point(B) & point(C) & point(D) & point(C1) & point(D1) & cong_less(A,B,C,D) & cong(C,D,C1,D1)) => (cong_less(A,B,C1,D1))))).
---
> fof(ax_metric8, axiom, (! [A,B,C] : ((point(A) & point(B) & point(C)) => (cong_area(A,B,C,C,A,B) & cong_area(A,B,C,A,C,B))))).
287a256
> fof(ax_metric9, axiom, (! [A,B,C,A1,B1,C1] : ((point(A) & point(B) & point(C) & point(A1) & point(B1) & point(C1) & cong(A,B,A1,B1) & cong(B,C,B1,C1) & cong(C,A,C1,A1) & cong_angle(A,B,C,A1,B1,C1) & cong_angle(B,C,A,B1,C1,A1) & cong_angle(C,A,B,C1,A1,B1)) => (cong_area(A,B,C,A1,B1,C1))))).
289,290d257
< %DEFINISEMO PREDIKAT cong_leq (less or equal)
< %Posto se definise preko cong_less mislim da ne trebaju dodatne aksiome tipa A=<B => A+C=<B+C
292,293d258
< %AB <= CD <--> AB = CD \/ AB < CD
< fof(ax_cong_leq1, axiom, (! [A,B,C,D] : ((point(A) & point(B) & point(C) & point(D) & cong_leq(A,B,C,D)) => (cong(A,B,C,D) | cong_less(A,B,C,D))))).
295d259
< fof(ax_cong_leq2, axiom, (! [A,B,C,D] : ((point(A) & point(B) & point(C) & point(D) & cong(A,B,C,D)) => (cong_leq(A,B,C,D))))).
297c261
< fof(ax_cong_leq3, axiom, (! [A,B,C,D] : ((point(A) & point(B) & point(C) & point(D) & cong_less(A,B,C,D)) => (cong_leq(A,B,C,D))))).
---
>    
300c264,265
< %DEFINISEMO PODUDARNOST UGLOVA predikat cong_angle
---
> % define congruence of angles
> % cong_angle
309,310c274
< %DEFINISEMO PRAV UGAO predikat right_angle, kroz Avigadove aksiome
< 
---
> % define predicate right_angle, with Avigad axioms
321,354c285
< %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
< %        METRIC INFERENCES               %
< %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
< 
< fof(ax_metric1_1, axiom, (! [A,B] : ((point(A) & point(B) & cong_zero(A,B)) => (A=B)))).
< 
< fof(ax_metric1_2, axiom, (! [A] : ((point(A)) => (cong_zero(A,A))))).
< 
< fof(ax_metric2, axiom, (! [A,B,C] : ((point(A) & point(B) & point(C)) => (cong_leq(A,A,B,C))))).
< 
< fof(ax_metric3, axiom, (! [A,B] : ((point(A) & point(B)) => (cong(A,B,B,A))))).
< 
< fof(ax_metric4, axiom, (! [A,B,C] : ((point(A) & point(B) & point(C) & A != B & A != C) => (cong_angle(A,B,C,C,B,A))))).
< 
< %Uvodimo predikat cong_angle_zero koji ce biti definisan naknadno u Diagram-angle aksiomama
< 
< %DEFINISEMO POREDJENJE UGLOVA predikat cong_angle_leq
< %Sana:Kako se definise cong_angle_leq
< 
< %PRELISTAJ STARU VERZIJU AKSIOMA I DODAJ STA FALI
< 
< fof(ax_metric5_1, axiom, (! [A,B,C,D,E,F] : ((point(A) & point(B) & point(C) & point(D) & point(E) & point(F) & cong_angle_zero(A,B,C)) => (cong_angle_leq(A,B,C,D,E,F))))).
< 
< fof(ax_metric5_2, axiom, (! [A,B,C,R1,R2,R3,P1,P2,P3,Q1,Q2,Q3] : ((point(A) & point(B) & point(C) & point(R1) & point(R2) & point(R3) & point(P1) & point(P2) & point(P3) & point(Q1) & point(Q2) & point(Q3) & right_angle(R1,R2,R3) & right_angle(P1,P2,P3) & angle_add(R1,R2,R3,P1,P2,P3,Q1,Q2,Q3)) => (cong_angle_leq(A,B,C,Q1,Q2,Q3))))).
< 
< %povrsina(AAB) = 0
< fof(ax_metric6, axiom, (! [A,B] : ((point(A) & point(B)) => (cong_area_zero(A,A,B))))).
< 
< %povrsina(A,B,C) >= 0
< fof(ax_metric7, axiom, (! [A,B,C,D,E,F] : ((point(A) & point(B) & point(C) & point(D) & point(E) & point(F) & cong_area_zero(A,B,C)) => (cong_area_leq(A,B,C,D,E,F))))).
< 
< fof(ax_metric8, axiom, (! [A,B,C] : ((point(A) & point(B) & point(C)) => (cong_area(A,B,C,C,A,B) & cong_area(A,B,C,A,C,B))))).
< 
< fof(ax_metric9, axiom, (! [A,B,C,A1,B1,C1] : ((point(A) & point(B) & point(C) & point(A1) & point(B1) & point(C1) & cong(A,B,A1,B1) & cong(B,C,B1,C1) & cong(C,A,C1,A1) & cong_angle(A,B,C,A1,B1,C1) & cong_angle(B,C,A,B1,C1,A1) & cong_angle(C,A,B,C1,A1,B1)) => (cong_area(A,B,C,A1,B1,C1))))).
---
> 	       
368a300,301
> % the following axiom has if and only if, and we need to split it into two axioms
> 
382c315
< %Uvodi cong_angle_zero
---
> % first time uses cong_angle_zero, has equivalence in original Avigads axiom
387c320
< %Uvodi sabiranje uglova, angle_add
---
> % addition of angles angle_add
392c325,327
< %Uvodi right_angle
---
> % Avigad notes that Euclids wording make it seem more natural to use a predicate to assert that abc forms a right angle - which is exactly what we have to do so we must be doing something right :)
> % introduces right_angle
>    
397c332
< %Sana: Proveriti da li su svi Euklidovi postulati i Common notions prisutni?
---
> %Euclid postulates and common notions are among these axioms
400c335,336
< %Kako zapisati Euclid postulate 5? And that if a straight-line falling across two (other) straight-lines makes internal angles on the same side (of itself whose sum is) less than two right-angles, then the two (other) straight-lines, being produced to infinity, meet on that side (of the original straight-line) that the (sum of the internal angles) is less than two right-angles (and do not meet on the other side).
---
> %Euclid postulate 5 - is it part of axioms 
> %And that if a straight-line falling across two (other) straight-lines makes internal angles on the same side (of itself whose sum is) less than two right-angles, then the two (other) straight-lines, being produced to infinity, meet on that side (of the original straight-line) that the (sum of the internal angles) is less than two right-angles (and do not meet on the other side).
404,408c340,342
< %Sana: ne znam kako da zapisem ax_angle5, pominje se sabiranje i poredjenje uglova
< %jako sumnjiv zapis
< 
< %Euklid postulat 4   
< fof(ax_angle5, axiom, (! [A,B,C,D,L,M,N,P1,P2,P3,R1,R2,R3,R4,R5,R6,R7,R8,R9,E] : ((point(A) & point(B) & point(C) & point(D) & line(L) & line(M) & line(N) & point(P1) & point(P2) & point(P3) & point(R1) & point(R2) & point(R3) & point(R4) & point(R5) & point(R6) & point(R7) & point(R8) & point(R9) & point(E) & on(A,L) & on(B,L) & on(B,M) & on(C,M) & on(C,N) & on(D,N) & B != C & sameside(A,D,N) & angle_add(A,B,C,B,C,D,P1,P2,P3) & right_angle(R1,R2,R3) & right_angle(R4,R5,R6) & angle_add(R1,R2,R3,R4,R5,R6,R7,R8,R9) & cong_angle_less(P1,P2,P3,R7,R8,R9) & on(E,L) & on(E,N)) => (intersects(L,N) & sameside(E,A,M))))).
---
> % Euclid postulat 4
> % I think error: sameside(A,D,M) instead of sameside(A,D,N) as D belongs to N
> fof(ax_angle5, axiom, (! [A,B,C,D,L,M,N,P1,P2,P3,R1,R2,R3,R4,R5,R6,R7,R8,R9,E] : ((point(A) & point(B) & point(C) & point(D) & line(L) & line(M) & line(N) & point(P1) & point(P2) & point(P3) & point(R1) & point(R2) & point(R3) & point(R4) & point(R5) & point(R6) & point(R7) & point(R8) & point(R9) & point(E) & on(A,L) & on(B,L) & on(B,M) & on(C,M) & on(C,N) & on(D,N) & B != C & sameside(A,D,M) & angle_add(A,B,C,B,C,D,P1,P2,P3) & right_angle(R1,R2,R3) & right_angle(R4,R5,R6) & angle_add(R1,R2,R3,R4,R5,R6,R7,R8,R9) & cong_angle_less(P1,P2,P3,R7,R8,R9) & on(E,L) & on(E,N)) => (intersects(L,N) & sameside(E,A,M))))).
414,415c348
< %DEFINICIJA cong_area_zero
< %Sana: dodati aksiome za sabiranje, poredjenje,... slicno kao za cong
---
> % cong_area_zero
417d349
< %Uvodimo povrsina(A,B,C) = 0
422c354,355
< %Uvodimo sabiranje povrsina trouglova
---
> % area_add
>    
425a359,640
> 
> % possible error in Avigad page 26, angle abc instead of bac
> % in Lean formalization this error is corrected
> 
> % possible error in Lean formalization, at the end
> % distinctPointsOnLine B1 C1 BC1 --- why BC1, why not B1C1?
> % distinctPointsOnLine A1 C1 AC1 --- why AC1, why not A1C1?
> % it was always used with same points...
> 
> % u dokazu th_prop4_proof.txt koristi se ova aksioma pa cemo da napakujemo taj korak   
> % A B C D E F
> % G -> E
> % H -> F
> % L -> DE
> 
> % C1!=B & C1!=A & cong_angle(B,A,C,B1,D,C1) & cong_angle(A,C,B,D,C1,B1) & cong_angle(C,B,A,C1,B1,D) & cong(A,B,D,B1) & cong(B,C,B1,C1) & cong(C,A,C1,D) & on(B1,L) & nbet(B1,D,G) & sameside(C1,H,L) & B1!=C1 & D!=C1
>    
> fof(ax_superposition1, axiom, ![A,B,C,D,G,H,L] : ((point(A) & point(B) & point(C) & point(D) & point(G) & point(H) & line(L) & ncol(A,B,C) & A!=B & A!=C & B!=C & D!=G & on(D,L) & on(G,L) & non(H,L)) => (? [A1,B1,C1] : (point(A1) & point(B1) & point(C1) & A1=D & C1!=B & C1!=A & cong_angle(B,A,C,B1,A1,C1) & cong_angle(A,C,B,A1,C1,B1) & cong_angle(C,B,A,C1,B1,A1) & cong(A,B,A1,B1) & cong(B,C,B1,C1) & cong(C,A,C1,A1) & on(B1,L) & nbet(B1,A1,G) & sameside(C1,H,L) & B1!=C1 & A1!=C1).
> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
> % COHERENT LOGIC TREATMENT OF NEGATION %
> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
> 
> %for every predicate R, new predicate nR is introduced with two following axioms per predicate
> 
> fof(ax_branch_on, axiom, (! [L,A] : ((line(L) & point(A)) => (on(A,L) | non(A,L))))).
> 
> fof(ax_false_on, axiom, (! [L,A] : ((line(L) & point(A) & on(A,L) & non(A,L)) => $false))).
> 
> fof(ax_branch_sameside, axiom, (! [L,A,B] : ((line(L) & point(A) & point(B)) => (sameside(A,B,L) | nsameside(A,B,L))))).
> 
> fof(ax_false_sameside, axiom, (! [L,A,B] : ((line(L) & point(A) & point(B) & sameside(A,B,L) & nsameside(A,B,L)) => $false))).
> 
> %fof(ax_branch_diffside, axiom, (! [L,A,B] : ((line(L) & point(A) & point(B)) => (diffside(A,B,L) | ndiffside(A,B,L))))).
> 
> %fof(ax_false_diffside, axiom, (! [L,A,B] : ((line(L) & point(A) & point(B) & diffside(A,B,L) & ndiffside(A,B,L)) => $false))).
> 
> fof(ax_branch_inside, axiom, (! [C,A] : ((point(A) & circle(C)) => (inside(A,C) | ninside(A,C))))).
> 
> fof(ax_false_inside, axiom, (! [C,A] : ((point(A) & circle(C) & inside(A,C) & ninside(A,C)) => $false))).
> 
> %fof(ax_branch_outside, axiom, (! [C,A] : ((point(A) & circle(C)) => (outside(A,C) | noutside(A,C))))).
> 
> %fof(ax_false_outside, axiom, (! [C,A] : ((point(A) & circle(C) & outside(A,C) & noutside(A,C)) => $false))).
> 
> fof(ax_branch_onc, axiom, (! [C,A] : ((circle(C) & point(A)) => (onc(A,C) | nonc(A,C))))).
> 
> fof(ax_false_onc, axiom, (! [C,A] : ((circle(C) & point(A) & onc(A,C) & nonc(A,C)) => $false))).
> 
> fof(ax_branch_center, axiom, (! [C,A] : ((circle(C) & point(A)) => (center(A,C) | ncenter(A,C))))).
> 
> fof(ax_false_center, axiom, (! [C,A] : ((circle(C) & point(A) & center(A,C) & ncenter(A,C)) => $false))).
> 
> fof(ax_branch_bet, axiom, (! [A,B,C] : ((point(A) & point(B) & point(C)) => (bet(A,B,C) | nbet(A,B,C))))).
> 
> fof(ax_false_bet, axiom, (! [A,B,C] : ((point(A) & point(B) & point(C) & bet(A,B,C) & nbet(A,B,C)) => $false))).
> 
> fof(ax_branch_cong, axiom, (! [A,B,C,D] : ((point(A) & point(B) & point(C) & point(D)) => (cong(A,B,C,D) | ncong(A,B,C,D))))).
> 
> fof(ax_false_cong, axiom, (! [A,B,C,D] : ((point(A) & point(B) & point(C) & point(D) & cong(A,B,C,D) & ncong(A,B,C,D)) => $false))).
> 
> fof(ax_branch_cong_zero, axiom, (! [A,B,C,D] : ((point(A) & point(B) & point(C) & point(D)) => (cong_zero(A,B,C,D) | ncong_zero(A,B,C,D))))).
> 
> fof(ax_false_cong_zero, axiom, (! [A,B,C,D] : ((point(A) & point(B) & point(C) & point(D) & cong_zero(A,B,C,D) & ncong_zero(A,B,C,D)) => $false))).
> 
> fof(ax_branch_segment_add, axiom, (! [A,B,C,D,E,F] : ((point(A) & point(B) & point(C) & point(D) & point(E) & point(F)) => (segment_add(A,B,C,D,E,F) | nsegment_add(A,B,C,D,E,F))))).
> 
> fof(ax_false_segment_add, axiom, (! [A,B,C,D,E,F] : ((point(A) & point(B) & point(C) & point(D) & point(E) & point(F) & segment_add(A,B,C,D,E,F) & nsegment_add(A,B,C,D,E,F)) => $false))).
> 
> 
> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
> %  ADDITIONAL AXIOMS  - AVIGAD PREDICATES  %
> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
> % outside(A,K) later
> % diffside(A,B,L) later
> % cong_leq(A,B,C,D)
> % not necessary, just a shorthand
> 
> % outside
> 
> %fof(ax_outside1, axiom, (! [A,K] : ((point(A) & circle(K) & ninside(A,K) & nonc(A,K)) => (outside(A,K))))).
> 
> %fof(ax_outside2, axiom, (! [A,K] : ((point(A) & circle(K) & outside(A,K)) => (ninside(A,K) & nonc(A,K))))).
> 
> % diffside
> 
> %fof(ax_diffside1, axiom, (! [A,B,L] : ((point(A) & point(B) & line(L) & diffside(A,B,L)) => (non(A,L) & non(B,L) & nsameside(A,B,L))))).
> 
> %fof(ax_diffside2, axiom, (! [A,B,L] : ((point(A) & point(B) & line(L) & non(A,L) & non(B,L) & nsameside(A,B,L)) => (diffside(A,B,L))))).
> 
> % cong_leq (less or equal)
> % it is defined through cong_less so some axioms do not have to be added like A=<B => A+C=<B+C
> 
> %AB <= CD <--> AB = CD \/ AB < CD
> fof(ax_cong_leq1, axiom, (! [A,B,C,D] : ((point(A) & point(B) & point(C) & point(D) & cong_leq(A,B,C,D)) => (cong(A,B,C,D) | cong_less(A,B,C,D))))).
> 
> fof(ax_cong_leq2, axiom, (! [A,B,C,D] : ((point(A) & point(B) & point(C) & point(D) & cong(A,B,C,D)) => (cong_leq(A,B,C,D))))).
> 
> fof(ax_cong_leq3, axiom, (! [A,B,C,D] : ((point(A) & point(B) & point(C) & point(D) & cong_less(A,B,C,D)) => (cong_leq(A,B,C,D))))).
> 
> 
> 
> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
> %  ADDITIONAL AXIOMS  - MAGNITUDES      %
> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
> 
> 
> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
> % CONG_ZERO, reflexivity, symmetry, transitivity %
> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
> 
> 
> %as our system does not work with functions, we must add new definitions and rules as axioms; These axioms are almost identical as some Tarski axioms
> 
> 
> %In our system we do not have magnitudes, so we will introduce additional predicate
> 
> %Avigad has magnitude 0, so we define length AA = 0, with new predicate cong_zero
> 
> % AB = 0 <=> A=B
> fof(ax_cong_zero1, axiom, (! [A,B,C] : ((point(A) & point(B) & point(C) & cong(A,B,C,C)) => cong_zero(A,B)))).
> 
> fof(ax_cong_zero2, axiom, (! [A,B,C] : ((point(A) & point(B) & point(C) & cong_zero(A,B)) => cong(A,B,C,C)))).
> 
> %to represent equal segment length we will use cong
> 
> % AB = AB
> fof(ax_cong_reflexivity, axiom, (! [A,B] : ((point(A) & point(B)) => (cong(A,B,A,B))))).
> 
> % AB = CD => CD = AB
> fof(ax_cong_symmetry, axiom, (! [A,B,C,D] : ((point(A) & point(B) & point(C) & point(D) & cong(A,B,C,D)) => (cong(C,D,A,B))))).
> 
> % AB = PQ & AB = RS => PQ = RS
> fof(ax_cong_transitivity, axiom, (! [A,B,P,Q,R,S] : ((point(A) & point(B) & point(P) & point(Q) & point(R) & point(S) & cong(A,B,P,Q) & cong(A,B,R,S)) => (cong(P,Q,R,S))))).
> 
> 
> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
> %   SEGMENT_ADD                                            %
> %   + is associative and commutative, identity 0 %         %
> %   < a linear ordering with least element 0               % 
> %   x<y => x+z < y+z                                       %
> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
> 
> % define addition of segments
> % segment_add
>    
> % basic definition from transfer inferences
> % defined in avigad_transfer_inferences.p
> % ax_segment1: (! [A,B,C] : ((point(A) & point(B) & point(C) & bet(A,B,C)) => (segment_add(A,B,B,C,A,C))).
> 
> %AB + CD = PQ, AB = A1B1 => A1B1 + CD = PQ
> fof(ax_segment_add1, axiom, (! [A1,A2,B1,B2,C1,C2,P,Q] : ((point(A1) & point(A2) & point(B1) & point(B2) & point(C1) & point(C2) & point(P) & point(Q) & segment_add(A1,A2,B1,B2,C1,C2) & cong(A1,A2,P,Q)) => (segment_add(P,Q,B1,B2,C1,C2))))).
> 
> %AB + CD = PQ, CD = C1D1 => AB + C1D1 = PQ
> fof(ax_segment_add2, axiom, (! [A1,A2,B1,B2,C1,C2,P,Q] : ((point(A1) & point(A2) & point(B1) & point(B2) & point(C1) & point(C2) & point(P) & point(Q) & segment_add(A1,A2,B1,B2,C1,C2) & cong(B1,B2,P,Q)) => (segment_add(A1,A2,P,Q,C1,C2))))).
> 
> %AB + CD = PQ, PQ = P1Q1 => AB + CD = P1Q1
> fof(ax_segment_add3, axiom, (! [A1,A2,B1,B2,C1,C2,P,Q] : ((point(A1) & point(A2) & point(B1) & point(B2) & point(C1) & point(C2) & point(P) & point(Q) & segment_add(A1,A2,B1,B2,C1,C2) & cong(C1,C2,P,Q)) => (segment_add(A1,A2,B1,B2,P,Q))))).
> 
> % commutativity of + 
> 		
> %AB + CD = PQ => CD + AB = PQ
> fof(ax_segment_add4, axiom, (! [A1,A2,B1,B2,C1,C2,P,Q] : ((point(A1) & point(A2) & point(B1) & point(B2) & point(C1) & point(C2) & point(P) & point(Q) & segment_add(A1,A2,B1,B2,C1,C2)) => (segment_add(B1,B2,A1,A2,C1,C2))))).
> 
> % identity for + is 0
> 		
> %AB + 0 = AB, 0 + AB = AB
> fof(ax_segment_add5, axiom, (! [A,B,C,D] : ((point(A) & point(B) & point(C) & point(D) & cong_zero(C,D)) => (segment_add(A,B,C,D,A,B) & segment_add(C,D,A,B,A,B))))).
> 
> %AB + CD = PQ, A1B1 + C1D1 = P1Q1, AB = A1B1, CD = C1D1 => PQ = P1Q1
> fof(ax_segment_add6, axiom, (! [A,B,C,D,P,Q,A1,B1,C1,D1,P1,Q1] : ((point(A) & point(B) & point(C) & point(D) & point(P) & point(Q) & segment_add(A,B,C,D,P,Q) & segment_add(A1,B1,C1,D1,P1,Q1) & cong(A,B,A1,B1) & cong(C,D,C1,D1)) => (cong(P,Q,P1,Q1))))).
> 
> %AB + CD = PQ, A1B1 + C1D1 = P1Q1, AB = A1B1, PQ = P1Q1 => CD = C1D1
> fof(ax_segment_add7, axiom, (! [A,B,C,D,P,Q,A1,B1,C1,D1,P1,Q1] : ((point(A) & point(B) & point(C) & point(D) & point(P) & point(Q) & segment_add(A,B,C,D,P,Q) & segment_add(A1,B1,C1,D1,P1,Q1) & cong(A,B,A1,B1) & cong(P,Q,P1,Q1)) => (cong(C,D,C1,D1))))).
> 
> %AB + CD = PQ, A1B1 + C1D1 = P1Q1, CD = C1D1, PQ = P1Q1 => AB = A1B1 
> fof(ax_segment_add8, axiom, (! [A,B,C,D,P,Q,A1,B1,C1,D1,P1,Q1] : ((point(A) & point(B) & point(C) & point(D) & point(P) & point(Q) & segment_add(A,B,C,D,P,Q) & segment_add(A1,B1,C1,D1,P1,Q1) & cong(C,D,C1,D1)& cong(P,Q,P1,Q1)) => (cong(A,B,A1,B1))))).
> 
> 
> 
> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
> %   segment comparison <                                   %
> %   cong_less                                              %
> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
> 
> 		
> % based on axiom1 in diagram-segment transfer axioms		
> fof(ax_cong_less1, axiom, (![A,B,C] : ((point(A) & point(B) & point(C) & col(A,B,C)) => (cong_less(A,B,A,C) & cong_less(B,C,A,C))))).
> 		
> %A1A2 + B1B2 = C1C2 => A1A2 < C1C2 & B1B2 < C1C2
> fof(ax_cong_less2, axiom, (![A1,A2,B1,B2,C1,C2] : ((point(A1) & point(A2) & point(B1) & point(B2) & point(C1) & point(C2) & segment_add(A1,A2,B1,B2,C1,C2)) => (cong_less(A1,A2,C1,C2) & cong_less(B1,B2,C1,C2))))).
> 
> %AB < CD => AB + EF < CD + EF;
> %AB + EF = GH; CD + EF = KL
> fof(ax_cong_less3, axiom, (! [A,B,C,D,E,F,G,H,K,L] : ((point(A) & point(B) & point(C) & point(D) & point(E) & point(F) & point(G) & point(H) & point(K) & point(L) & cong_less(A,B,C,D) & segment_add(A,B,E,F,G,H) & segment_add(C,D,E,F,K,L)) => (cong_less(G,H,K,L))))).
> 
> %AB < CD, AB = A1B1 => A1B1 < CD
> fof(ax_cong_less4, axiom, (! [A,B,C,D,A1,B1] : ((point(A) & point(B) & point(C) & point(D) & point(A1) & point(B1) & cong_less(A,B,C,D) & cong(A,B,A1,B1)) => (cong_less(A1,B1,C,D))))).
> 
> %AB < CD, CD = C1D1 => AB < C1D1
> fof(ax_cong_less5, axiom, (! [A,B,C,D,C1,D1] : ((point(A) & point(B) & point(C) & point(D) & point(C1) & point(D1) & cong_less(A,B,C,D) & cong(C,D,C1,D1)) => (cong_less(A,B,C1,D1))))).   
> 
>    
> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
> % CONG_ANGLE_ZERO, reflexivity, symmetry, transitivity %
> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
> 
> % angle ABC = 0 is defined as nbet(B,A,C) <=> cong_angle_zero(B,A,C)
> % axiom 1, i.e. ax_angle1_1, and ax_angle1_2 in diagram-angle transfer axioms
> 		
> 
> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
> % ANGLE_ADD, reflexivity, symmetry, transitivity %
> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
> 
> % defined in ax_angle2 in diagram-angle transfer axioms
> 
> % angle(A,B,C) + angle(Z1,Z2,Z3) = angle(A,B,C) <=> cong_angle_zero(Z1,Z2,Z3)
> 
> fof(ax_angle_add1_1, axiom, (![A,B,C,Z1,Z2,Z3] : ((point(A) & point(B) & point(C) & point(Z1) & point(Z2) & point(Z3) & cong_angle_zero(Z1,Z2,Z3)) => (angle_add(A,B,C,Z1,Z2,Z3,A,B,C))))).
> 
> fof(ax_angle_add1_2, axiom, (![A,B,C,Z1,Z2,Z3] : ((point(A) & point(B) & point(C) & point(Z1) & point(Z2) & point(Z3) & angle_add(A,B,C,Z1,Z2,Z3,A,B,C)) => cong_angle_zero(Z1,Z2,Z3)))).
> 
> % angle A1A2A3 + angle B1B2B3 = angle C1C2C3 &
> % angle A1A2A3 = angle D1D2D3                =>
> % angle D1D2D3 + angle B1B2B3 = angle C1C2C3
> 
> fof(ax_angle_add2, axiom, (![A1,A2,A3,B1,B2,B3,C1,C2,C3,D1,D2,D3] : ((point(A1) & point(A2) & point(A3) & point(B1) & point(B2) & point(B3) & point(C1) & point(C2) & point(C3) & point(D1) & point(D2) & point(D3) & angle_add(A1,A2,A3,B1,B2,B3,C1,C2,C3) & cong_angle(A1,A2,A3,D1,D2,D3)) => (angle_add(D1,D2,D3,B1,B2,B3,C1,C2,C3))))).
> 
> % angle A1A2A3 + angle B1B2B3 = angle C1C2C3 &
> % angle B1B2B3 = angle D1D2D3                =>
> % angle A1A2A3 + angle D1D2D3 = angle C1C2C3
> 
> fof(ax_angle_add3, axiom, (![A1,A2,A3,B1,B2,B3,C1,C2,C3,D1,D2,D3] : ((point(A1) & point(A2) & point(A3) & point(B1) & point(B2) & point(B3) & point(C1) & point(C2) & point(C3) & point(D1) & point(D2) & point(D3) & angle_add(A1,A2,A3,B1,B2,B3,C1,C2,C3) & cong_angle(B1,B2,B3,D1,D2,D3)) => (angle_add(A1,A2,A3,D1,D2,D3,C1,C2,C3))))).
> 
> 		
> % angle A1A2A3 + angle B1B2B3 = angle C1C2C3 &
> % angle C1C2C3 = angle D1D2D3                =>
> % angle A1A2A3 + angle B1B2B3 = angle D1D2D3
> 
> fof(ax_angle_add4, axiom, (![A1,A2,A3,B1,B2,B3,C1,C2,C3,D1,D2,D3] : ((point(A1) & point(A2) & point(A3) & point(B1) & point(B2) & point(B3) & point(C1) & point(C2) & point(C3) & point(D1) & point(D2) & point(D3) & angle_add(A1,A2,A3,B1,B2,B3,C1,C2,C3) & cong_angle(C1,C2,C3,D1,D2,D3)) => (angle_add(A1,A2,A3,B1,B2,B3,D1,D2,D3))))).
> 
> 		
> % angle A1A2A3 + angle B1B2B3 = angle C1C2C3 =>
> % angle B1B2B3 + angle A1A2A3 = angle C1C2C3 
> 
> fof(ax_angle_add5, axiom, (![A1,A2,A3,B1,B2,B3,C1,C2,C3] : ((point(A1) & point(A2) & point(A3) & point(B1) & point(B2) & point(B3) & point(C1) & point(C2) & point(C3) & angle_add(A1,A2,A3,B1,B2,B3,C1,C2,C3)) => (angle_add(B1,B2,B3,A1,A2,A3,C1,C2,C3))))).
> 
> 		
> % angle A1A2A3 + angle B1B2B3 = angle C1C2C3 &
> % angle A4A5A6 + angle B4B5B6 = angle C4C5C6 &
> % angle A1A2A3 = angle A4A5A6                &
> % angle B1B2B3 = angle B4B5B6                =>
> % angle C1C2C3 = angle C4C5C6                
> 
> fof(ax_angle_add6, axiom, (![A1,A2,A3,B1,B2,B3,C1,C2,C3,A4,A5,A6,B4,B5,B6,C4,C5,C6] : ((point(A1) & point(A2) & point(A3) & point(B1) & point(B2) & point(B3) & point(C1) & point(C2) & point(C3) & point(A4) & point(A5) & point(A6) & point(B4) & point(B5) & point(B6) & point(C4) & point(C5) & point(C6) & angle_add(A1,A2,A3,B1,B2,B3,C1,C2,C3) & angle_add(A4,A5,A6,B4,B5,B6,C4,C5,C6) & cong_angle(A1,A2,A3,A4,A5,A6) & cong_angle(B1,B2,B3,B4,B5,B6)) => (cong_angle(C1,C2,C3,C4,C5,C6))))).
> 
> 		
> % angle A1A2A3 + angle B1B2B3 = angle C1C2C3 &
> % angle A4A5A6 + angle B4B5B6 = angle C4C5C6 &
> % angle A1A2A3 = angle A4A5A6                &
> % angle C1C2C3 = angle C4C5C6                =>
> % angle B1B2B3 = angle B4B5B6                
> 
> 
> fof(ax_angle_add7, axiom, (![A1,A2,A3,B1,B2,B3,C1,C2,C3,A4,A5,A6,B4,B5,B6,C4,C5,C6] : ((point(A1) & point(A2) & point(A3) & point(B1) & point(B2) & point(B3) & point(C1) & point(C2) & point(C3) & point(A4) & point(A5) & point(A6) & point(B4) & point(B5) & point(B6) & point(C4) & point(C5) & point(C6) & angle_add(A1,A2,A3,B1,B2,B3,C1,C2,C3) & angle_add(A4,A5,A6,B4,B5,B6,C4,C5,C6) & cong_angle(A1,A2,A3,A4,A5,A6) & cong_angle(C1,C2,C3,C4,C5,C6)) => (cong_angle(B1,B2,B3,B4,B5,B6))))).
> 		
> 
> % angle A1A2A3 + angle B1B2B3 = angle C1C2C3 &
> % angle A4A5A6 + angle B4B5B6 = angle C4C5C6 &
> % angle B1B2B3 = angle B4B5B6                &
> % angle C1C2C3 = angle C4C5C6                =>
> % angle A1A2A3 = angle A4A5A6                
> 
> 
> fof(ax_angle_add8, axiom, (![A1,A2,A3,B1,B2,B3,C1,C2,C3,A4,A5,A6,B4,B5,B6,C4,C5,C6] : ((point(A1) & point(A2) & point(A3) & point(B1) & point(B2) & point(B3) & point(C1) & point(C2) & point(C3) & point(A4) & point(A5) & point(A6) & point(B4) & point(B5) & point(B6) & point(C4) & point(C5) & point(C6) & angle_add(A1,A2,A3,B1,B2,B3,C1,C2,C3) & angle_add(A4,A5,A6,B4,B5,B6,C4,C5,C6) & cong_angle(B1,B2,B3,B4,B5,B6) & cong_angle(C1,C2,C3,C4,C5,C6)) => (cong_angle(A1,A2,A3,A4,A5,A6))))).
> 
> 
> 		
> 
> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
> % CONG_AREA_ZERO, reflexivity, symmetry, transitivity  %
> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
