Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-12-12 02:33:42 -0800 (Sun, 12 Dec 2004)
Revision: 6356
Log message:
- Added the var_bterm case support for make_bterm in base_reflection.
- Fixed some bugs in itt_reflection; Added some primitive rules.
The four lemmas for "subst_make_bterm" haven't been proved yet.
Just want to do the commit before fixing this bug:
---------
Do we consider these two bterms are the same?
1. 'b1 = bterm{| x: term >- it[@] |}
2. 'b2 = bterm{| >- it[@] |}
If yes, then we should modify the definition of if_simple_bterm.
If no, then "makebterm_same_op" is not valid, since
make_bterm { 'b1; [] } <-->
make_bterm{ 'b1; subterms{'b1} } <-->
'b1
and
make_bterm{ 'b1; [] } <-->
make_bterm{ 'b1; subterms{'b2} } <-->
'b2
which gives
'b1 <--> 'b2