// This prints the left floatting menu

### Theoremdiv_mod.sym_eq_mod_aux_body_S

Statement

∀ p, leibniz (λm. λn. if (leb m n) then m else (mod_aux p (m - (n+1)) n)) (mod_aux_body (p+1))

Main Dependencies
Theory

Statement

Theorem sym_eq_mod_aux_body_S : forall (p:nat.nat), leibniz.leibniz (nat.nat -> nat.nat -> nat.nat) (fun (m:nat.nat) => fun (n:nat.nat) => bool.match_bool_type (nat.nat) m (mod_aux p (nat.minus m (nat.S n)) n) (nat.leb m n)) (mod_aux_body (nat.S p)).

Statement

theorem sym_eq_mod_aux_body_S : \forall (p:nat). (leibniz) (nat -> nat -> nat) (\lambda m : nat. \lambda n : nat. (match_bool_type) (nat) m ((mod_aux) p ((minus) m ((S) n)) n) ((leb) m n)) ((mod_aux_body) ((S) p)).

Statement

theorem sym_eq_mod_aux_body_S : forall (p:nat.nat) , (((leibniz.leibniz) ((nat.nat) -> (nat.nat) -> nat.nat)) (fun (m : nat.nat) , fun (n : nat.nat) , ((((bool.match_bool_type) (nat.nat)) (m)) (((((div_mod.mod_aux) ) (p)) ((((nat.minus) ) (m)) (((nat.S) ) (n)))) (n))) ((((nat.leb) ) (m)) (n)))) (((div_mod.mod_aux_body) ) (((nat.S) ) (p))).

Statement

sym_eq_mod_aux_body_S : LEMMA (FORALL(p:nat_sttfa_th.sttfa_nat):leibniz_sttfa_th.leibniz[[nat_sttfa_th.sttfa_nat -> [nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]]]((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](m)(div_mod_sttfa.mod_aux(p)(nat_sttfa_th.minus(m)(nat_sttfa_th.sttfa_S(n)))(n))(nat_sttfa_th.leb(m)(n)))))(div_mod_sttfa.mod_aux_body(nat_sttfa_th.sttfa_S(p))))

Printing for OpenTheory is not working at the moment.