Logipedia

// This prints the left floatting menu

Load

Dedukti-jumb

Theorem
gcd.divides_to_gcd_aux

Statement

∀ p m n, O < p ⇒ O < n ⇒ n | m ⇒ (gcd_aux p m n) = n

Main Dependencies

theorem

gcd.sym_eq_gcd_aux gcd.sym_eq_gcd_aux_body_S nat.lt_O_n_elim primes.divides_to_dividesb_true

Theory

axiom

bool.axiom_match_bool_type_false bool.axiom_match_bool_type_true bool.match_bool_prop connectives.I connectives.Not_ind connectives.equal_leibniz connectives.falsity connectives.match_Or_prop connectives.nmk connectives.or_introl connectives.or_intror div_mod.axiom_div_aux div_mod.axiom_div_aux_body_O div_mod.axiom_div_aux_body_S div_mod.axiom_mod_aux div_mod.axiom_mod_aux_body_O div_mod.axiom_mod_aux_body_S div_mod.div_mod_spec_intro div_mod.match_div_mod_spec_prop gcd.axiom_gcd_aux gcd.axiom_gcd_aux_body_S leibniz.sym_leibniz logic.eq_ind logic.refl nat.axiom_eqb nat.axiom_eqb_body_O nat.axiom_eqb_body_S nat.axiom_filter_nat_type_O nat.axiom_filter_nat_type_S nat.axiom_leb nat.axiom_leb_body_O nat.axiom_leb_body_S nat.axiom_match_nat_type_O nat.axiom_match_nat_type_S nat.axiom_minus nat.axiom_minus_body_O nat.axiom_minus_body_S nat.axiom_plus nat.axiom_plus_body_O nat.axiom_plus_body_S nat.axiom_times nat.axiom_times_body_O nat.axiom_times_body_S nat.le_S nat.le_ind nat.le_n nat.match_nat_prop nat.nat_ind primes.match_divides_prop

definition

div_mod.mod leibniz.leibniz nat.lt primes.dividesb

tyop

bool.bool nat.nat

Coq-Jumb

Statement

Theorem divides_to_gcd_aux : forall (p:nat.nat), forall (m:nat.nat), forall (n:nat.nat), (nat.lt nat.O p) -> (nat.lt nat.O n) -> (primes.divides n m) -> logic.eq (nat.nat) (gcd_aux p m n) n.

Matita-Jumb

Statement

theorem divides_to_gcd_aux : \forall (p:nat). \forall (m:nat). \forall (n:nat). ((lt) (O) p) -> ((lt) (O) n) -> ((divides) n m) -> (eq) (nat) ((gcd_aux) p m n) n.

Lean-jumb

Statement

theorem divides_to_gcd_aux : forall (p:nat.nat) , forall (m:nat.nat) , forall (n:nat.nat) , ((((nat.lt_) ) ((nat.O) )) (p)) -> ((((nat.lt_) ) ((nat.O) )) (n)) -> ((((primes.divides) ) (n)) (m)) -> (((logic.eq_) (nat.nat)) (((((gcd.gcd_aux) ) (p)) (m)) (n))) (n).

PVS-jumb

Statement

divides_to_gcd_aux : LEMMA (FORALL(p:nat_sttfa_th.sttfa_nat):(FORALL(m:nat_sttfa_th.sttfa_nat):(FORALL(n:nat_sttfa_th.sttfa_nat):(nat_sttfa_th.lt(nat_sttfa_th.sttfa_O)(p) => (nat_sttfa_th.lt(nat_sttfa_th.sttfa_O)(n) => (primes_sttfa_th.sttfa_divides(n)(m) => logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](gcd_sttfa.gcd_aux(p)(m)(n))(n)))))))

OpenTheory

Printing for OpenTheory is not working at the moment.