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

Axiom

div_mod.axiom_div_aux_body_S

Statement

∀ p, equal (div_aux_body (p+1)) (λm. λn. if (leb m n) then O else ((div_aux p (m - (n+1)) n)+1))

Main Dependencies
Theory

Coq-Jumb
Statement

Axiom axiom_div_aux_body_S : forall (p:nat.nat), connectives.equal (nat.nat -> nat.nat -> nat.nat) (div_aux_body (nat.S p)) (fun (m:nat.nat) => fun (n:nat.nat) => bool.match_bool_type (nat.nat) nat.O (nat.S (div_aux p (nat.minus m (nat.S n)) n)) (nat.leb m n))



Matita-Jumb
Statement

axiom axiom_div_aux_body_S : \forall (p:nat). (equal) (nat -> nat -> nat) ((div_aux_body) ((S) p)) (\lambda m : nat. \lambda n : nat. (match_bool_type) (nat) (O) ((S) ((div_aux) p ((minus) m ((S) n)) n)) ((leb) m n))



Lean-jumb
Statement

axiom axiom_div_aux_body_S : forall (p:nat.nat) , (((connectives.equal) ((nat.nat) -> (nat.nat) -> nat.nat)) (((div_mod.div_aux_body) ) (((nat.S) ) (p)))) (fun (m : nat.nat) , fun (n : nat.nat) , ((((bool.match_bool_type) (nat.nat)) ((nat.O) )) (((nat.S) ) (((((div_mod.div_aux) ) (p)) ((((nat.minus) ) (m)) (((nat.S) ) (n)))) (n)))) ((((nat.leb) ) (m)) (n)))



PVS-jumb

Statement

axiom_div_aux_body_S : AXIOM (FORALL(p:nat_sttfa_th.sttfa_nat):connectives_sttfa_th.equal[[nat_sttfa_th.sttfa_nat -> [nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]]](div_mod_sttfa.div_aux_body(nat_sttfa_th.sttfa_S(p)))((LAMBDA(m:nat_sttfa_th.sttfa_nat):(LAMBDA(n:nat_sttfa_th.sttfa_nat):bool_sttfa_th.match_bool_type[nat_sttfa_th.sttfa_nat](nat_sttfa_th.sttfa_O)(nat_sttfa_th.sttfa_S(div_mod_sttfa.div_aux(p)(nat_sttfa_th.minus(m)(nat_sttfa_th.sttfa_S(n)))(n)))(nat_sttfa_th.leb(m)(n))))))



OpenTheory

Printing for OpenTheory is not working at the moment.