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

Theorem

permutation.let_clause_1063

Statement

∀ f n, permut f n ⇒ ∀ i j, i ≤ n ⇒ j ≤ n ⇒ ∀ a, (a ≤ n) ∧ ((f a) = i) ⇒ a ≤ n ⇒ (f a) = i ⇒ ∀ b, (b ≤ n) ∧ ((f b) = j) ⇒ b ≤ n ⇒ (f b) = j ⇒ ∀ i0, i0 ≤ n ⇒ (f i0) ≤ n ⇒ injn f n ⇒ a = b ⇒ (f a) = j

Main Dependencies
Theory

Coq-Jumb
Statement

Theorem let_clause_1063 : forall (f:(nat.nat -> nat.nat)), forall (n:nat.nat), (permut f n) -> forall (i:nat.nat), forall (j:nat.nat), (nat.le i n) -> (nat.le j n) -> forall (a:nat.nat), (connectives.And (nat.le a n) (logic.eq (nat.nat) (f a) i)) -> (nat.le a n) -> (logic.eq (nat.nat) (f a) i) -> forall (b:nat.nat), (connectives.And (nat.le b n) (logic.eq (nat.nat) (f b) j)) -> (nat.le b n) -> (logic.eq (nat.nat) (f b) j) -> (forall (i0:nat.nat), (nat.le i0 n) -> nat.le (f i0) n) -> (injn f n) -> (logic.eq (nat.nat) a b) -> logic.eq (nat.nat) (f a) j.



Matita-Jumb
Statement

theorem let_clause_1063 : \forall (f:nat -> nat). \forall (n:nat). ((permut) f n) -> \forall (i:nat). \forall (j:nat). ((le) i n) -> ((le) j n) -> \forall (a:nat). ((And) ((le) a n) ((eq) (nat) (f a) i)) -> ((le) a n) -> ((eq) (nat) (f a) i) -> \forall (b:nat). ((And) ((le) b n) ((eq) (nat) (f b) j)) -> ((le) b n) -> ((eq) (nat) (f b) j) -> (\forall (i0:nat). ((le) i0 n) -> (le) (f i0) n) -> ((injn) f n) -> ((eq) (nat) a b) -> (eq) (nat) (f a) j.



Lean-jumb
Statement

theorem let_clause_1063 : forall (f:(nat.nat) -> nat.nat) , forall (n:nat.nat) , ((((permutation.permut) ) (f)) (n)) -> forall (i:nat.nat) , forall (j:nat.nat) , ((((nat.le_) ) (i)) (n)) -> ((((nat.le_) ) (j)) (n)) -> forall (a:nat.nat) , ((((connectives.And) ) ((((nat.le_) ) (a)) (n))) ((((logic.eq_) (nat.nat)) ((f) (a))) (i))) -> ((((nat.le_) ) (a)) (n)) -> ((((logic.eq_) (nat.nat)) ((f) (a))) (i)) -> forall (b:nat.nat) , ((((connectives.And) ) ((((nat.le_) ) (b)) (n))) ((((logic.eq_) (nat.nat)) ((f) (b))) (j))) -> ((((nat.le_) ) (b)) (n)) -> ((((logic.eq_) (nat.nat)) ((f) (b))) (j)) -> (forall (i0:nat.nat) , ((((nat.le_) ) (i0)) (n)) -> (((nat.le_) ) ((f) (i0))) (n)) -> ((((permutation.injn) ) (f)) (n)) -> ((((logic.eq_) (nat.nat)) (a)) (b)) -> (((logic.eq_) (nat.nat)) ((f) (a))) (j).



PVS-jumb

Statement

let_clause_1063 : LEMMA (FORALL(f:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):(FORALL(n:nat_sttfa_th.sttfa_nat):(permutation_sttfa.permut(f)(n) => (FORALL(i:nat_sttfa_th.sttfa_nat):(FORALL(j:nat_sttfa_th.sttfa_nat):(nat_sttfa_th.le(i)(n) => (nat_sttfa_th.le(j)(n) => (FORALL(a:nat_sttfa_th.sttfa_nat):(connectives_sttfa_th.sttfa_And(nat_sttfa_th.le(a)(n))(logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](f(a))(i)) => (nat_sttfa_th.le(a)(n) => (logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](f(a))(i) => (FORALL(b:nat_sttfa_th.sttfa_nat):(connectives_sttfa_th.sttfa_And(nat_sttfa_th.le(b)(n))(logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](f(b))(j)) => (nat_sttfa_th.le(b)(n) => (logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](f(b))(j) => ((FORALL(i0:nat_sttfa_th.sttfa_nat):(nat_sttfa_th.le(i0)(n) => nat_sttfa_th.le(f(i0))(n))) => (permutation_sttfa.injn(f)(n) => (logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](a)(b) => logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](f(a))(j)))))))))))))))))))



OpenTheory

Printing for OpenTheory is not working at the moment.