1 Jun 2012 06:17

### Re: rigorous axiomatic geometry proof in HOL Light

```   Yes, this may be the core problem: the default built-in miz3 prover
doesn't know much about sets [...] SET_TAC [...] it may make sense
for us to improve the default miz3 prover

Thanks, John!  Maybe we don't have to improve miz3 for my set theory
needs, but instead, I need to rewrite some definitions.  Details:

1) Searching for SET_TAC , and found new set theorems IN_SING,
SING_SUBSET, MEMBER_NOT_EMPTY in sets.ml and got rid of three of mine!

2) sets.ml shows how DELETE & IN_DELETE (which I use in my code) work:

parse_as_infix("DELETE",(21,"left"));;

let DELETE = new_definition
`s DELETE x = {y:A | y IN s /\ ~(y = x)}`;;

let IN_DELETE = prove
(`!s. !x:A. !y. x IN (s DELETE y) <=> x IN s /\ ~(x = y)`,
REWRITE_TAC[IN_ELIM_THM; DELETE]);;

3) Why can't I do that?  I prove theorems ConverseCrossbar_THM &
WholeRayInterior_THM (code included below) using

let Ray_DEF = new_definition
`!A B X.  ray(X, A, B) <=> ~(A = B) /\ Collinear(A, B, X) /\ ~ Between(X, A, B)`;;

let InteriorAngle_DEF = new_definition
`!A O B P.
int_angle(P, A, O, B) <=> ~ Collinear(A, O, B) /\ ?a b.
```
(Continue reading)

1 Jun 2012 18:27

### Re: rigorous axiomatic geometry proof in HOL Light

```
Hi Bill,

| I'm really happy these two proofs worked, because now I know I can
| code up my Hilbert axiom paper.  But I'd prefer (change ray to rag):
|
| let Rag_DEF = new_definition
|   `!A B.  rag(A, B) = if (A = B) {} else {X | Collinear(A, B, X) /\ ~ Between(X, A, B)`;;
|
| let IN_RAG = prove
|  (`!A. !X:point. !B. X IN rag(A, B) <=> ~(A = B)  /\ Collinear(A, B, X) /\ ~ Between(X, A, B)`,
|   REWRITE_TAC[IN_ELIM_THM; DELETE]);;
|
| Ray_DEF worked but IN_RAY gave the error message
|
| Exception: Failure "term after binary operator expected".

Are you sure there isn't a cut-and-paste error, or that the problem
wasn't actually with Ray_DEF? On the face of it your if-then-else
expression is missing a "then" and shouldn't parse.

| I'm so ignorant, I'm not surprised, so I tried a stunt from sets.ml:
|
| let IN_RAG = prove
|  (`!A. !X:point. !B. X IN rag(A, B) <=> ~(A = B)  /\ Collinear(A, B, X) /\ ~ Between(X, A, B)`,
|   REWRITE_TAC[IN_ELIM_THM; DELETE] THEN SET_TAC[]);;

The basic issue here is that SET_TAC (in common with the other
built-in HOL inference rules and tactics) never implicitly uses
definitions, so you need to either expand them or supply them as
```
(Continue reading)

3 Jun 2012 01:20

### Re: miz3 semantics discussion

```Freek, your advice about exec GOAL_TAC; p();; helped me solve a
skeleton error that was really bugging me (fixed code below), and I
think you taught me something really valuable about variable scope.

I thought we could rebind variables (with consider) in the body of a
proof environment, and I realized we can't.  So my proof worked fine
after I changed the conflicting variable names.  Look at this snippet:

consider a' b' such that
O IN a' /\ A IN a' /\ O IN b' /\B IN b' /\
~(D IN a') /\ ~(D IN b') /\
D,B same_side a' /\ D,A same_side b' [existsa'b'] by H2, InteriorAngle_DEF;
a' = a /\ b' = b by Distinct, a_OA, b_OB, existsa'b', I1;
[...]
~(D int_angle B,O,A') [notD_BOA']
proof
assume D int_angle B,O,A';
consider a' b' such that
O IN a' /\ A' IN a' /\ O IN b' /\B IN b' /\
~(D IN a') /\ ~(D IN b') /\
D,B same_side a' /\ D,A' same_side b' [X1] by -, InteriorAngle_DEF;
exec GOAL_TAC;
b' = b by Distinct, b_OB, X1, I1;
~(D IN b) /\ D,A' same_side b by -, X1;
qed by -;

I got a skeleton error on the line before exec GOAL_TAC;.
You can see the problem right off, but I realize it after
p();;

```
(Continue reading)

2 Jun 2012 16:52

### SSLST 2012: 3rd announcement

*********************************************************************

2012 INTERNATIONAL SUMMER SCHOOL IN LANGUAGE AND SPEECH TECHNOLOGIES

SSLST 2012

(formerly InternationalPhDSchool in Language and Speech Technologies)

Tarragona, Spain

July 30 – August 3, 2012

Organized by:

Research Group on Mathematical Linguistics (GRLMC)

Rovira i Virgili University

http://grammars.grlmc.com/sslst2012/

*********************************************************************

AIM:

SSLST 2012 offers a broad and intensive series of lectures at different levels on language and speech technologies. The students choose their preferred courses according to their interests and background. Instructors are top names in their respective fields. The School intends to help students initiate and foster their research career.

The previous event in this series was WSLST 2012: http://grammars.grlmc.com/wslst2012/

ADDRESSED TO:

Graduate (and advanced undergraduate) students from around the world. Most appropriate degrees include: Computer Science and Linguistics. Other students (for instance, from Mathematics, Electrical Engineering, Philosophy, or Cognitive Science) are welcome too.

The School is appropriate also for people more advanced in their career who want to keep themselves updated on developments in the field.

There is no overlap in the class schedule.

COURSES AND PROFESSORS:

- Jont B. Allen (U Illinois Urbana-Champaign), A Parametric Analysis of Speech Perception [introductory, 8 hours]

- Hervé Bourlard (Idiap Research Institute, Martigny), Automatic Speech Recognition and Multilingual Speech Processing: HMM, Hybrid HMM/ANN and Posterior-based Systems [introductory/intermediate, 6 hours]

- Marcello Federico (Bruno Kessler Foundation, Trento), Statistical Machine Translation [introductory/intermediate, 6 hours]

- Giuseppe Riccardi (U Trento), Spoken Language Understanding [intermediate/advanced, 6 hours]

- Noah A. Smith (Carnegie Mellon U), Probability and Structure in Natural Language Processing [intermediate, 9 hours]

- Bayya Yegnanarayana (International Institute of Information Technology Hyderabad), Speech Signal Processing [introductory/intermediate, 8 hours]

REGISTRATION:

It has to be done on line at

http://grammars.grlmc.com/sslst2012/Registration.php

FEES:

They are variable, depending on the number of courses each student takes. The rule is:

1 hour =

- 10 euros (for payments until May 18, 2012),

- 15 euros (for payments after May 18, 2012).

PAYMENT PROCEDURE:

The fees must be paid to the School's bank account:

Uno-e Bank

bank’s address: Julian Camarillo 4 C, 28037 Madrid, Spain

IBAN: ES3902270001820201823142

BIC/SWIFT code: UNOEESM1

account holder: Carlos Martin-Vide GRLMC

account holder’s address: Av. Catalunya 35, 43002 Tarragona, Spain

Please mention SSLST 2012 and your name in the subject. A receipt will be provided on site.

Remarks:

- Bank transfers should not involve any expense for the School.

- People claiming early registration will be requested to prove that the bank transfer order was carried out by the deadline.

- Students may be refunded only in the case when a course gets cancelled due to the unavailability of the instructor.

People registering on site at the beginning of the School must pay in cash. For the sake of local organization, however, it is much recommended to do it earlier.

ACCOMMODATION:

Information about accommodation is available on the website of the School.

CERTIFICATE:

Students will be delivered a certificate stating the courses attended, their contents, and their duration.

IMPORTANT DATES:

Announcement of the programme: April 12, 2012

Starting of the registration: April 12, 2012

Early registration deadline: May 18, 2012

Starting of the School: July 30, 2012

End of the School: August 3, 2012

QUESTIONS AND FURTHER INFORMATION:

Lilica Voicu:

florentinalilica.voicu <at> urv.cat

WEBSITE:

http://grammars.grlmc.com/sslst2012/

POSTAL ADDRESS:

SSLST 2012

Research Group on Mathematical Linguistics (GRLMC)

Rovira i Virgili University

Av. Catalunya, 35

43002 Tarragona, Spain

Phone: +34-977-559543

Fax: +34-977-558386

ACKNOWLEDGEMENTS:

Diputació de Tarragona

Universitat Rovira i Virgili

```------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/```
```_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
```
3 Jun 2012 12:37

### Turing Centenary Conference, Manchester, June 22-25: Call for Participation

```THE TURING CENTENARY CONFERENCE
Manchester, UK, June 22-25, 2012
http://www.turing100.manchester.ac.uk/

Call for Participation

NEWS:
(1) The early registration deadline has been extended to
June 11, 2012
(2) The organisers have funds for supporting participants.
Please write to the programme chair if support is
essential for your attendance.

The programme includes 18 invited talks (of which 10 are given
by Turing Award winners), 2 public talks, 2 panels, a poster
session, a chess programme and a competition of programs
proving theorems.

Public lectures:

-- Jack Copeland (University of Canterbury, New Zealand)
Alan Turing, Pioneer of the Information Age
-- Sir Roger Penrose (University of Oxford, Wolf Prize winner)
The Problem of Modelling the Mathematical Mind

Invited lectures:

-- Garry Kasparov (Kasparov Chess Foundation)
The Reconstruction of Turing's "Paper Machine"
-- Vint Cerf (Google, Turing Award winner)
Turing's Legacy in the Networked World
-- David Ferrucci (IBM)
Beyond Jeopardy! The Future of Watson
-- Don Knuth (Stanford University, Turing Award winner)
All Remaining Questions Answered
-- Adi Shamir (Weizmann Institute of Science, Turing Award winner)
Turing's Cryptography from a Modern Perspective
-- Samuel Klein (Wikipedia)
TBC
-- George Ellis (University of Cape Town, Templeton Award winner)
On the Nature of Causation in Digital Computer Systems
-- Frederick P. Brooks, Jr. (University of North Carolina, Turing Award winner)
Pilot ACE Architecture in Context
-- Sir Tony Hoare (Microsoft Research, Turing Award winner)
Can Computers Understand Their Own Programs?
-- Edmund M. Clarke (Carnegie Mellon University, Turing Award winner)
Model Checking and the Curse of Dimensionality
-- Michael O. Rabin (Harvard University, Turing Award winner)
Turing, Church, GÃ¶del, Computability, Complexity and
Randomization: A Personal Perspective
-- Leslie Valiant (Harvard University, Turing Award winner)
Computer Science as a Natural Science
-- Andrew Chi-Chih Yao (Tsinghua University, Turing Award winner)
Quantum Computing: A Great Science in the Making
-- Manuela M. Veloso (Carnegie Mellon University)
Symbiotic Autonomy: Robots, Humans, and the Web
-- Rodney Brooks (MIT)
Turing's Humanoid Thinking Machines
-- Hans Meinhardt (Max Planck Institute for Developmental Biology)
Turing's Pioneering Paper 'The Chemical Basis of Morphogenesis
and the Subsequent Development of Theories of Biological Pattern
Formation
-- Yuri Matiyasevich (Institute of Mathematics, St. Petersburgh)
Alan Turing and Number Theory

Panel speakers:
-- Samson Abramsky (Oxford University)
-- Ron Brachman (Yahoo Labs)
-- Martin Davis (New York University)
-- Steve Furber (The University of Manchester)
-- Carole Goble (The University of Manchester)
-- Pat Hayes (Institute for Human and Machine Cognition, Pensacola)
-- Bertrand Meyer (Swiss Federal Institute of Technology)
-- Moshe Vardi (Rice University)

For more details please check
http://www.turing100.manchester.ac.uk/.

REGISTRATION:

The number of participants is limited. Register early to avoid
disappointment! To register, access
https://www.easychair.org/conferences/?conf=turing100 and click on
"Registration".

*** Registration fees ***

All fees are in Pound Sterling.

early (on or before June 11)	 late (June 12 or later)
Student	                280                      330
Regular                 380                      450

To qualify for a student registration you must be a registered
full-time student on June 23, 2012.

The registration fees include

- Attendance of sessions
- Conference reception
- Conference dinner
- Coffee breaks and lunches
- Poster session proceedings

CHAIRS:

Honorary Chairs:
Rodney Brooks (MIT)
Roger Penrose (Oxford)
Conference Chairs:
Matthias Baaz (Vienna University of Technology)
Andrei Voronkov (The University of Manchester)
Turing Fellowships Chair:
Barry Cooper (University of Leeds)
Theorem Proving Competition Chair:
Geoff Sutcliffe (University of Miami)
Computer Chess Programme Chair
Frederic Friedel (Chessbase)
Programme Chair
Andrei Voronkov (The University of Manchester)

-------------------------------------------------------------------
The Alan Turing Year:
http://www.turingcentenary.eu/
-------------------------------------------------------------------

```
```------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/```
```_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
```
3 Jun 2012 15:25

### CFP SYNASC 2012, Timisoara, Romania

```
[Please post - apologies for multiple copies.]

Call for Papers
----------------
SYNASC 2012
14th International Symposium on
Symbolic and Numeric Algorithms for Scientific Computing

~~ In honor of Professor Bruno Buchberger's 70th birthday and of
Professor Stefan Maruster's 75th birthday ~~

September 26-29, 2012, Timisoara, Romania
http://synasc12.info.uvt.ro/

Aim
---

SYNASC aims to stimulate the interaction between the two scientific communities of symbolic and numeric
computing and to exhibit interesting applications of the areas both in theory and in practice. The choice of
the topic is motivated by the belief of the organizers that the dialogue between the two communities is very
necessary for accelerating the progress in making the computer a truly intelligent aid for
mathematicians
and engineers.

Important Dates
---------------

17 June 2012            :  Abstract submission (Extended deadline)
24 June 2012            :  Paper submission
01 August 2012          :  Notification of acceptance
01 September 2012       :  Registration
08 September 2012       :  Revised papers according to the reviews
26-29 September 2012    :  Symposium
18 November 2012        :  Final papers for post-proceedings

Tracks
------
* Symbolic Computation
* Numerical Computing
* Logic and Programming
* Distributed Computing
* Artificial Intelligence
* Advances in the Theory of Computing

Invited Speakers
----------------
* Bruno Buchberger, Johannes Kepler University, Linz, Austria
* Sumit Gulwani, Microsoft Research, Redmond, USA
* Tetsuo Ida, University of Tsukuba, Japan
* Michael Kohlhase, Jacobs University Bremen, Germany
* Sascha Ossowski, Rey Juan Carlos University Madrid, Spain
* Paul Tarau, University of North Texas, USA

Workshops  -  http://synasc12.info.uvt.ro/workshops/
---------
* ACSys 2012 - Workshop on Agents for Complex Systems
* IAFP 2012 - Workshop on Iterative Approximation of Fixed Points
* MICAS 2012 - Workshop on Management of Resources and Services in Cloud and Sky Computing
* NCA 2012 - Workshop on Natural Computing and Applications
* WOHS 2012 - Workshop of HPC Services

Tutorials  -  http://synasc12.info.uvt.ro/tutorials
---------
* MPI Tutorial
- James Davenport, University of Bath, UK
* Globus Tutorial for Administrators and Users
- Ioan Lucian Muntean, Technical University of Cluj Napoca, Romania
* Computing with numbers and symbols in a bio-inspired framework: Membrane Computing
- Gheorghe Paun, Romanian Academy & University of Sevilla, Spain
* Programming Language Design and Analysis using the K Framework
- Dorel Lucanu, "Al. I. Cuza” University of Iasi, Romania
- Traian-Florin Serbanuta, University of Illinois at Urbana-Champaign, USA &
"Al.I.Cuza"
University of Iasi, Romania

Publication
-----------
The research papers accepted and presented at the symposium are
collected in post-proceedings published by Conference Publishing Service (CPS) (ISI Proceedings). For
previous proceedings see http://ieeexplore.ieee.org.

The SYNASC post-proceedings will be submitted for indexing to: ISI Web of Knowledge,
ACM Digital Library, EI Compendex, DBLP, SCOPUS.

Submission
-----------

Submissions of research papers are invited. The papers must contain
original research results not submitted and not published elsewhere.

The submission process consists of two steps.

* In the first step the authors are invited to express their
intention to participate at the conference by submitting a short
abstract (1/2 page, at maximum) where it is clearly stated the main
contribution(s) of the paper.

* In the second step the authors should submit the full paper
(up to 8 pages in the two-columns IEEE conference style).

Both the abstract and the full paper should be submitted electronically
through http://www.easychair.org/conferences/?conf=synasc2012.

Honorary Chairs
---------------
* Bruno Buchberger, Johannes Kepler University, Austria
* Stefan Maruster, West University of Timisoara, Romania

General Chair
-------------
* Viorel Negru, West University of Timisoara, Romania

Program Chair
-------------
* Andrei Voronkov, Manchester University, UK

Steering Committee
------------------
* Tetsuo Ida, University of Tsukuba, Japan
* Tudor Jebelean, Johannes Kepler University, Austria
* Viorel Negru, West University of Timisoara, Romania
* Dana Petcu, West University of Timisoara, Romania
* Stephen Watt, University of Western Ontario, Canada
* Daniela Zaharie, West University of Timisoara, Romania

Track Chairs
------------
* Symbolic Computation
+ Tetsuo Ida, University of Tsukuba, Japan
+ Stephen Watt, University of Western Ontario, Canada

* Numerical Computing
+ Yonghong Yao, Tianjin Polytechnic University, China
+ Ioan A. Rus, “Babes-Bolyai” University of Cluj-Napoca, Romania

* Logic and Programming
+ Tudor Jebelean, Johannes Kepler University, Austria
+ Laura Kovacs, Vienna University of Technology, Austria
+ Nikolaj Bjorner, Microsoft

* Distributed Computing
+ Dana Petcu, West University of Timisoara, Romania
+ Karoly Bosa, Johannes Kepler University, Austria

* Artificial Intelligence
+ Siby Abraham, University of Mumbay, India
+ Daniela Zaharie, West University of Timisoara, Romania

* Advances in the Theory of Computing
+ Mircea Marin, West University of Timisoara, Romania
+ Gabriel Istrate, Research Institute e-Austria Timisoara,Romania

Workshops chair
---------------
* Laura Kovacs, Vienna University of Technology, Austria

Tutorial chair
--------------
* Dana Petcu, West University of Timisoara, Romania

Proceedings Chairs
------------------
* Andrei Voronkov, Manchester University, UK
* Daniela Zaharie, West University of Timisoara, Romania

Local Committee Chairs
----------------------
* Isabela Dramnesc, West University of Timisoara, Romania
* Silviu Panica, Institute e-Austria Timisoara, Romania

-----------
SYNASC 2012
West University of Timisoara
Department of Computer Science
Bd. V. Parvan 4, 300223 Timisoara, Romania
tel: + (40) 256 592155
fax: + (40) 256 592316
e-mail: synasc12 <at> info.uvt.ro

------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
```
1 Jun 2012 12:46

### GAMES 2012 -- Call for contributions --

```[We apologize if you have received multiple copies of this message]

================================================================

GAMES 2012 - CALL FOR CONTRIBUTIONS

Annual Workshop of the ESF Networking Programme on

Games for Design and Verification

7th - 12th September 2012 - Napoli, Italy

http://www.games.unina.it/

================================================================

The ESF Networking Programme on Games for Design and Verification is a
European Network pursuing research and training on the design and
verification of computing systems. This network proposes a research
and training programme for the design and verification of computing
systems, using a methodological framework that is based on the
interplay of finite and infinite games, mathematical logic and
automata theory. For details, see www.games.rwth-aachen.de/

GAMES is the annual workshop of the Network and this year edition is the
concluding one.

GAMES 2012 will be held at Universita' di Napoli Federico II, Italy.

SCOPE:
The scope of the workshop includes the mathematical and algorithmic
analysis of finite and infinite games, the interplay of games with
automata theory and logic, and applications of games, automata, and
logic to the design and verification of computing systems.

PROGRAMME:
As in previous years, GAMES 2012 will be an informal workshop, without
proceedings. Its programme consists of 10 invited talks,
contributed talks (30 min) and short presentations (15 min).
Contributed talks and short presentations will be selected by the
programme committee on the basis of submitted abstracts.

INVITED SPEAKERS:

- Mikolaj Bojanczyk (Warsaw University, Poland)
- Krishnendu Chatterjee (IST Vienna, Austria)
- Thomas Colcombet (CNRS Paris, France)
- Olivier Friedman (University of Munich, Germany)
- Hugo Gimbert (CNRS, France)
- Joseph Halpern (Cornell University, USA)
- Damian Niwinsky (Warsaw University, Poland)
- Luke Ong  (Oxford University, UK)
- Jean-François Raskin (Université Libre de Bruxelles, Belgium)
- Wolfgang Thomas (RWTH Aachen University, Germany)

SUBMISSIONS:
Researchers who would like to present a talk at GAMES 2012 are invited
to submit an abstract of up to two pages by email to

esfgames2012 <at> gmail.com

by 27 June 2012.
Decisions about acceptance will be made by 17 July 2012.

IMPORTANT DATES:
Abstract submission:        June 27th 2012
Author notification:        July 17th 2012
Travel grant application:   July 30th 2012
Regular registration:       July 30th 2012
Workshop:                   September 7th - 12th 2012

TRAVEL SUPPORT:
We will be able to cover travel and accommodation costs for a limited
number of participants (especially students). For information, please
contact Aniello Murano via <esfgames2012 <at> gmail.com>.
There will be no registration fee.

LOCATION:
The workshop will be held at the Centro Congressi Ateneo Federico II,
Via Partenope 36, Napoli, located on a wonderful seafront promenade, close
to the historical center and the Castel dell'Ovo. The location is just in
front of the baia that hosted last America's Cup World Competition.

PROGRAMME COMMITTEE:
- Krzysztof Apt, CWI and University of Amsterdam, The Netherlands
- Dietmar Berwanger, CNRS and ENS Cachan, France
- Erich Grädel, RWTH Aachen University, Germany
- Christof Löding, RWTH Aachen University, Germany
- Angelo Montanari, University of Udine, Italy
- Aniello Murano, Università di Napoli, Italy (Main Organizer)
- Mimmo Parente, Univerità di Salerno, Italy
- Sven Shewe, University of Liverpool, UK
- Igor Walukiewicz, Université Bordeaux 1, France

CO-LOCATED EVENTS:
GandALF 2012 - Third International Symposium on Games, Automata, Logics,
and Formal Verification - www.gandalf.unina.it/ - September 6th-8th, 2012

INFO:
Please visit the workshop website (http://www.games.unina.it) for more
information.

------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
```
4 Jun 2012 15:41

### Re: Problem building HOL Light

```I have just tried to install HOL Light, but seem to be encountering a version of the problem documented in
this thread.

I would be grateful for any advice - particularly if it had newbie-granularity.

I have camlp4 installed as well as camlp5 now, but don't see any signs of their interference.  Do I have any
reason to have both, or should I uninstall camlp4?

Thank you in advance,

Colin Rowat
University of Birmingham

System: Ubuntu 12.04 running on an 64-bit Intel CORE i7 vPro
Used Synaptic to install camlp4 (v.3.12.1), camlp5, ocaml  (v.3.12.1)
Used SVN to checkout HOL Light (rev 146)
Found a "Error 2" in Make that seemed to interfere with HOL Light's parsing
Found this thread, so used Synaptic to uninstall camlp5
Downloaded camlp5-6.06 to Desktop and then:

\$ make clean
\$ ./configure --strict
\$ make world.opt
\$ sudo make install

>From hol_light directory:

\$ make clean
\$ make

with this last command yielding:

<begins>
\
if test `ocamlc -version | cut -c3` = "0" ; \
then cp pa_j_`ocamlc -version | cut -c1-4`.ml pa_j.ml ; \
else if test `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -c1-6` = "6.02.1" ; \
then cp pa_j_3.1x_6.02.1.ml pa_j.ml; \
else if test `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -c1-6` = "6.02.2" -o `camlp5 -v 2>&1 | cut -f3
-d' ' | cut -f1-3 -d'.' | cut -c1-6` = "6.02.3" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -c1-6` =
"6.05" ; \
then cp pa_j_3.1x_6.02.2.ml pa_j.ml; \
else cp pa_j_3.1x_`camlp5 -v 2>&1 | cut -f3 -d' ' | cut -c1`.xx.ml pa_j.ml; \
fi \
fi \
fi
if test `ocamlc -version | cut -c3` = "0" ; \
then ocamlc -c -pp "camlp4r pa_extend.cmo q_MLast.cmo" -I +camlp4 pa_j.ml; \
else ocamlc -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo" -I +camlp5 pa_j.ml; \
fi
File "pa_j.ml", line 195, characters 6-21:
Error: The constructor PaLab expects 2 argument(s),
but is applied here to 3 argument(s)
make: *** [pa_j.cmo] Error 2
<ends>

The relevant line of pa_j.ml reads:

<begins>
| PaLab loc x1 x2 ->
<ends>
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
```
4 Jun 2012 16:52

### Postdoc Position on Coverage Analysis of Concurrent Specification Languages, Inria/LIG, Grenoble, France

```
The Convecs team (Inria Grenoble Rhône-Alpes research center / LIG
laboratory) recruits a postdoc. More information at:

http://convecs.inria.fr/jobs/2012d.html

Applications should be addressed directly to Gwen Salaün, preferably
by e-mail. Applications received after July 15st, 2012 might not be
considered if a candidate has been selected already.

```
```------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/```
```_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
```
5 Jun 2012 05:54

### Re: rigorous axiomatic geometry proof in HOL Light

```John, I made big progress on our set theory problem!  700+ lines of
code below.  I just reference `IN', the first definition in sets.ml

let IN = new_definition
`!P:A->bool. !x. x IN P <=> P x`;;

So I define `ray' as a curried function

let Ray_DEF = new_definition
`!A B X. ray (A,B) X <=> ~(A = B) /\ Collinear(A, B, X) /\ ~Between(X, A, B)`;;

and later I can write, as if a ray was a set,

G IN ray(O,D) [G_OD] by DnotO, ODGcol, -, IN, Ray_DEF;

I can then even ``intersect'' rays with other sets using INTER.  I'm
really happy about this!  It's not everything I wanted (yet), but it
should be all the set theory I need to code up my Hilbert paper.

--
best,
Bill

(*
Paste in these 2 commands:			(setq case-fold-search nil)
cd ~/hol_light; ocaml
#use "hol.ml";;
then paste in the following file*)

(* ================================================================= *)
(* HOL Light Hilbert geometry axiomatic proofs. *)
(* ================================================================= *)

(* Thanks to Mizar folks who wrote an influential language I was able
to learn, Freek Wiedijk, who wrote the miz3 port of Mizar to HOL
Light, and especially John Harrison, who came up with the entire
framework here of porting my axiomatic proofs to HOL Light.       *)

new_type("point",0);;
new_type_abbrev("line",`:point->bool`);;
new_constant("Between",`:point#point#point->bool`);;
new_constant("===",`:point#point->point#point->bool`);;
parse_as_infix("===",(12, "right"));;
parse_as_infix("cong",(12, "right"));;
parse_as_infix("same_side",(12, "right"));;
parse_as_infix("int_angle",(12, "right"));;

let cong_DEF = new_definition
`A,B,C cong X,Y,Z <=>
A,B === X,Y /\ A,C === X,Z /\ B,C === Y,Z`;;

let is_ordered_DEF = new_definition
`is_ordered (A,B,C,D) <=>
Between (A,B,C) /\ Between (A,B,D) /\ Between (A,C,D) /\ Between (B,C,D)`;;

let Collinear_DEF = new_definition
`Collinear(A, B, C)  <=>
?l:line. A IN l /\ B IN l /\ C IN l`;;

let Twiddle_DEF = new_definition
`Twiddle A l B <=>
~(?X. (X IN l) /\ Between(A, X, B))`;;

let same_side_DEF = new_definition
`A,B same_side l <=>
~(?X. (X IN l) /\ Between(A, X, B))`;;

let Reflexive_relation_DEF = new_definition
`Reflexive_Property <=>
!l:line A:point. ~(A IN l) ==> A,A same_side l`;;

let Symmetric_relation_DEF = new_definition
`Symmetric_Property <=>
!l:line A:point B:point. ~(A IN l) /\ ~(B IN l) ==>
A,B same_side l ==> B,A same_side l`;;

let Transitive_relation_DEF = new_definition
`Transitive_Property <=>
!l:line A:point B:point C:point.
~(A IN l) /\ ~(B IN l) /\ ~(C IN l) ==>
A,B same_side l /\ B,C same_side l ==> A,C same_side l`;;

let Ray_DEF = new_definition
`!A B X. ray (A,B) X <=> ~(A = B) /\ Collinear(A, B, X) /\ ~Between(X, A, B)`;;

(*
exec GOAL_TAC;
p();;

let Angle_DEF = new_definition
`!A O B. Angle(A, O, B) = if Collinear(A, O, B) then {} else
{ray(O, A), ray(O, B)}`;;
*)

let InteriorAngle_DEF = new_definition
`!A O B P.
P int_angle A,O,B <=> ~Collinear(A, O, B) /\ ?a b.
O IN a /\ A IN a /\ O IN b /\ B IN b /\
~(P IN a) /\ ~(P IN b) /\ P,B same_side a /\ P,A same_side b`;;

(* ------------------------------------------------------------------------- *)
(* The axioms.                                                               *)
(* ------------------------------------------------------------------------- *)

let I1 = new_axiom
`!A B.  ~(A = B) ==> ?! l. A IN l /\ B IN l`;;

let I2 = new_axiom
`!l. ? A B. A IN l /\ B IN l /\ ~(A = B)`;;

let I3 = new_axiom
`?A:point B:point C:point. ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ ~Collinear(A, B, C)`;;

let B1 = new_axiom
`! A B C. Between(A, B, C) ==> ~(A = B) /\ ~(A = C) /\ ~(B = C) /\
Between(C, B, A) /\ Collinear(A, B, C)`;;

let B2 = new_axiom
`! A B. ~(A = B) ==> ?C. Between(A, B, C)`;;

let B3 = new_axiom
`!A B C. ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ Collinear(A, B, C)
==> (Between(A, B, C) \/ Between(B, C, A) \/ Between(C, A, B)) /\
~(Between(A, B, C) /\ Between(B, C, A)) /\
~(Between(A, B, C) /\ Between(C, A, B)) /\
~(Between(B, C, A) /\ Between(C, A, B))`;;

let B4 = new_axiom
`!l A B C. ~Collinear(A, B, C) ==>
!l. ~(A IN l) /\ ~(B IN l) /\ ~(C IN l) ==>
(?X. X IN l /\ Between(A, X, C)) ==>
(?Y. Y IN l /\ Between(A, Y, B)) \/
(?Y. Y IN l /\ Between(B, Y, C))`;;

#load "unix.cma";;
loadt "miz3/miz3.ml";;

horizon := 0;;

let BiggerThanSingleton_THM = thm `;
let p be A->bool;
let x be A;
assume x IN p                                                         [H1];
assume ~(p = {x})                                                     [H2];
thus ?a . a IN p /\ ~(a = x)

proof
{x} SUBSET p by H1, SING_SUBSET;
~(p SUBSET {x}) by -,  H2, SUBSET_ANTISYM;
consider a such that
a IN p /\ ~(a IN {x})                       [X1] by -, SUBSET;
~(a = x) by -, IN_SING;
qed by -, X1`;;

let DisjointOneNotOther_THM = thm `;
let x be A;
let l m be A->bool;
assume l INTER m = {}                                                 [H1];
assume x IN m                                                         [H2];
thus ~(x IN l)

proof
assume (x IN l);
x IN l INTER m by -, H2, IN_INTER;
F by -, NOT_IN_EMPTY, H1;
qed by -`;;

let IntersectionSingletonOneNotOther_THM = thm `;
let e x be A;
let l m be A->bool;
assume l INTER m = {x}                                                [H1];
assume e IN l                                                         [H2];
assume ~(e = x)                                                       [H3];
thus ~(e IN m)

proof
assume e IN m;
e IN l INTER m by H2, -, IN_INTER;
e = x by -, H1, IN_SING;
F by -, H3;
qed by -`;;

let EquivIntersectionHelp_THM = thm `;
let a x be A;
let l m be A->bool;
assume l INTER m = {x}                                                [H1];
assume a IN m DELETE x                                                [H2];
thus ~(a IN l)

proof
a IN m /\ ~(a = x)                          [X1] by H2, IN_DELETE;
qed by -, H1, H2, IntersectionSingletonOneNotOther_THM`;;

let OnePointImpliesAnother_THM = thm `;
let P be point;
thus ?Q:point. ~(Q = P)

proof
consider A B C such that
~(A = B) /\ ~(A = C) /\ ~(B = C) /\ ~Collinear(A, B, C) [X1] by I3;
cases;
suppose B = P;
~(A = B) by -, X1;
qed by -;
suppose ~(B = P);
qed by -;
end`;;

let ExistsPointOffLine_THM = thm `;
let l be line;
thus ?Q:point. ~(Q IN l)

proof
consider A B C such that
~(A = B) /\ ~(A = C) /\ ~(B = C) /\ ~Collinear(A, B, C) [useI3] by I3;
cases;
suppose ~(A IN l) \/ ~(B IN l) \/ ~(C IN l);
qed by -;
suppose (A IN l) /\ (B IN l) /\ (C IN l);
Collinear(A, B, C) by -, Collinear_DEF;
F by -, useI3;
qed by -;
end`;;

let B4'_THM = thm `;
let l be line;
let A B C be point;
assume ~Collinear(A, B, C) /\ ~(A IN l) /\ ~(B IN l) /\ ~(C IN l)     [H1];
assume A,B same_side l /\ B,C same_side l                             [H2];
thus A,C same_side l

proof
~(?Y. Y IN l /\ Between(A, Y, B)) /\
~(?Y. Y IN l /\ Between(B, Y, C)) ==>
~(?X. X IN l /\ Between(A, X, C))  by H1, B4;
qed by -, H1, H2, same_side_DEF`;;

let BetweenLinear_THM = thm `;
let A B C be point;
let m be line;
assume A IN m /\ C IN m                                               [H1];
assume Between(A, B, C) \/ Between(B, C, A)  \/ Between(C, A, B)      [H2];
thus B IN m

proof
~(A = C) /\
(Collinear(A,B,C) \/ Collinear(B,C,A) \/ Collinear(C,A,B))  [X1] by H2, B1;
consider l such that
A IN l /\ B IN l /\ C IN l                  [X2] by -, Collinear_DEF;
l = m by X1, -, H2, H1, I1;
qed by -, X2`;;

let CollinearLinear_THM = thm `;
let A B C be point;
let m be line;
assume A IN m /\ C IN m                                               [H1];
assume Collinear(A,B,C) \/ Collinear(B,C,A) \/ Collinear(C,A,B)       [H2];
assume ~(A = C)                                                       [H3];
thus B IN m

proof
consider l such that
A IN l /\ B IN l /\ C IN l                  [X1] by H2, Collinear_DEF;
l = m by H3, -, H1, I1;
qed by -, X1`;;

let NonCollinearImpliesDistinct_THM = thm `;
let A B C be point;
assume ~Collinear(A, B, C)                                            [H1];
thus ~(A = B) /\ ~(A = C) /\ ~(B = C)

proof
cases;
suppose A = B /\ B = C                                              [C1];
consider Q such that ~(Q = A) by OnePointImpliesAnother_THM;
consider l such that A IN l /\ Q IN l by -, I1;
Collinear(A, B, C) by -, C1, Collinear_DEF;
qed by -, H1;
suppose ~(A = B) /\ B = C                                           [C2];
consider l such that A IN l /\ B IN l by -, I1;
Collinear(A, B, C) by -, C2, Collinear_DEF;
qed by -, H1;
suppose ~(B = C)                                                    [C3];
consider l such that B IN l /\ C IN l [X1] by C3, I1;
~(A = B)								[U]
proof
assume A = B;
Collinear(A, B, C) by -, X1, Collinear_DEF;
qed by -, H1;
~(A = C)								[V]
proof
assume A = C;
Collinear(A, B, C) by -, X1, Collinear_DEF;
qed by -, H1;
qed by U, V, C3;
end`;;

let OriginInRay_THM = thm `;
let O Q be point;
assume ~(Q = O)                               [H1];
thus O IN ray(O, Q)

proof
~Between (O,O,Q) [OOQ] by B1;
consider l such that
O IN l /\ Q IN l by H1, I1;
Collinear (O,Q,O) by -, Collinear_DEF;
O IN ray(O,Q) by H1, -, OOQ, IN, Ray_DEF;
qed by -`;;

let Line01infinity_THM = thm `;
let X be point;
let l m be line;
assume ~(l = m)                                                       [H1];
assume X IN l /\ X IN m                                               [H2];
thus l INTER m = {X}

proof
(l INTER m = {X}) \/ ~(l INTER m = {X});
assume ~(l INTER m = {X})                                           [H3];
X IN l INTER m by H2, IN_INTER;
consider A such that
A IN l INTER m  /\ ~(A = X)         [X1] by -, H3, BiggerThanSingleton_THM;
A IN l /\ X IN l /\ A IN m /\ X IN m by -, H2, IN_INTER;
l = m by -, X1, I1;
F by -, H1;
qed by -`;;

let EquivIntersection_THM = thm `;
let A B X be point;
let l m be line;
assume l INTER m = {X}                                                [H1];
assume A IN m DELETE X /\ B IN m DELETE X                             [H2];
assume ~ Between(A, X, B)                                             [H3];
thus  ~(A IN l) /\ ~(B IN l) /\ A,B same_side l

proof
A IN m /\ ~(A = X)                          [X1] by H2, IN_DELETE;
B IN m /\ ~(B = X)                          [X2] by H2, IN_DELETE;
~(A IN l) /\ ~(B IN l) [X3] by H1, H2, EquivIntersectionHelp_THM;
A,B same_side l                                                     [X4]
proof
assume ~(A,B same_side l);
consider G such that
(G IN l) /\ Between(A, G, B)              [X5] by -, same_side_DEF;

~(A = B) /\ Collinear(A, G, B)           [X6] by -, B1;
consider k such that
A IN k /\ G IN k /\ B IN k                [X7] by -, Collinear_DEF;
k = m by -, X1, X2, X6, I1;
G IN l INTER m by -, X5, X7, IN_INTER;
G = X by -, H1, IN_SING;
Between(A, X, B) by -, X5;
F by -, H3;
qed by -;
qed by X3, X4`;;

let SameSideReflexiveRelation_THM = thm `;
thus Reflexive_Property

proof
!l:line A:point. A,A same_side l
proof
let l be line;
let A be point;
~(?X. (X IN l) /\ Between(A, X, A)) by B1;
qed by -, same_side_DEF;
qed by -, Reflexive_relation_DEF`;;

let SameSideSymmetricRelation_THM = thm `;
thus Symmetric_Property

proof
!l:line A:point B:point. ~(A IN l) /\ ~(B IN l) ==>
A,B same_side l ==> B,A same_side l
proof
let l be line;
let A B be point;
assume A,B same_side l                                            [H1];
assume ~(A IN l) /\ ~(B IN l);
~(?X. (X IN l) /\ Between(A, X, B)) by H1, same_side_DEF;
~(?X. (X IN l) /\ Between(B, X, A)) by -, B1;
qed by -, same_side_DEF;
qed by -, Symmetric_relation_DEF`;;

let SameSideTransitiveRelation_THM = thm `;
thus Transitive_Property

proof
!l:line A:point B:point C:point.
~(A IN l) /\ ~(B IN l) /\ ~(C IN l) ==>
A,B same_side l /\ B,C same_side l ==> A,C same_side l
proof
let l be line;
let A B C be point;
assume ~(A IN l) /\ ~(B IN l) /\ ~(C IN l)                        [H0];
assume A,B same_side l                                            [H1];
assume B,C same_side l                                            [H2];
A,C same_side l
proof
~Collinear(A, B, C) \/ Collinear(A, B, C);
cases by -;
suppose ~Collinear(A, B, C);
qed by -, H0, H1, H2, B4'_THM;
suppose Collinear(A, B, C)                                      [Coll];
cases;
suppose A = B \/ A = C \/ B = C;
qed by -, H2, H0, SameSideReflexiveRelation_THM,
Reflexive_relation_DEF, H1;
suppose ~(A = B) /\ ~(A = C) /\ ~(B = C)      [Distinct];
consider m such that
A IN m /\ C IN m                            [W1] by Distinct, I1;
~(l = m)                                    [W2] by W1, H0;
cases;
suppose l INTER m = {}                      [Disjoint];
!X. Between(A, X, C) ==> ~(X IN l)
proof
let X be point;
assume Between(A, X, C);
X IN m by -, W1, BetweenLinear_THM;
~(X IN l) by -, Disjoint, DisjointOneNotOther_THM;
qed by -;
qed by -, same_side_DEF;
suppose ~(l INTER m = {})                   [NotDisjoint];
consider X such that
X IN l INTER m by NotDisjoint, MEMBER_NOT_EMPTY;
X IN l /\ X IN m                          [U1] by -, IN_INTER;
l INTER m = {X}           [U2] by W2, -, Line01infinity_THM;
consider E such that
E IN l /\ ~(E = X)                        [U3] by U1, I2;
~(E IN m) [U4] by U2, U3, IntersectionSingletonOneNotOther_THM;
~(E = B) by U3, H0;
consider B' such that
Between(E, B, B') by -, B2;
Between(B', B, E)                         [U5] by -, B1;
~(B' = E) /\ ~(B = E) /\ ~(B' = B) /\ Collinear(B', B, E) [U6] by -, B1;
consider n such that
E IN n /\ B' IN n                         [U7] by -, I1;
B IN n                    [U8] by U7, U5, BetweenLinear_THM;
~(l = n)                  [U9] by H0, -;
l INTER n = {E} [U10] by U9, U7, U3, Line01infinity_THM;
~(B' IN l) [U11] by -, U7, U6, IntersectionSingletonOneNotOther_THM;
~ Between(B, E, B')        [U12] by U6, U5, B3;
B' IN n DELETE E /\ B IN n DELETE E by U7, U8, U6, IN_DELETE;
B, B' same_side l [U13] by U10, -, U12, EquivIntersection_THM;
~(m = n)                   [U14] by  U7, U4;
B IN m by W1, Coll, Distinct, CollinearLinear_THM;
m INTER n = {B} [U15]  by -, U8, U14, Line01infinity_THM;
~(A IN n) [U16] by -, W1, Distinct, IntersectionSingletonOneNotOther_THM;
~Collinear(A, B, B') by U6, U7, U8, I1, U16, Collinear_DEF;
A,B' same_side l          [U17] by -, H0, U11, H1, U13, B4'_THM;
~(C IN n)                 [U18] by U15, W1, Distinct,
IntersectionSingletonOneNotOther_THM;
C,B same_side l [U19] by H0, H2, SameSideSymmetricRelation_THM,
Symmetric_relation_DEF;
~Collinear(C, B, B') by U6, U7, U8, I1, U18, Collinear_DEF;
C,B' same_side l by -, H0, U11, U19, U13, B4'_THM;
B',C same_side l [U20] by H0, U11, -, SameSideSymmetricRelation_THM,
Symmetric_relation_DEF;
~(B' IN m) [U21] by U15, U7, U6, IntersectionSingletonOneNotOther_THM;
~Collinear(A, B', C) by Distinct, W1, I1, U21, Collinear_DEF;
A, C same_side l by -, H0, U11, U17, U20, B4'_THM;
qed by -;
end;
end;
end;
qed by -;
qed by -, Transitive_relation_DEF`;;

let SameSideEquivalenceRelation_THM = thm `;
thus Reflexive_Property /\ Symmetric_Property /\ Transitive_Property
proof
qed by SameSideReflexiveRelation_THM, SameSideSymmetricRelation_THM,
SameSideTransitiveRelation_THM`;;

let ConverseCrossbar_THM = thm `;
let O A B G be point;
assume ~Collinear(A, O, B)						[H1];
assume Between(A, G, B)                       			[H2];
thus G int_angle A,O,B

proof
~(A = O) /\ ~(A = B) /\ ~(O = B) [Distinct] by H1,
NonCollinearImpliesDistinct_THM;
consider a such that O IN a /\ A IN a                         [aOA] by -, I1;
consider b such that O IN b /\ B IN b                  [bOB] by Distinct, I1;
consider l such that A IN l /\ B IN l                  [lAB] by Distinct, I1;
~(B IN a) by H1, aOA, Collinear_DEF;
~(a = l) by -, lAB;
a INTER l = {A}                     [alA] by -, aOA, lAB, Line01infinity_THM;
~(A = G) /\ ~(A = B) /\ ~(G = B) /\  Between(B, G, A) /\ Collinear(A, G, B)
[X1] by H2, B1;
~ Between(G, A, B)                                 [notGAB] by -, H2, B3, B1;
G IN l                                  [Ginl] by lAB, H2, BetweenLinear_THM;
~(G IN a)    [notGina] by alA, Ginl, X1, IntersectionSingletonOneNotOther_THM;
G IN l DELETE A /\ B IN l DELETE A by Ginl, lAB, X1, IN_DELETE;
G,B same_side a           [Gsim_aB] by alA, -, notGAB, EquivIntersection_THM;
:: same argument shows   G,A same_side b
~(A IN b) by H1, bOB, Collinear_DEF;
~(b = l) by -, lAB;
b INTER l = {B}                     [blB] by -, bOB, lAB, Line01infinity_THM;
~ Between(G, B, A)                  [notGBA] by H2, B1, B3;
~(G IN b)   [notGinb] by blB, Ginl, X1, IntersectionSingletonOneNotOther_THM;
G IN l DELETE B /\ A IN l DELETE B by Ginl, lAB, X1, IN_DELETE;
G,A same_side b            [Gsim_bA]by blB, -, notGBA, EquivIntersection_THM;
qed by H1, aOA, bOB, notGina, notGinb, Gsim_aB, Gsim_bA, InteriorAngle_DEF`;;

let InteriorHelp_THM = thm `;
let A O B P be point;
let a b be line;
assume O IN a /\ A IN a /\ O IN b /\ B IN b				[aOAbOB];
assume  P int_angle A,O,B						[P_AOB];
thus ~(P IN a) /\ ~(P IN b) /\ P,B same_side a /\ P,A same_side b

proof
consider alpha beta such that ~Collinear (A,O,B) /\
O IN alpha /\ A IN alpha /\ O IN beta /\B IN beta /\
~(P IN alpha) /\ ~(P IN beta) /\
P,B same_side alpha /\ P,A same_side beta [exists] by P_AOB, InteriorAngle_DEF;
~(A = O) /\ ~(A = B) /\ ~(O = B) [Distinct] by -, NonCollinearImpliesDistinct_THM;
alpha = a /\ beta = b by -, aOAbOB, exists, I1;
qed by -, exists`;;

let WholeRayInterior_THM = thm `;
let A O B X P be point;
assume ~Collinear(A, O, B)                                            [H1];
assume X int_angle A,O,B                                              [H2];
assume P IN ray(O,X)							[H3];
assume ~(P = O)                                                       [H4];
thus P int_angle A,O,B

proof
~(A = O) /\ ~(A = B) /\ ~(O = B) [Distinct] by H1, NonCollinearImpliesDistinct_THM;
consider a such that O IN a /\ A IN a       [a_OA] by Distinct, I1;
consider b such that O IN b /\ B IN b       [b_OB] by Distinct, I1;
~(X IN a) /\ ~(X IN b) /\ X,B same_side a /\ X,A same_side b [XintAOB] by H2, a_OA, b_OB, InteriorHelp_THM;
~(O = X) /\ Collinear(O, X, P) /\ ~ Between(P, O, X) [P_OX] by H3, IN, Ray_DEF;
consider x such that O IN x /\ X IN x       [x_OX] by P_OX, I1;
:: P IN x       [Pin_x] by x_OX, P_OX, Collinear_DEF, CollinearLinear_THM;
P IN x       [Pin_x] by x_OX, P_OX, CollinearLinear_THM;
P IN x DELETE O                         [Pin_x_O] by Pin_x, H4, IN_DELETE;
X IN x DELETE O                    [Xin_x_O] by x_OX, P_OX,  IN_DELETE;
~(x = a) /\ ~(x = b)               [x_not_ab] by XintAOB, x_OX;
a INTER x = {O} /\ b INTER x = {O} [axb_intO] by x_not_ab, x_OX, a_OA, b_OB, Line01infinity_THM;
~(P IN a) /\ P,X same_side a [Psim_aX] by axb_intO, Pin_x_O, Xin_x_O, P_OX, EquivIntersection_THM;
~(P IN b) /\ P,X same_side b [Psim_bX] by axb_intO, Pin_x_O, Xin_x_O, P_OX, EquivIntersection_THM;
P,B same_side a  /\ P,A same_side b by Psim_aX, Psim_bX, XintAOB, a_OA, b_OB, H1, Collinear_DEF,
SameSideTransitiveRelation_THM, Transitive_relation_DEF;
qed by H1, a_OA, b_OB, Psim_aX, Psim_bX, -, InteriorAngle_DEF`;;

let AngleOrdering_THM = thm `;
let O A P Q be point;
let a be line;
assume ~(O = A)                                                       [H1];
assume O IN a /\ A IN a                                               [H2];
assume ~(P IN a) /\ ~(Q IN a)                                         [H3];
assume P, Q same_side a                                               [H4];
assume ~Collinear(P, O, Q)                                            [H5];
thus P int_angle Q,O,A \/ Q int_angle P,O,A

proof
~(P = O) /\ ~(P = Q) /\ ~(O = Q) [Distinct] by H5, NonCollinearImpliesDistinct_THM;
consider p such that O IN p /\ P IN p             [p_OP] by Distinct, I1;
consider q such that O IN q /\ Q IN q             [q_OQ] by Distinct, I1;
~(q = a) by H3, q_OQ;
q INTER a = {O}                       by -, H2, q_OQ, Line01infinity_THM;
~(A IN q) by -, H2, H1, IntersectionSingletonOneNotOther_THM;
~(P IN q)                             [notPq] by q_OQ, H5, Collinear_DEF;
~(p = q) by -, p_OP;
p INTER q = {O}              	by -, p_OP, q_OQ, Line01infinity_THM;
~Collinear(Q, O, A)        [QOA_noncol] by H1, H2, I1, H3, Collinear_DEF;
~Collinear (P,O,A)         [POA_noncol] by H1, H2, I1, H3, Collinear_DEF;

assume ~(P int_angle Q,O,A)                                   [notP_QOA];
Q int_angle P,O,A
proof
~(P, A same_side q)           		 by QOA_noncol, H2, q_OQ, H3,
notPq, H4, notP_QOA, InteriorAngle_DEF;
consider G such that (G IN q) /\ Between(P, G, A) [existG] by -, same_side_DEF;
G int_angle P,O,A [G_POA] by  POA_noncol, existG, ConverseCrossbar_THM;
~(G IN a) /\ G,P same_side a [Gsim_aP] by -, InteriorAngle_DEF, H1, H2, I1;
~(G = O)                     [GnotO] by -, H2;
G,Q same_side a              by Gsim_aP, H3, H4,
SameSideTransitiveRelation_THM, Transitive_relation_DEF;
~Between (Q,O,G) 		   [notQOG] by -, same_side_DEF, H2, B1;
Collinear(O,G,Q)             by q_OQ, existG, Collinear_DEF;
Q IN ray(O,G) by GnotO, -, notQOG, IN, Ray_DEF;
qed by POA_noncol, G_POA, -, Distinct, WholeRayInterior_THM;
qed by -`;;

let InteriorReflectionInterior_THM = thm `;
let A O B D A' be point;
assume ~Collinear(A, O, B)                                            [H1];
assume D int_angle A,O,B                                              [H2];
assume Between(A, O, A')                                              [H3];
thus B  int_angle D,O,A'

proof
~(A = O) /\ ~(A = B) /\ ~(O = B) [Distinct] by H1, NonCollinearImpliesDistinct_THM;
consider a such that
O IN a /\ A IN a                                  [a_OA] by Distinct, I1;
consider b such that
O IN b /\ B IN b				      [b_OB] by Distinct, I1;
~(A IN b) 	                          [notAb] by b_OB, H1, Collinear_DEF;
~(B IN a)                      	  [notBa] by a_OA, H1, Collinear_DEF;
~(a = b) by -, b_OB;
b INTER a = {O}		 [ab_O] by -, a_OA, b_OB, Line01infinity_THM;
A' IN a    	     	         [A'a] by H3, a_OA, BetweenLinear_THM;
A' IN a DELETE O by A'a, H3, B1, IN_DELETE;
~(A' IN b) 	     	      [notA'b] by ab_O, -, EquivIntersectionHelp_THM;
~(A,A' same_side b)       [Ansim_bA'] by b_OB, H3, same_side_DEF ;
~(D IN a) /\ ~(D IN b) /\
D,B same_side a /\ D,A same_side b [DintAOB] by a_OA, b_OB, H2, InteriorHelp_THM;
~(D,A' same_side b)       [Dnsim_bA']
proof
assume D,A' same_side b;
A',D same_side b by DintAOB, notA'b, -, SameSideSymmetricRelation_THM, Symmetric_relation_DEF;
A',A same_side b by DintAOB, notA'b, notAb, -, SameSideTransitiveRelation_THM,
Transitive_relation_DEF;
A,A' same_side b by notA'b, notAb, -, SameSideSymmetricRelation_THM, Symmetric_relation_DEF;
F by -, Ansim_bA';
qed by -;
~(D int_angle B,O,A')					[notD_BOA']
proof
assume D int_angle B,O,A';
D,A' same_side b by b_OB, a_OA, A'a, -, DintAOB, InteriorHelp_THM;
F by -, Dnsim_bA';
qed by -;
~Collinear (D,O,B) [DOB_noncol] by Distinct, b_OB, I1, DintAOB, Collinear_DEF;
~(O = A') by H3, B1;
B int_angle D,O,A' by -, a_OA, A'a, DintAOB, notBa, DOB_noncol, notD_BOA', AngleOrdering_THM;
qed by -`;;

let Crossbar_THM = thm `;
let O A B D be point;
assume ~Collinear(A, O, B)						[H1];
assume D int_angle A,O,B                                              [H2];
thus ?G. Between(A, G, B) /\ G IN ray(O, D)

proof
~(A = O) /\ ~(A = B) /\ ~(O = B) [Distinct] by H1, NonCollinearImpliesDistinct_THM;
consider a such that
O IN a /\ A IN a                                  [a_OA] by Distinct, I1;
consider b such that
O IN b /\ B IN b                                  [b_OB] by Distinct, I1;
~(B IN a) [notBa] by a_OA, H1, Collinear_DEF;
~(D IN a) /\ ~(D IN b) /\ D,B same_side a [D_AOB] by a_OA, b_OB, H2, InteriorHelp_THM;
~(D = O)  	     	      	  	      	      [DnotO] by D_AOB, a_OA;
consider l such that
O IN l /\ D IN l				      [l_OD] by -, I1;
~(a = l) /\ ~(b = l)  [abl_distinct] by l_OD, D_AOB, b_OB, notBa;
a INTER l = {O} [alO] by abl_distinct, a_OA, l_OD, Line01infinity_THM;
b INTER l = {O} [blO] by abl_distinct, b_OB, l_OD, Line01infinity_THM;
~(A IN l) /\ ~(B IN l) [ABnot_l] by alO, blO, a_OA, b_OB, Distinct, IntersectionSingletonOneNotOther_THM;
consider A' such that Between(A, O, A') 	      [AOA'] by Distinct, B2;
A' IN a  	     	  	         [A'a] by a_OA, -, BetweenLinear_THM;
~(A' = O) [A'notO] by AOA', B1;
~(A,A' same_side l) 	    [Ansim_lA'] by l_OD, AOA', same_side_DEF;
~(A' IN l) [A'not_l] by alO, A'a, A'notO, IntersectionSingletonOneNotOther_THM;

B int_angle D,O,A'  by H1, H2, AOA', InteriorReflectionInterior_THM;
B,A' same_side l [Bsim_lA'] by l_OD, a_OA, A'a, -, InteriorHelp_THM;
~(A,B same_side l)						[Ansim_lB]
proof
assume A,B same_side l;
A,A' same_side l by ABnot_l, A'not_l, -, Bsim_lA', SameSideTransitiveRelation_THM, Transitive_relation_DEF;
qed by -, Ansim_lA';
consider G such that
Between(A, G, B) /\ G IN l		      [AGB] by Ansim_lB, same_side_DEF;
Collinear (O,D,G) 	     		  [ODGcol] by AGB, l_OD, Collinear_DEF;
G int_angle A,O,B 		              by H1, AGB, ConverseCrossbar_THM;
~(G IN a) /\ G,B same_side a [Gsim_aB] by a_OA, b_OB, -, InteriorHelp_THM;
D,B same_side a by a_OA, b_OB, H2, InteriorHelp_THM;
B,D same_side a by notBa, D_AOB, -, SameSideSymmetricRelation_THM, Symmetric_relation_DEF;
G,D same_side a [Gsim_aD] by Gsim_aB, notBa, D_AOB, Gsim_aB, -, SameSideTransitiveRelation_THM, Transitive_relation_DEF;
~Between(G, O, D) by a_OA, -, same_side_DEF;
G IN ray(O,D) [G_OD] by DnotO, ODGcol, -, IN, Ray_DEF;
qed by AGB, G_OD`;;

(*
exec GOAL_TAC;
p();;
*)

let IntervalTransitivity_THM = thm `;
let O P Q R be point;
let m be line;
assume O IN m								[H1];
assume P IN m DELETE O /\ Q IN m DELETE O /\ R IN m DELETE O		[H2];
assume ~Between(P, O, Q) /\ ~Between(Q, O, R)     	     		[H3];
thus ~Between(P, O, R)

proof
P IN m /\ Q IN m /\ R IN m /\ ~(P = O) /\ ~(Q = O) /\ ~(R = O) [H2'] by H2, IN_DELETE;
consider E such that
~(E IN m)				 [notEm] by ExistsPointOffLine_THM;
~(O = E) by H1, notEm;
consider l such that
O IN l /\ E IN l			 [OE_l] by -, I1;
~(m = l) by notEm, OE_l;
l INTER m = {O}			 [ml_O] by -, H1, OE_l, Line01infinity_THM;
~(P IN l) /\  ~(Q IN l) /\ ~(R IN l) [PQRnotl] by ml_O, H2', IntersectionSingletonOneNotOther_THM;
P,Q same_side l /\ Q,R same_side l   [Psim_lQsim_lR] by ml_O, H2, H3, PQRnotl, EquivIntersection_THM;
P,R same_side l    	   	     	 [Psim_lR] by PQRnotl, Psim_lQsim_lR,
SameSideTransitiveRelation_THM, Transitive_relation_DEF;
qed by OE_l, -, same_side_DEF`;;

------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
```

Gmane