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

Theorem

bigops.timesAC

Statement

ACop 1

Main Dependencies
Theory
Coq-Jumb
Statement

Theorem timesAC : ACop (nat.nat) (nat.S nat.O).


Matita-Jumb
Statement

theorem timesAC : (ACop) (nat) ((S) (O) ).


Lean-jumb
Statement

theorem timesAC : ((bigops.ACop) (nat.nat)) (((nat.S) ) ((nat.O) )).


PVS-jumb
Statement

timesAC : LEMMA bigops_sttfa.ACop[nat_sttfa_th.sttfa_nat](nat_sttfa_th.sttfa_S(nat_sttfa_th.sttfa_O))


OpenTheory

Printing for OpenTheory is not working at the moment.