Wed Mar 17 12:03:01 CET 2010

Proving rules

Is it really so that a correctness proof is too difficult?  Some of
them are really quite trivial, i.e.:

  (((movlw a) (exit) pseudo) ((retlw a)))

The good thing about proof is that all rules can be treated
individually.  For testing, I'm not so sure about that.

 (([qw a ] [qw b] -)             ([qw (tv: a b -)]))
 (([addlw a] [qw b] -)           ([addlw (tv: a b -)]))
 (([qw a] -)                     ([addlw (tv: a -1 *)]))