[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] automatically dedution failed for OR in consequent ?



Hello, 

     I have a basic example :

test3: THEORY
BEGIN

a,b,c: bool

L1: AXIOM a  IMPLIES b OR c

L2: LEMMA a  IMPLIES b OR c

END test3

   And my question is: how to prove L2 without explicit using lemma L1 ? like this:

test2: THEORY
BEGIN

a,b,c: bool

L1: AXIOM a AND b IMPLIES c

L2: LEMMA b AND a IMPLIES c

%|- L2 : PROOF
%|- (then (auto-rewrite-theory test2) (flatten) (assert))
%|- QED

END test2


Best Regards,
Zengbo