Strong-semantics probabilistic parser for HOL Light

• sin 0 = cos pi / 2
• exp o sin continuous_on X
• x cross y = -- y cross x
• MAP f CONS x NIL = CONS f x NIL
• x + y ** z = x ** z + y ** z
• sin -- x = -- sin x
• inv a * b = inv b * inv a
• sin 2 * y = 2 * sin y * cos y
• -- -- x = x
• ( x * y ) * z = y * ( x * z )
• A0 EXP A1 + A2 = A0 EXP A1 * A0 EXP A2
• A1 A1 continuous_on A0
• abs continuous atreal x
• bounded X ==> compact frontier X
• compact X ==> compact IMAGE -- X
• exp ( ii * x) = ii * (sin x) + (cos x)
• polyhedron p ==> convex relative_interior p