(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Definition: muR                                                            *)
(* Chapter: LEG                                                               *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2010-02-07                                                           *)
(* ========================================================================== *)

This is the cayleyR function, expressed in terms of the unsquared variables
indexing: five vertices v1..v5, yij runs from vi to vj,
two tetrahedra, shared face v1,v2,v3.
v4 v5 in opposite half-planes.
enclosed = y45 = sqrt(x45) is the distance from v4 to v5.
y1..y6 is the usual indexing of a simplex.
y4..y9 is mod 6 congruent to the usual indexing.

module type Mur_def_type = sig
  val muR : thm
  val muRa : thm

flyspeck_needs "leg/cayleyR_def.hl";;

module Mur : Mur_def_type = struct

  let cayleyR = Cayleyr.cayleyR;;

let muR = 
new_definition `muR y1 y2 y3 y4 y5 y6 y7 y8 y9 x = cayleyR (y6*y6) (y5*y5) (y1*y1) (y7*y7) (y4*y4) (y2*y2) (y8*y8)  (y3*y3) (y9*y9) x`;;
let muRa = 
prove( `muR y1 y2 y3 y4 y5 y6 y7 y8 y9 = cayleyR (y6*y6) (y5*y5) (y1*y1) (y7*y7) (y4*y4) (y2*y2) (y8*y8) (y3*y3) (y9*y9)`,