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

Theorem

exp.eq_exp_body_S

Statement

∀ n m, leibniz (exp_body n (m+1)) ((n ^ m) × n)

Main Dependencies
Theory

Coq-Jumb
Statement

Theorem eq_exp_body_S : forall (n:nat.nat), forall (m:nat.nat), leibniz.leibniz (nat.nat) (exp_body n (nat.S m)) (nat.times (exp n m) n).



Matita-Jumb
Statement

theorem eq_exp_body_S : \forall (n:nat). \forall (m:nat). (leibniz) (nat) ((exp_body) n ((S) m)) ((times) ((exp) n m) n).



Lean-jumb
Statement

theorem eq_exp_body_S : forall (n:nat.nat) , forall (m:nat.nat) , (((leibniz.leibniz) (nat.nat)) ((((exp.exp_body) ) (n)) (((nat.S) ) (m)))) ((((nat.times) ) ((((exp.exp) ) (n)) (m))) (n)).



PVS-jumb

Statement

eq_exp_body_S : LEMMA (FORALL(n:nat_sttfa_th.sttfa_nat):(FORALL(m:nat_sttfa_th.sttfa_nat):leibniz_sttfa_th.leibniz[nat_sttfa_th.sttfa_nat](exp_sttfa.exp_body(n)(nat_sttfa_th.sttfa_S(m)))(nat_sttfa_th.times(exp_sttfa.sttfa_exp(n)(m))(n))))



OpenTheory

Printing for OpenTheory is not working at the moment.