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

Theorem

permutation.sym_eq_invert_permut_body_O

Statement

leibniz (λf. λm. if (m = (f O)) then O else O) (invert_permut_body O)

Main Dependencies
Theory

Coq-Jumb
Statement

Theorem sym_eq_invert_permut_body_O : leibniz.leibniz ((nat.nat -> nat.nat) -> nat.nat -> nat.nat) (fun (f:(nat.nat -> nat.nat)) => fun (m:nat.nat) => bool.match_bool_type (nat.nat) nat.O nat.O (nat.eqb m (f nat.O))) (invert_permut_body nat.O).



Matita-Jumb
Statement

theorem sym_eq_invert_permut_body_O : (leibniz) ((nat -> nat) -> nat -> nat) (\lambda f : nat -> nat. \lambda m : nat. (match_bool_type) (nat) (O) (O) ((eqb) m (f (O) ))) ((invert_permut_body) (O) ).



Lean-jumb
Statement

theorem sym_eq_invert_permut_body_O : (((leibniz.leibniz) (((nat.nat) -> nat.nat) -> (nat.nat) -> nat.nat)) (fun (f : (nat.nat) -> nat.nat) , fun (m : nat.nat) , ((((bool.match_bool_type) (nat.nat)) ((nat.O) )) ((nat.O) )) ((((nat.eqb) ) (m)) ((f) ((nat.O) ))))) (((permutation.invert_permut_body) ) ((nat.O) )).



PVS-jumb

Statement

sym_eq_invert_permut_body_O : LEMMA leibniz_sttfa_th.leibniz[[[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat] -> [nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]]]((LAMBDA(f:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):(LAMBDA(m: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_O)(nat_sttfa_th.eqb(m)(f(nat_sttfa_th.sttfa_O))))))(permutation_sttfa.invert_permut_body(nat_sttfa_th.sttfa_O))



OpenTheory

Printing for OpenTheory is not working at the moment.