Hi Bill,
| I have your InteriorAngle_DEF, which looks great, and thanks for
| writing it. Does my Line_DEF look OK? I have a thm which gets no
| error message until the last line
|
| thus G IN int_angle(A, O, B) by H1, Distinct, I3, notGina, notGinb,
Gsim_aB,
| Gsim_bA, InteriorAngle_DEF ;
|
| and Freek's miz3 error message is #2 inference time-out, which means
| that miz3 couldn't prove this assertion G IN int_angle(A, O, B).
| Well, I could believe I messed up something that complicated, and I'll
| try some things.
Without seeing the exact script I can't be absolutely sure, but I
think it's very likely that the default prover is failing to expand
or otherwise take account of the "let" construct. Can you try it
with the lets manually expanded? For example, do
let InteriorAngle_ALT =
CONV_RULE(TOP_DEPTH_CONV let_CONV) InteriorAngle_DEF;;
and try using InteriorAngle_ALT in place of InteriorAngle_DEF.
John.
------------------------------------------------------------------------------
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
