Dear all,
Happy proving :)
1) I wonder how I suppose to tackle situation like this
A, B, C |- D.
and D is a complicated term with D1 and D2 somewhere in it.
D1 can be rewrite to D1' under assumption of A,B,C while if I simply use
the ASM_REWRITE_RULE then I will do some other changes in D which I don't
want to.
2) Another related question: is there any way I can deal with situation
like
A, B, C |- D but I want to replace C by C' where C = C'
one way in my mind is to get
A, B |- C ==> D then use rewrite to get C' ==> D as concl but, that may
lead to the change in D as well.
It would be very nice if you can give me some advice.
Thanks very much!
--
Regards,
Robert
------------------------------------------------------------------------------
One dashboard for servers and applications across Physical-Virtual-Cloud
Widest out-of-the-box monitoring support with 50+ applications
Performance metrics, stats and reports that give you Actionable Insights
Deep dive visibility with transaction tracing using APM Insight.
http://ad.doubleclick.net/ddm/clk/290420510;117567292;y
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
