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

Theorem

permutation.permut_S_to_permut_transpose

Statement

∀ f m, permut f (m+1) ⇒ permut (λn. transpose (f (m+1)) (m+1) (f n)) m

Main Dependencies
Theory

Coq-Jumb
Statement

Theorem permut_S_to_permut_transpose : forall (f:(nat.nat -> nat.nat)), forall (m:nat.nat), (permut f (nat.S m)) -> permut (fun (n:nat.nat) => transpose (f (nat.S m)) (nat.S m) (f n)) m.



Matita-Jumb
Statement

theorem permut_S_to_permut_transpose : \forall (f:nat -> nat). \forall (m:nat). ((permut) f ((S) m)) -> (permut) (\lambda n : nat. (transpose) (f ((S) m)) ((S) m) (f n)) m.



Lean-jumb
Statement

theorem permut_S_to_permut_transpose : forall (f:(nat.nat) -> nat.nat) , forall (m:nat.nat) , ((((permutation.permut) ) (f)) (((nat.S) ) (m))) -> (((permutation.permut) ) (fun (n : nat.nat) , ((((permutation.transpose) ) ((f) (((nat.S) ) (m)))) (((nat.S) ) (m))) ((f) (n)))) (m).



PVS-jumb

Statement

permut_S_to_permut_transpose : LEMMA (FORALL(f:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):(FORALL(m:nat_sttfa_th.sttfa_nat):(permutation_sttfa.permut(f)(nat_sttfa_th.sttfa_S(m)) => permutation_sttfa.permut((LAMBDA(n:nat_sttfa_th.sttfa_nat):permutation_sttfa.transpose(f(nat_sttfa_th.sttfa_S(m)))(nat_sttfa_th.sttfa_S(m))(f(n))))(m))))



OpenTheory

Printing for OpenTheory is not working at the moment.