// This prints the left floatting menu
Dedukti    Load Matita      Load Coq         Load Lean        Load PVS         Load OpenTheory Load
Dedukti-jumb

Theorem

bool.andb_true_r

Statement

∀ b1 b2, (andb b1 b2) = true ⇒ b2 = true

Main Dependencies
Theory

Coq-Jumb
Statement

Theorem andb_true_r : forall (b1:bool), forall (b2:bool), (logic.eq (bool) (andb b1 b2) true) -> logic.eq (bool) b2 true.



Matita-Jumb
Statement

theorem andb_true_r : \forall (b1:bool). \forall (b2:bool). ((eq) (bool) ((andb) b1 b2) (true) ) -> (eq) (bool) b2 (true) .



Lean-jumb
Statement

theorem andb_true_r : forall (b1:bool.bool) , forall (b2:bool.bool) , ((((logic.eq_) (bool.bool)) ((((bool.andb) ) (b1)) (b2))) ((bool.true) )) -> (((logic.eq_) (bool.bool)) (b2)) ((bool.true) ).



PVS-jumb

Statement

andb_true_r : LEMMA (FORALL(b1:bool_sttfa.sttfa_bool):(FORALL(b2:bool_sttfa.sttfa_bool):(logic_sttfa_th.eq[bool_sttfa.sttfa_bool](bool_sttfa.andb(b1)(b2))(bool_sttfa.sttfa_true) => logic_sttfa_th.eq[bool_sttfa.sttfa_bool](b2)(bool_sttfa.sttfa_true))))



OpenTheory

Printing for OpenTheory is not working at the moment.