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

Theorem

bigops.let_clause_10471

Statement

∀ n1 n2 p1 p2 f1 f2, iso n1 n2 p1 p2 f1 f2 ⇒ ∀ h, ex (λk. ((∀ i, i < n1 ⇒ (p1 i) = true ⇒ (f1 i) = (f2 (h i))) ∧ (sub_hk h k n1 n2 p1 p2 f1 f2)) ∧ (sub_hk k h n2 n1 p2 p1 f2 f1)) ⇒ ∀ k, ((∀ i, i < n1 ⇒ (p1 i) = true ⇒ (f1 i) = (f2 (h i))) ∧ (sub_hk h k n1 n2 p1 p2 f1 f2)) ∧ (sub_hk k h n2 n1 p2 p1 f2 f1) ⇒ (∀ i, i < n1 ⇒ (p1 i) = true ⇒ (f1 i) = (f2 (h i))) ∧ (sub_hk h k n1 n2 p1 p2 f1 f2) ⇒ ∀ i, i < n1 ⇒ (p1 i) = true ⇒ (f1 i) = (f2 (h i)) ⇒ ∀ i m, ∀ f, O ≤ n1 ⇒ sub_hk h k O m p1 f f1 f2 ⇒ sub_hk k h m O f p1 f2 f1 ⇒ (bigop O (λi0. p1 i0) 1 times (λi0. f1 i0)) = (bigop m (λi0. f i0) 1 times (λi0. f2 i0)) ⇒ ∀ p20, O ≤ n1 ⇒ sub_hk h k O (m+1) p1 p20 f1 f2 ⇒ sub_hk k h (m+1) O p20 p1 f2 f1 ⇒ ∀ x2571 x2572, x2571 = ((x2572 × (div x2571 x2572)) + (mod x2571 x2572))

Main Dependencies
Theory

Coq-Jumb
Statement

Theorem let_clause_10471 : forall (n1:nat.nat), forall (n2:nat.nat), forall (p1:(nat.nat -> bool.bool)), forall (p2:(nat.nat -> bool.bool)), forall (f1:(nat.nat -> nat.nat)), forall (f2:(nat.nat -> nat.nat)), (iso n1 n2 p1 p2 f1 f2) -> forall (h:(nat.nat -> nat.nat)), (connectives.ex (nat.nat -> nat.nat) (fun (k:(nat.nat -> nat.nat)) => connectives.And (connectives.And (forall (i:nat.nat), (nat.lt i n1) -> (logic.eq (bool.bool) (p1 i) bool.true) -> logic.eq (nat.nat) (f1 i) (f2 (h i))) (sub_hk h k n1 n2 p1 p2 f1 f2)) (sub_hk k h n2 n1 p2 p1 f2 f1))) -> forall (k:(nat.nat -> nat.nat)), (connectives.And (connectives.And (forall (i:nat.nat), (nat.lt i n1) -> (logic.eq (bool.bool) (p1 i) bool.true) -> logic.eq (nat.nat) (f1 i) (f2 (h i))) (sub_hk h k n1 n2 p1 p2 f1 f2)) (sub_hk k h n2 n1 p2 p1 f2 f1)) -> (connectives.And (forall (i:nat.nat), (nat.lt i n1) -> (logic.eq (bool.bool) (p1 i) bool.true) -> logic.eq (nat.nat) (f1 i) (f2 (h i))) (sub_hk h k n1 n2 p1 p2 f1 f2)) -> (forall (i:nat.nat), (nat.lt i n1) -> (logic.eq (bool.bool) (p1 i) bool.true) -> logic.eq (nat.nat) (f1 i) (f2 (h i))) -> forall (i:nat.nat), forall (m:nat.nat), (forall (f:(nat.nat -> bool.bool)), (nat.le nat.O n1) -> (sub_hk h k nat.O m p1 f f1 f2) -> (sub_hk k h m nat.O f p1 f2 f1) -> logic.eq (nat.nat) (bigop (nat.nat) nat.O (fun (i0:nat.nat) => p1 i0) (nat.S nat.O) nat.times (fun (i0:nat.nat) => f1 i0)) (bigop (nat.nat) m (fun (i0:nat.nat) => f i0) (nat.S nat.O) nat.times (fun (i0:nat.nat) => f2 i0))) -> forall (p20:(nat.nat -> bool.bool)), (nat.le nat.O n1) -> (sub_hk h k nat.O (nat.S m) p1 p20 f1 f2) -> (sub_hk k h (nat.S m) nat.O p20 p1 f2 f1) -> forall (x2571:nat.nat), forall (x2572:nat.nat), logic.eq (nat.nat) x2571 (nat.plus (nat.times x2572 (div_mod.div x2571 x2572)) (div_mod.mod x2571 x2572)).



Matita-Jumb
Statement

theorem let_clause_10471 : \forall (n1:nat). \forall (n2:nat). \forall (p1:nat -> bool). \forall (p2:nat -> bool). \forall (f1:nat -> nat). \forall (f2:nat -> nat). ((iso) n1 n2 p1 p2 f1 f2) -> \forall (h:nat -> nat). ((ex) (nat -> nat) (\lambda k : nat -> nat. (And) ((And) (\forall (i:nat). ((lt) i n1) -> ((eq) (bool) (p1 i) (true) ) -> (eq) (nat) (f1 i) (f2 (h i))) ((sub_hk) h k n1 n2 p1 p2 f1 f2)) ((sub_hk) k h n2 n1 p2 p1 f2 f1))) -> \forall (k:nat -> nat). ((And) ((And) (\forall (i:nat). ((lt) i n1) -> ((eq) (bool) (p1 i) (true) ) -> (eq) (nat) (f1 i) (f2 (h i))) ((sub_hk) h k n1 n2 p1 p2 f1 f2)) ((sub_hk) k h n2 n1 p2 p1 f2 f1)) -> ((And) (\forall (i:nat). ((lt) i n1) -> ((eq) (bool) (p1 i) (true) ) -> (eq) (nat) (f1 i) (f2 (h i))) ((sub_hk) h k n1 n2 p1 p2 f1 f2)) -> (\forall (i:nat). ((lt) i n1) -> ((eq) (bool) (p1 i) (true) ) -> (eq) (nat) (f1 i) (f2 (h i))) -> \forall (i:nat). \forall (m:nat). (\forall (f:nat -> bool). ((le) (O) n1) -> ((sub_hk) h k (O) m p1 f f1 f2) -> ((sub_hk) k h m (O) f p1 f2 f1) -> (eq) (nat) ((bigop) (nat) (O) (\lambda i0 : nat. p1 i0) ((S) (O) ) (times) (\lambda i0 : nat. f1 i0)) ((bigop) (nat) m (\lambda i0 : nat. f i0) ((S) (O) ) (times) (\lambda i0 : nat. f2 i0))) -> \forall (p20:nat -> bool). ((le) (O) n1) -> ((sub_hk) h k (O) ((S) m) p1 p20 f1 f2) -> ((sub_hk) k h ((S) m) (O) p20 p1 f2 f1) -> \forall (x2571:nat). \forall (x2572:nat). (eq) (nat) x2571 ((plus) ((times) x2572 ((div) x2571 x2572)) ((mod) x2571 x2572)).



Lean-jumb
Statement

theorem let_clause_10471 : forall (n1:nat.nat) , forall (n2:nat.nat) , forall (p1:(nat.nat) -> bool.bool) , forall (p2:(nat.nat) -> bool.bool) , forall (f1:(nat.nat) -> nat.nat) , forall (f2:(nat.nat) -> nat.nat) , ((((((((bigops.iso) ) (n1)) (n2)) (p1)) (p2)) (f1)) (f2)) -> forall (h:(nat.nat) -> nat.nat) , (((connectives.ex) ((nat.nat) -> nat.nat)) (fun (k : (nat.nat) -> nat.nat) , (((connectives.And) ) ((((connectives.And) ) (forall (i:nat.nat) , ((((nat.lt_) ) (i)) (n1)) -> ((((logic.eq_) (bool.bool)) ((p1) (i))) ((bool.true) )) -> (((logic.eq_) (nat.nat)) ((f1) (i))) ((f2) ((h) (i))))) ((((((((((bigops.sub_hk) ) (h)) (k)) (n1)) (n2)) (p1)) (p2)) (f1)) (f2)))) ((((((((((bigops.sub_hk) ) (k)) (h)) (n2)) (n1)) (p2)) (p1)) (f2)) (f1)))) -> forall (k:(nat.nat) -> nat.nat) , ((((connectives.And) ) ((((connectives.And) ) (forall (i:nat.nat) , ((((nat.lt_) ) (i)) (n1)) -> ((((logic.eq_) (bool.bool)) ((p1) (i))) ((bool.true) )) -> (((logic.eq_) (nat.nat)) ((f1) (i))) ((f2) ((h) (i))))) ((((((((((bigops.sub_hk) ) (h)) (k)) (n1)) (n2)) (p1)) (p2)) (f1)) (f2)))) ((((((((((bigops.sub_hk) ) (k)) (h)) (n2)) (n1)) (p2)) (p1)) (f2)) (f1))) -> ((((connectives.And) ) (forall (i:nat.nat) , ((((nat.lt_) ) (i)) (n1)) -> ((((logic.eq_) (bool.bool)) ((p1) (i))) ((bool.true) )) -> (((logic.eq_) (nat.nat)) ((f1) (i))) ((f2) ((h) (i))))) ((((((((((bigops.sub_hk) ) (h)) (k)) (n1)) (n2)) (p1)) (p2)) (f1)) (f2))) -> (forall (i:nat.nat) , ((((nat.lt_) ) (i)) (n1)) -> ((((logic.eq_) (bool.bool)) ((p1) (i))) ((bool.true) )) -> (((logic.eq_) (nat.nat)) ((f1) (i))) ((f2) ((h) (i)))) -> forall (i:nat.nat) , forall (m:nat.nat) , (forall (f:(nat.nat) -> bool.bool) , ((((nat.le_) ) ((nat.O) )) (n1)) -> ((((((((((bigops.sub_hk) ) (h)) (k)) ((nat.O) )) (m)) (p1)) (f)) (f1)) (f2)) -> ((((((((((bigops.sub_hk) ) (k)) (h)) (m)) ((nat.O) )) (f)) (p1)) (f2)) (f1)) -> (((logic.eq_) (nat.nat)) (((((((bigops.bigop) (nat.nat)) ((nat.O) )) (fun (i0 : nat.nat) , (p1) (i0))) (((nat.S) ) ((nat.O) ))) ((nat.times) )) (fun (i0 : nat.nat) , (f1) (i0)))) (((((((bigops.bigop) (nat.nat)) (m)) (fun (i0 : nat.nat) , (f) (i0))) (((nat.S) ) ((nat.O) ))) ((nat.times) )) (fun (i0 : nat.nat) , (f2) (i0)))) -> forall (p20:(nat.nat) -> bool.bool) , ((((nat.le_) ) ((nat.O) )) (n1)) -> ((((((((((bigops.sub_hk) ) (h)) (k)) ((nat.O) )) (((nat.S) ) (m))) (p1)) (p20)) (f1)) (f2)) -> ((((((((((bigops.sub_hk) ) (k)) (h)) (((nat.S) ) (m))) ((nat.O) )) (p20)) (p1)) (f2)) (f1)) -> forall (x2571:nat.nat) , forall (x2572:nat.nat) , (((logic.eq_) (nat.nat)) (x2571)) ((((nat.plus) ) ((((nat.times) ) (x2572)) ((((div_mod.div) ) (x2571)) (x2572)))) ((((div_mod.mod) ) (x2571)) (x2572))).



PVS-jumb

Statement

let_clause_10471 : LEMMA (FORALL(n1:nat_sttfa_th.sttfa_nat):(FORALL(n2:nat_sttfa_th.sttfa_nat):(FORALL(p1:[nat_sttfa_th.sttfa_nat -> bool_sttfa_th.sttfa_bool]):(FORALL(p2:[nat_sttfa_th.sttfa_nat -> bool_sttfa_th.sttfa_bool]):(FORALL(f1:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):(FORALL(f2:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):(bigops_sttfa.iso(n1)(n2)(p1)(p2)(f1)(f2) => (FORALL(h:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):(connectives_sttfa_th.sttfa_ex[[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]]((LAMBDA(k:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):connectives_sttfa_th.sttfa_And(connectives_sttfa_th.sttfa_And((FORALL(i:nat_sttfa_th.sttfa_nat):(nat_sttfa_th.lt(i)(n1) => (logic_sttfa_th.eq[bool_sttfa_th.sttfa_bool](p1(i))(bool_sttfa_th.sttfa_true) => logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](f1(i))(f2(h(i)))))))(bigops_sttfa.sub_hk(h)(k)(n1)(n2)(p1)(p2)(f1)(f2)))(bigops_sttfa.sub_hk(k)(h)(n2)(n1)(p2)(p1)(f2)(f1)))) => (FORALL(k:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):(connectives_sttfa_th.sttfa_And(connectives_sttfa_th.sttfa_And((FORALL(i:nat_sttfa_th.sttfa_nat):(nat_sttfa_th.lt(i)(n1) => (logic_sttfa_th.eq[bool_sttfa_th.sttfa_bool](p1(i))(bool_sttfa_th.sttfa_true) => logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](f1(i))(f2(h(i)))))))(bigops_sttfa.sub_hk(h)(k)(n1)(n2)(p1)(p2)(f1)(f2)))(bigops_sttfa.sub_hk(k)(h)(n2)(n1)(p2)(p1)(f2)(f1)) => (connectives_sttfa_th.sttfa_And((FORALL(i:nat_sttfa_th.sttfa_nat):(nat_sttfa_th.lt(i)(n1) => (logic_sttfa_th.eq[bool_sttfa_th.sttfa_bool](p1(i))(bool_sttfa_th.sttfa_true) => logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](f1(i))(f2(h(i)))))))(bigops_sttfa.sub_hk(h)(k)(n1)(n2)(p1)(p2)(f1)(f2)) => ((FORALL(i:nat_sttfa_th.sttfa_nat):(nat_sttfa_th.lt(i)(n1) => (logic_sttfa_th.eq[bool_sttfa_th.sttfa_bool](p1(i))(bool_sttfa_th.sttfa_true) => logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](f1(i))(f2(h(i)))))) => (FORALL(i:nat_sttfa_th.sttfa_nat):(FORALL(m:nat_sttfa_th.sttfa_nat):((FORALL(f:[nat_sttfa_th.sttfa_nat -> bool_sttfa_th.sttfa_bool]):(nat_sttfa_th.le(nat_sttfa_th.sttfa_O)(n1) => (bigops_sttfa.sub_hk(h)(k)(nat_sttfa_th.sttfa_O)(m)(p1)(f)(f1)(f2) => (bigops_sttfa.sub_hk(k)(h)(m)(nat_sttfa_th.sttfa_O)(f)(p1)(f2)(f1) => logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](bigops_sttfa.bigop[nat_sttfa_th.sttfa_nat](nat_sttfa_th.sttfa_O)((LAMBDA(i0:nat_sttfa_th.sttfa_nat):p1(i0)))(nat_sttfa_th.sttfa_S(nat_sttfa_th.sttfa_O))(nat_sttfa_th.times)((LAMBDA(i0:nat_sttfa_th.sttfa_nat):f1(i0))))(bigops_sttfa.bigop[nat_sttfa_th.sttfa_nat](m)((LAMBDA(i0:nat_sttfa_th.sttfa_nat):f(i0)))(nat_sttfa_th.sttfa_S(nat_sttfa_th.sttfa_O))(nat_sttfa_th.times)((LAMBDA(i0:nat_sttfa_th.sttfa_nat):f2(i0)))))))) => (FORALL(p20:[nat_sttfa_th.sttfa_nat -> bool_sttfa_th.sttfa_bool]):(nat_sttfa_th.le(nat_sttfa_th.sttfa_O)(n1) => (bigops_sttfa.sub_hk(h)(k)(nat_sttfa_th.sttfa_O)(nat_sttfa_th.sttfa_S(m))(p1)(p20)(f1)(f2) => (bigops_sttfa.sub_hk(k)(h)(nat_sttfa_th.sttfa_S(m))(nat_sttfa_th.sttfa_O)(p20)(p1)(f2)(f1) => (FORALL(x2571:nat_sttfa_th.sttfa_nat):(FORALL(x2572:nat_sttfa_th.sttfa_nat):logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](x2571)(nat_sttfa_th.plus(nat_sttfa_th.times(x2572)(div_mod_sttfa_th.div(x2571)(x2572)))(div_mod_sttfa_th.mod(x2571)(x2572)))))))))))))))))))))))))



OpenTheory

Printing for OpenTheory is not working at the moment.