Let X, Tx, C and eps be given.
We prove the intermediate
claim HUcover:
open_cover X Tx U.
We will
prove (∀u : set, u ∈ U → u ∈ Tx) ∧ covers X U.
Apply andI to the current goal.
Let u be given.
An
exact proof term for the current goal is
(SepE1 Tx (λN : set ⇒ ∃x : set, x ∈ X ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ C ∧ ∀A : set, A ∈ C → A ∩ N ≠ Empty → A ∈ S) u HuU).
Let x be given.
We prove the intermediate
claim Hlocx:
∀x0 : set, x0 ∈ X → ∃N : set, N ∈ Tx ∧ x0 ∈ N ∧ ∃S : set, finite S ∧ S ⊆ C ∧ ∀A : set, A ∈ C → A ∩ N ≠ Empty → A ∈ S.
We prove the intermediate
claim HexN:
∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ C ∧ ∀A : set, A ∈ C → A ∩ N ≠ Empty → A ∈ S.
An exact proof term for the current goal is (Hlocx x HxX).
Apply HexN to the current goal.
Let N be given.
Assume HNpack.
We prove the intermediate
claim HN0:
(N ∈ Tx ∧ x ∈ N) ∧ ∃S : set, finite S ∧ S ⊆ C ∧ ∀A : set, A ∈ C → A ∩ N ≠ Empty → A ∈ S.
An exact proof term for the current goal is HNpack.
We prove the intermediate
claim HNopen:
N ∈ Tx.
We prove the intermediate
claim HxN:
x ∈ N.
We prove the intermediate
claim HexS:
∃S : set, finite S ∧ S ⊆ C ∧ ∀A : set, A ∈ C → A ∩ N ≠ Empty → A ∈ S.
An
exact proof term for the current goal is
(andER (N ∈ Tx ∧ x ∈ N) (∃S : set, finite S ∧ S ⊆ C ∧ ∀A : set, A ∈ C → A ∩ N ≠ Empty → A ∈ S) HN0).
We use N to witness the existential quantifier.
Apply andI to the current goal.
Apply (SepI Tx (λN0 : set ⇒ ∃x0 : set, x0 ∈ X ∧ x0 ∈ N0 ∧ ∃S : set, finite S ∧ S ⊆ C ∧ ∀A : set, A ∈ C → A ∩ N0 ≠ Empty → A ∈ S) N) to the current goal.
An exact proof term for the current goal is HNopen.
We use x to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HxX.
An exact proof term for the current goal is HxN.
An exact proof term for the current goal is HexS.
An exact proof term for the current goal is HxN.
Apply HexP to the current goal.
Let P be given.
We prove the intermediate
claim HPdom:
∀f : set, f ∈ P → ∃u : set, u ∈ U ∧ support_of X Tx f ⊆ u.
We prove the intermediate
claim HPval_in_R:
∀f x : set, f ∈ P → x ∈ X → apply_fun f x ∈ R.
Let f and x be given.
An exact proof term for the current goal is (HPui f x HfP HxX).
We prove the intermediate
claim HPval_nonneg:
∀f x : set, f ∈ P → x ∈ X → Rle 0 (apply_fun f x).
Let f and x be given.
An exact proof term for the current goal is (HPui f x HfP HxX).
An exact proof term for the current goal is Hnlt.
Let f be given.
We prove the intermediate
claim Hexu:
∃u0 : set, u0 ∈ U ∧ support_of X Tx f ⊆ u0.
An exact proof term for the current goal is (HPdom f HfP).
We prove the intermediate
claim Hu:
u ∈ U ∧ support_of X Tx f ⊆ u.
Apply Hexu to the current goal.
Let u0 be given.
An
exact proof term for the current goal is
(Eps_i_ax (λu1 : set ⇒ u1 ∈ U ∧ support_of X Tx f ⊆ u1) u0 Hu0).
We prove the intermediate
claim Huapply:
apply_fun u_of f = u.
rewrite the current goal using Huapply (from left to right).
An exact proof term for the current goal is Hu.
We prove the intermediate
claim HUfinite_hits:
∀u : set, u ∈ U → ∃x : set, x ∈ X ∧ x ∈ u ∧ ∃S : set, finite S ∧ S ⊆ C ∧ ∀A : set, A ∈ C → A ∩ u ≠ Empty → A ∈ S.
Let u be given.
An
exact proof term for the current goal is
(SepE2 Tx (λN : set ⇒ ∃x : set, x ∈ X ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ C ∧ ∀A : set, A ∈ C → A ∩ N ≠ Empty → A ∈ S) u HuU).
Let u be given.
We prove the intermediate
claim HexS:
∃S : set, finite S ∧ S ⊆ C ∧ ∀A : set, A ∈ C → A ∩ u ≠ Empty → A ∈ S.
Apply (HUfinite_hits u HuU) to the current goal.
Let x be given.
Assume Hxpack.
An
exact proof term for the current goal is
(andER (x ∈ X ∧ x ∈ u) (∃S : set, finite S ∧ S ⊆ C ∧ ∀A : set, A ∈ C → A ∩ u ≠ Empty → A ∈ S) Hxpack).
We prove the intermediate
claim HSu:
finite Su ∧ Su ⊆ C ∧ ∀A : set, A ∈ C → A ∩ u ≠ Empty → A ∈ Su.
Apply HexS to the current goal.
Let S be given.
Assume HS.
An
exact proof term for the current goal is
(Eps_i_ax (λS0 : set ⇒ finite S0 ∧ S0 ⊆ C ∧ ∀A : set, A ∈ C → A ∩ u ≠ Empty → A ∈ S0) S HS).
We prove the intermediate
claim HSapply:
apply_fun S_of u = Su.
rewrite the current goal using HSapply (from left to right).
An exact proof term for the current goal is HSu.
Let u be given.
We prove the intermediate
claim HVfin:
finite V.
An exact proof term for the current goal is (HUepsVals_finite u HuU).
We prove the intermediate
claim HallS:
∀y : set, y ∈ V → SNo y.
Let y be given.
Let c be given.
Assume HcSu.
Assume HyEq.
rewrite the current goal using HyEq (from left to right).
We prove the intermediate
claim HSu_subC:
apply_fun S_of u ⊆ C.
We prove the intermediate
claim HcC:
c ∈ C.
An exact proof term for the current goal is (HSu_subC c HcSu).
We prove the intermediate
claim Hepsc:
apply_fun eps c ∈ R.
We prove the intermediate
claim HVne0:
V ≠ 0.
We prove the intermediate
claim Hexc:
∃c : set, c ∈ apply_fun S_of u.
Apply Hexc to the current goal.
Let c be given.
We prove the intermediate
claim HcV:
apply_fun eps c ∈ V.
We prove the intermediate
claim Hcin0:
apply_fun eps c ∈ 0.
rewrite the current goal using HV0 (from right to left).
An exact proof term for the current goal is HcV.
An
exact proof term for the current goal is
(EmptyE (apply_fun eps c) Hcin0).
We prove the intermediate
claim Hexm:
∃m : set, SNo_min_of V m.
Apply Hexm to the current goal.
Let m be given.
An
exact proof term for the current goal is
(Eps_i_ax (λr : set ⇒ SNo_min_of V r) m HmMin).
Let u and c be given.
We prove the intermediate
claim HcinEmpty:
c ∈ Empty.
rewrite the current goal using HSu0 (from right to left).
An exact proof term for the current goal is HcSu.
An
exact proof term for the current goal is
(EmptyE c HcinEmpty).
An exact proof term for the current goal is (Hr_of_min u HuU HSuNe).
We prove the intermediate
claim HrS:
SNo (apply_fun r_of u).
We prove the intermediate
claim Hprop:
∀y ∈ V, SNo y → apply_fun r_of u ≤ y.
We prove the intermediate
claim Hepsc_in_V:
apply_fun eps c ∈ V.
We prove the intermediate
claim HepscS:
SNo (apply_fun eps c).
Let c0 be given.
Assume Hc0Su.
Assume Heq.
rewrite the current goal using Heq (from left to right).
We prove the intermediate
claim HSu_subC:
apply_fun S_of u ⊆ C.
We prove the intermediate
claim Hc0C:
c0 ∈ C.
An exact proof term for the current goal is (HSu_subC c0 Hc0Su).
We prove the intermediate
claim Hepsc0R:
apply_fun eps c0 ∈ R.
An
exact proof term for the current goal is
(Hprop (apply_fun eps c) Hepsc_in_V HepscS).
We prove the intermediate
claim HrR:
apply_fun r_of u ∈ R.
We prove the intermediate
claim HrInV:
apply_fun r_of u ∈ V.
Let c0 be given.
Assume Hc0Su.
Assume Heq.
rewrite the current goal using Heq (from left to right).
We prove the intermediate
claim HSu_subC:
apply_fun S_of u ⊆ C.
We prove the intermediate
claim Hc0C:
c0 ∈ C.
An exact proof term for the current goal is (HSu_subC c0 Hc0Su).
We prove the intermediate
claim HepscR:
apply_fun eps c ∈ R.
We prove the intermediate
claim HSu_subC:
apply_fun S_of u ⊆ C.
We prove the intermediate
claim HcC:
c ∈ C.
An exact proof term for the current goal is (HSu_subC c HcSu).
rewrite the current goal using Heq (from right to left) at position 2.
An exact proof term for the current goal is HltS.
Let u and A be given.
We prove the intermediate
claim HAinSu:
A ∈ apply_fun S_of u.
We prove the intermediate
claim HSuProp:
∀B : set, B ∈ C → B ∩ u ≠ Empty → B ∈ apply_fun S_of u.
An exact proof term for the current goal is (HSuProp A HA Hmeet).
An exact proof term for the current goal is (Hr_of_le_on_S u A HuU HAinSu).
We prove the intermediate
claim Hr_of_pos:
∀u : set, u ∈ U → Rlt 0 (apply_fun r_of u).
Let u be given.
An
exact proof term for the current goal is
Rlt_0_1.
An exact proof term for the current goal is (Hr_of_min u HuU HSuNe).
We prove the intermediate
claim HrInV:
apply_fun r_of u ∈ V.
Let c0 be given.
Assume Hc0Su.
Assume Heq.
rewrite the current goal using Heq (from left to right).
We prove the intermediate
claim HSu_subC:
apply_fun S_of u ⊆ C.
We prove the intermediate
claim Hc0C:
c0 ∈ C.
An exact proof term for the current goal is (HSu_subC c0 Hc0Su).
We prove the intermediate
claim Hcoef_pos:
∀f : set, f ∈ P → Rlt 0 (apply_fun coef_of f).
Let f be given.
We prove the intermediate
claim HuU:
apply_fun u_of f ∈ U.
An
exact proof term for the current goal is
(Hr_of_pos (apply_fun u_of f) HuU).
We prove the intermediate
claim Hnonzero_in_support:
∀f x : set, f ∈ P → x ∈ X → apply_fun f x ≠ 0 → x ∈ support_of X Tx f.
Let f and x be given.
We prove the intermediate
claim HxA0:
x ∈ A0.
An
exact proof term for the current goal is
(SepI X (λz : set ⇒ apply_fun f z ≠ 0) x HxX Hnx0).
We prove the intermediate
claim HA0subX:
A0 ⊆ X.
We prove the intermediate
claim HA0subCl:
A0 ⊆ closure_of X Tx A0.
An exact proof term for the current goal is (HA0subCl x HxA0).
Let f, A and x be given.
We prove the intermediate
claim HxSupp:
x ∈ support_of X Tx f.
An exact proof term for the current goal is (Hnonzero_in_support f x HfP HxX Hnx0).
An exact proof term for the current goal is (Hu_of f HfP).
We prove the intermediate
claim HxU:
x ∈ apply_fun u_of f.
An exact proof term for the current goal is (HSuppSubU x HxSupp).
We prove the intermediate
claim HxCap:
x ∈ A ∩ (apply_fun u_of f).
We prove the intermediate
claim HxEmpty:
x ∈ Empty.
rewrite the current goal using Hcap0 (from right to left).
An exact proof term for the current goal is HxCap.
An
exact proof term for the current goal is
(EmptyE x HxEmpty).
Let f, A and x be given.
An exact proof term for the current goal is (Hu_of f HfP).
We prove the intermediate
claim HuU:
apply_fun u_of f ∈ U.
An exact proof term for the current goal is (Hu_of_meets f A x HfP HA HxX HxA Hnx0).
An
exact proof term for the current goal is
(Hr_of_le_on_hits (apply_fun u_of f) A HuU HA Hmeet).
Set weighted_sum to be the term
λx : set ⇒ λn e : set ⇒ nat_primrec 0 (weighted_step x e) n.
We prove the intermediate
claim weighted_sum_0:
∀x e : set, weighted_sum x 0 e = 0.
Let x and e be given.
We prove the intermediate
claim Hdef:
weighted_sum x 0 e = nat_primrec 0 (weighted_step x e) 0.
rewrite the current goal using Hdef (from left to right).
An
exact proof term for the current goal is
(nat_primrec_0 0 (weighted_step x e)).
We prove the intermediate
claim weighted_sum_S:
∀x e n : set, nat_p n → weighted_sum x (ordsucc n) e = weighted_step x e n (weighted_sum x n e).
Let x, e and n be given.
rewrite the current goal using HdefS (from left to right).
An
exact proof term for the current goal is
(nat_primrec_S 0 (weighted_step x e) n HnNat).
rewrite the current goal using HprimS (from left to right).
Use reflexivity.
We prove the intermediate
claim weighted_step_congr_acc:
∀x e k acc1 acc2 : set, acc1 = acc2 → weighted_step x e k acc1 = weighted_step x e k acc2.
Let x, e, k, acc1 and acc2 be given.
rewrite the current goal using Hacc (from left to right).
Use reflexivity.
We prove the intermediate
claim weighted_step_congr_e_at:
∀x e1 e2 k acc : set, apply_fun e1 k = apply_fun e2 k → weighted_step x e1 k acc = weighted_step x e2 k acc.
Let x, e1, e2, k and acc be given.
rewrite the current goal using Hdef1 (from left to right).
rewrite the current goal using Hdef2 (from left to right).
rewrite the current goal using Heq (from left to right).
Use reflexivity.
Let e, m and i be given.
rewrite the current goal using Hdef (from left to right).
Use reflexivity.
Let e, i, n and j be given.
rewrite the current goal using Hdef (from left to right).
Use reflexivity.
Let e, i and n be given.
rewrite the current goal using Hsa (from left to right).
We prove the intermediate
claim Hneq:
¬ (ordsucc i = i).
We prove the intermediate
claim Hii:
i ∈ i.
rewrite the current goal using Heq (from right to left) at position 2.
An
exact proof term for the current goal is
(ordsuccI2 i).
An
exact proof term for the current goal is
((In_irref i) Hii).
Use reflexivity.
Let F, e, i and n be given.
Let j be given.
We prove the intermediate
claim Hsubst:
∀S T : set, S = T → T ∈ F → S ∈ F.
Let S and T be given.
rewrite the current goal using HeqST (from left to right).
An exact proof term for the current goal is HT.
Apply (xm (j = i)) to the current goal.
An
exact proof term for the current goal is
(HeFun (ordsucc i) HsiDom).
An exact proof term for the current goal is (HeFun i HiDom).
An exact proof term for the current goal is (HeFun j HjDom).
Let F, e, i and n be given.
We prove the intermediate
claim HeFun:
function_on e n F.
We prove the intermediate
claim Huniq:
∀y : set, y ∈ F → ∃x0 : set, x0 ∈ n ∧ apply_fun e x0 = y ∧ (∀x' : set, x' ∈ n → apply_fun e x' = y → x' = x0).
Apply andI to the current goal.
Let y be given.
Apply (Huniq y HyF) to the current goal.
Let x0 be given.
Assume Hx0pack.
We prove the intermediate
claim Hx0AB:
x0 ∈ n ∧ apply_fun e x0 = y.
We prove the intermediate
claim Hx0Dom:
x0 ∈ n.
An
exact proof term for the current goal is
(andEL (x0 ∈ n) (apply_fun e x0 = y) Hx0AB).
We prove the intermediate
claim Hex0:
apply_fun e x0 = y.
An
exact proof term for the current goal is
(andER (x0 ∈ n) (apply_fun e x0 = y) Hx0AB).
We prove the intermediate
claim Hx1Dom:
x1 ∈ n.
rewrite the current goal using Hx1Def (from left to right) at position 1.
Apply (xm (x0 = i)) to the current goal.
An exact proof term for the current goal is HsiDom.
rewrite the current goal using
(If_i_1 (x0 = ordsucc i) i x0 Hx0si) (from left to right).
An exact proof term for the current goal is HiDom.
rewrite the current goal using
(If_i_0 (x0 = ordsucc i) i x0 Hx0nsi) (from left to right).
An exact proof term for the current goal is Hx0Dom.
rewrite the current goal using Hsa (from left to right).
rewrite the current goal using Hx1Def (from left to right) at position 1.
Apply (xm (x0 = i)) to the current goal.
We prove the intermediate
claim Hneq:
¬ (ordsucc i = i).
We prove the intermediate
claim HiIn:
i ∈ i.
rewrite the current goal using Heq (from right to left) at position 2.
An
exact proof term for the current goal is
(ordsuccI2 i).
An
exact proof term for the current goal is
((In_irref i) HiIn).
rewrite the current goal using Hx0i (from right to left) at position 1.
An exact proof term for the current goal is Hex0.
rewrite the current goal using
(If_i_1 (x0 = ordsucc i) i x0 Hx0si) (from left to right).
We prove the intermediate
claim Hii:
i = i.
rewrite the current goal using Hx0si (from right to left) at position 1.
An exact proof term for the current goal is Hex0.
rewrite the current goal using
(If_i_0 (x0 = ordsucc i) i x0 Hx0nsi) (from left to right).
An exact proof term for the current goal is Hex0.
We use x1 to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hx1Dom.
An exact proof term for the current goal is Hx1Eq.
Let x' be given.
We prove the intermediate
claim Hx0Uniq:
∀z : set, z ∈ n → apply_fun e z = y → z = x0.
We prove the intermediate
claim Hx2Dom:
x2 ∈ n.
rewrite the current goal using Hx2Def (from left to right) at position 1.
Apply (xm (x' = i)) to the current goal.
An exact proof term for the current goal is HsiDom.
rewrite the current goal using
(If_i_1 (x' = ordsucc i) i x' Hx'si) (from left to right).
An exact proof term for the current goal is HiDom.
rewrite the current goal using
(If_i_0 (x' = ordsucc i) i x' Hx'nsi) (from left to right).
An exact proof term for the current goal is Hx'Dom.
rewrite the current goal using Hsa' (from right to left) at position 1.
An exact proof term for the current goal is HsxEq.
We prove the intermediate
claim Hx2Ey:
apply_fun e x2 = y.
Apply (xm (x' = i)) to the current goal.
rewrite the current goal using Hx2Def (from left to right) at position 1.
An exact proof term for the current goal is HifEq.
rewrite the current goal using Hx2Def (from left to right) at position 1.
rewrite the current goal using
(If_i_1 (x' = ordsucc i) i x' Hx'si) (from left to right).
An exact proof term for the current goal is HifEq.
rewrite the current goal using Hx2Def (from left to right) at position 1.
rewrite the current goal using
(If_i_0 (x' = ordsucc i) i x' Hx'nsi) (from left to right).
An exact proof term for the current goal is HifEq.
We prove the intermediate
claim Hx2x0:
x2 = x0.
An exact proof term for the current goal is (Hx0Uniq x2 Hx2Dom Hx2Ey).
We prove the intermediate
claim Hneqsi:
¬ (ordsucc i = i).
We prove the intermediate
claim HiIn:
i ∈ i.
rewrite the current goal using Heq (from right to left) at position 2.
An
exact proof term for the current goal is
(ordsuccI2 i).
An
exact proof term for the current goal is
((In_irref i) HiIn).
Apply (xm (x0 = i)) to the current goal.
rewrite the current goal using Hx1Def (from left to right) at position 1.
rewrite the current goal using
(If_i_1 (x0 = i) (ordsucc i) (If_i (x0 = ordsucc i) i x0) Hx0i) (from left to right) at position 1.
We prove the intermediate
claim Hx2i:
x2 = i.
rewrite the current goal using Hx2x0 (from left to right) at position 1.
An exact proof term for the current goal is Hx0i.
An exact proof term for the current goal is Hx'si.
Apply FalseE to the current goal.
Apply (xm (x' = i)) to the current goal.
We prove the intermediate
claim Hx2si:
x2 = ordsucc i.
rewrite the current goal using Hx2Def (from left to right) at position 1.
Use reflexivity.
We prove the intermediate
claim HsiEq:
ordsucc i = i.
rewrite the current goal using Hx2si (from right to left) at position 1.
An exact proof term for the current goal is Hx2i.
An exact proof term for the current goal is (Hneqsi HsiEq).
We prove the intermediate
claim Hx2Eqx':
x2 = x'.
rewrite the current goal using Hx2Def (from left to right) at position 1.
rewrite the current goal using
(If_i_0 (x' = ordsucc i) i x' Hx'nsi) (from left to right).
Use reflexivity.
We prove the intermediate
claim Hx'i:
x' = i.
rewrite the current goal using Hx2Eqx' (from right to left) at position 1.
An exact proof term for the current goal is Hx2i.
An exact proof term for the current goal is (Hx'ni Hx'i).
rewrite the current goal using Hx1Def (from left to right) at position 1.
rewrite the current goal using
(If_i_0 (x0 = i) (ordsucc i) (If_i (x0 = ordsucc i) i x0) Hx0ni) (from left to right) at position 1.
rewrite the current goal using
(If_i_1 (x0 = ordsucc i) i x0 Hx0si) (from left to right) at position 1.
We prove the intermediate
claim Hx2si:
x2 = ordsucc i.
rewrite the current goal using Hx2x0 (from left to right) at position 1.
An exact proof term for the current goal is Hx0si.
Apply (xm (x' = i)) to the current goal.
An exact proof term for the current goal is Hx'i.
Apply FalseE to the current goal.
We prove the intermediate
claim Hx2i:
x2 = i.
rewrite the current goal using Hx2Def (from left to right) at position 1.
rewrite the current goal using
(If_i_1 (x' = ordsucc i) i x' Hx'si) (from left to right).
Use reflexivity.
We prove the intermediate
claim HsiEq:
ordsucc i = i.
rewrite the current goal using Hx2si (from right to left) at position 1.
An exact proof term for the current goal is Hx2i.
An exact proof term for the current goal is (Hneqsi HsiEq).
We prove the intermediate
claim Hx2Eqx':
x2 = x'.
rewrite the current goal using Hx2Def (from left to right) at position 1.
rewrite the current goal using
(If_i_0 (x' = ordsucc i) i x' Hx'nsi) (from left to right).
Use reflexivity.
We prove the intermediate
claim Hx'si2:
x' = ordsucc i.
rewrite the current goal using Hx2Eqx' (from right to left) at position 1.
An exact proof term for the current goal is Hx2si.
An exact proof term for the current goal is (Hx'nsi Hx'si2).
rewrite the current goal using Hx1Def (from left to right) at position 1.
rewrite the current goal using
(If_i_0 (x0 = i) (ordsucc i) (If_i (x0 = ordsucc i) i x0) Hx0ni) (from left to right) at position 1.
rewrite the current goal using
(If_i_0 (x0 = ordsucc i) i x0 Hx0nsi) (from left to right) at position 1.
Apply (xm (x' = i)) to the current goal.
Apply FalseE to the current goal.
We prove the intermediate
claim Hx2si:
x2 = ordsucc i.
rewrite the current goal using Hx2Def (from left to right) at position 1.
Use reflexivity.
We prove the intermediate
claim Hx0si:
x0 = ordsucc i.
rewrite the current goal using Hx2x0 (from right to left) at position 1.
An exact proof term for the current goal is Hx2si.
An exact proof term for the current goal is (Hx0nsi Hx0si).
Apply FalseE to the current goal.
We prove the intermediate
claim Hx2i:
x2 = i.
rewrite the current goal using Hx2Def (from left to right) at position 1.
rewrite the current goal using
(If_i_1 (x' = ordsucc i) i x' Hx'si) (from left to right).
Use reflexivity.
We prove the intermediate
claim Hx0i:
x0 = i.
rewrite the current goal using Hx2x0 (from right to left) at position 1.
An exact proof term for the current goal is Hx2i.
An exact proof term for the current goal is (Hx0ni Hx0i).
We prove the intermediate
claim Hx2Eqx':
x2 = x'.
rewrite the current goal using Hx2Def (from left to right) at position 1.
rewrite the current goal using
(If_i_0 (x' = ordsucc i) i x' Hx'nsi) (from left to right).
Use reflexivity.
rewrite the current goal using Hx2Eqx' (from right to left) at position 1.
An exact proof term for the current goal is Hx2x0.
Let F, e and m be given.
Let i be given.
rewrite the current goal using Hdef (from left to right) at position 1.
Apply (xm (i = m)) to the current goal.
An
exact proof term for the current goal is
(HeFun (ordsucc m) HsmDom).
An exact proof term for the current goal is (HeFun m HmDom).
An exact proof term for the current goal is (HeFun i HiDom).
Let e, m and i be given.
rewrite the current goal using Hdef (from left to right) at position 1.
We prove the intermediate
claim Hneq1:
¬ (i = m).
We prove the intermediate
claim HmIn:
m ∈ m.
rewrite the current goal using Heq (from right to left) at position 1.
An exact proof term for the current goal is HiIn.
An
exact proof term for the current goal is
((In_irref m) HmIn).
We prove the intermediate
claim Hneq2:
¬ (i = ordsucc m).
We prove the intermediate
claim HsmIn:
ordsucc m ∈ m.
rewrite the current goal using Heq (from right to left) at position 1.
An exact proof term for the current goal is HiIn.
We prove the intermediate
claim HmOrd:
ordinal m.
An
exact proof term for the current goal is
(nat_p_ordinal m HmNat).
We prove the intermediate
claim HmTS:
TransSet m.
We prove the intermediate
claim HsmSub:
ordsucc m ⊆ m.
An
exact proof term for the current goal is
(HmTS (ordsucc m) HsmIn).
We prove the intermediate
claim HmIn:
m ∈ m.
An
exact proof term for the current goal is
(HsmSub m (ordsuccI2 m)).
An
exact proof term for the current goal is
((In_irref m) HmIn).
Use reflexivity.
Let e and m be given.
rewrite the current goal using Hdef (from left to right) at position 1.
We prove the intermediate
claim Hmm:
m = m.
Use reflexivity.
Let e and m be given.
rewrite the current goal using Hdef (from left to right) at position 1.
We prove the intermediate
claim Hneq:
¬ (ordsucc m = m).
We prove the intermediate
claim HmIn:
m ∈ m.
rewrite the current goal using Heq (from right to left) at position 2.
An
exact proof term for the current goal is
(ordsuccI2 m).
An
exact proof term for the current goal is
((In_irref m) HmIn).
Use reflexivity.
Let F, e and m be given.
Apply andI to the current goal.
Let y be given.
Apply (Huniq y HyF) to the current goal.
Let x0 be given.
Assume Hx0pack.
We prove the intermediate
claim Hex0:
apply_fun e x0 = y.
rewrite the current goal using Hx1Def (from left to right) at position 1.
Apply (xm (x0 = m)) to the current goal.
rewrite the current goal using
(If_i_1 (x0 = ordsucc m) m x0 Hx0sm) (from left to right).
rewrite the current goal using
(If_i_0 (x0 = ordsucc m) m x0 Hx0nsm) (from left to right).
An exact proof term for the current goal is Hx0Dom.
rewrite the current goal using Hx1Def (from left to right) at position 1.
Apply (xm (x0 = m)) to the current goal.
rewrite the current goal using Hdef2 (from left to right) at position 1.
We prove the intermediate
claim Hneq:
¬ (ordsucc m = m).
We prove the intermediate
claim HmIn:
m ∈ m.
rewrite the current goal using Heq (from right to left) at position 2.
An
exact proof term for the current goal is
(ordsuccI2 m).
An
exact proof term for the current goal is
((In_irref m) HmIn).
rewrite the current goal using Hx0m (from right to left) at position 1.
An exact proof term for the current goal is Hex0.
rewrite the current goal using
(If_i_1 (x0 = ordsucc m) m x0 Hx0sm) (from left to right).
rewrite the current goal using Hdef2 (from left to right) at position 1.
We prove the intermediate
claim Hmm:
m = m.
rewrite the current goal using Hx0sm (from right to left) at position 1.
An exact proof term for the current goal is Hex0.
rewrite the current goal using
(If_i_0 (x0 = ordsucc m) m x0 Hx0nsm) (from left to right).
We prove the intermediate
claim Hx0InSm:
x0 ∈ ordsucc m.
An
exact proof term for the current goal is
(ordsuccE (ordsucc m) x0 Hx0Dom).
Apply (Hcase (x0 ∈ ordsucc m)) to the current goal.
An exact proof term for the current goal is Hx0In.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hx0nsm Hx0Eq).
We prove the intermediate
claim Hx0InM:
x0 ∈ m.
We prove the intermediate
claim Hcase:
x0 ∈ m ∨ x0 = m.
An
exact proof term for the current goal is
(ordsuccE m x0 Hx0InSm).
Apply (Hcase (x0 ∈ m)) to the current goal.
An exact proof term for the current goal is Hx0In.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hx0nm Hx0Eq).
rewrite the current goal using Hdef3 (from left to right) at position 1.
An exact proof term for the current goal is Hex0.
We use x1 to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hx1Dom.
An exact proof term for the current goal is Hx1Eq.
Let x' be given.
An
exact proof term for the current goal is
(ordsuccE (ordsucc m) x' Hx'Dom).
Apply (Hx'case (x' = x1)) to the current goal.
We prove the intermediate
claim Hx'case2:
x' ∈ m ∨ x' = m.
An
exact proof term for the current goal is
(ordsuccE m x' Hx'InSm).
Apply (Hx'case2 (x' = x1)) to the current goal.
We prove the intermediate
claim HyEqE:
apply_fun e x' = y.
rewrite the current goal using (swap_last_two_agree_lt e m x' HmNat Hx'InM) (from right to left) at position 1.
An exact proof term for the current goal is Hx'Eq.
We prove the intermediate
claim Hx'x0:
x' = x0.
An exact proof term for the current goal is (Huniq0 x' Hx'Dom HyEqE).
Apply (xm (x0 = m)) to the current goal.
Apply FalseE to the current goal.
We prove the intermediate
claim Hx'm:
x' = m.
rewrite the current goal using Hx'x0 (from left to right) at position 1.
An exact proof term for the current goal is Hx0m.
We prove the intermediate
claim HmIn:
m ∈ m.
rewrite the current goal using Hx'm (from right to left) at position 1.
An exact proof term for the current goal is Hx'InM.
An
exact proof term for the current goal is
((In_irref m) HmIn).
Apply FalseE to the current goal.
We prove the intermediate
claim Hx'sm:
x' = ordsucc m.
rewrite the current goal using Hx'x0 (from left to right) at position 1.
An exact proof term for the current goal is Hx0sm.
We prove the intermediate
claim HsmIn:
ordsucc m ∈ m.
rewrite the current goal using Hx'sm (from right to left) at position 1.
An exact proof term for the current goal is Hx'InM.
We prove the intermediate
claim HmOrd:
ordinal m.
An
exact proof term for the current goal is
(nat_p_ordinal m HmNat).
We prove the intermediate
claim HmTS:
TransSet m.
We prove the intermediate
claim HsmSub:
ordsucc m ⊆ m.
An
exact proof term for the current goal is
(HmTS (ordsucc m) HsmIn).
We prove the intermediate
claim HmIn:
m ∈ m.
An
exact proof term for the current goal is
(HsmSub m (ordsuccI2 m)).
An
exact proof term for the current goal is
((In_irref m) HmIn).
rewrite the current goal using
(If_i_0 (x0 = ordsucc m) m x0 Hx0nsm) (from left to right).
rewrite the current goal using Hx'x0 (from right to left) at position 1.
Use reflexivity.
rewrite the current goal using Hx'm (from right to left) at position 2.
An exact proof term for the current goal is Hx'Eq.
rewrite the current goal using
(swap_last_two_at_m e m HmNat) (from right to left) at position 1.
An exact proof term for the current goal is Htmp.
We prove the intermediate
claim Hx0sm0:
ordsucc m = x0.
We prove the intermediate
claim Hx0sm:
x0 = ordsucc m.
Use symmetry.
An exact proof term for the current goal is Hx0sm0.
Apply (xm (x0 = m)) to the current goal.
Apply FalseE to the current goal.
We prove the intermediate
claim Heq:
m = ordsucc m.
rewrite the current goal using Hx0m (from right to left) at position 1.
An exact proof term for the current goal is Hx0sm.
We prove the intermediate
claim HmIn:
m ∈ m.
rewrite the current goal using Heq (from left to right) at position 2.
An
exact proof term for the current goal is
(ordsuccI2 m).
An
exact proof term for the current goal is
((In_irref m) HmIn).
rewrite the current goal using
(If_i_1 (x0 = ordsucc m) m x0 Hx0sm) (from left to right).
rewrite the current goal using Hx'm (from right to left) at position 1.
Use reflexivity.
We prove the intermediate
claim HyEqE:
apply_fun e m = y.
rewrite the current goal using Hx'sm (from right to left) at position 1.
An exact proof term for the current goal is Hx'Eq.
rewrite the current goal using
(swap_last_two_at_sm e m HmNat) (from right to left) at position 1.
An exact proof term for the current goal is Htmp.
We prove the intermediate
claim Hx0m0:
m = x0.
We prove the intermediate
claim Hx0m:
x0 = m.
Use symmetry.
An exact proof term for the current goal is Hx0m0.
rewrite the current goal using Hx'sm (from right to left) at position 1.
Use reflexivity.
We prove the intermediate
claim weighted_sum_congr:
∀x n e1 e2 : set, nat_p n → (∀k : set, k ∈ n → apply_fun e1 k = apply_fun e2 k) → weighted_sum x n e1 = weighted_sum x n e2.
Let x, n, e1 and e2 be given.
We prove the intermediate
claim Hdef1:
weighted_sum x n e1 = nat_primrec 0 (weighted_step x e1) n.
We prove the intermediate
claim Hdef2:
weighted_sum x n e2 = nat_primrec 0 (weighted_step x e2) n.
rewrite the current goal using Hdef1 (from left to right).
rewrite the current goal using Hdef2 (from left to right).
We prove the intermediate
claim HP0:
Pws 0.
Let eA and eB be given.
rewrite the current goal using
(nat_primrec_0 0 (weighted_step x eA)) (from left to right).
rewrite the current goal using
(nat_primrec_0 0 (weighted_step x eB)) (from left to right).
Use reflexivity.
We prove the intermediate
claim HPS:
∀m : set, nat_p m → Pws m → Pws (ordsucc m).
Let m be given.
Assume IHm: Pws m.
Let eA and eB be given.
rewrite the current goal using
(nat_primrec_S 0 (weighted_step x eA) m HmNat) (from left to right).
rewrite the current goal using
(nat_primrec_S 0 (weighted_step x eB) m HmNat) (from left to right).
Let k be given.
An
exact proof term for the current goal is
(HeqS k (ordsuccI1 m k Hk)).
An exact proof term for the current goal is (IHm eA eB Heqm).
An
exact proof term for the current goal is
(HeqS m (ordsuccI2 m)).
rewrite the current goal using Hacc (from left to right).
rewrite the current goal using Hem (from left to right).
Use reflexivity.
We prove the intermediate claim HnP: Pws n.
An
exact proof term for the current goal is
(nat_ind Pws HP0 HPS n HnNat).
An exact proof term for the current goal is (HnP e1 e2 Heq).
Let x, e and m be given.
An
exact proof term for the current goal is
(nat_ordsucc m HmNat).
We prove the intermediate
claim Hm_congr:
weighted_sum x m (swap_last_two e m) = weighted_sum x m e.
Apply (weighted_sum_congr x m (swap_last_two e m) e HmNat) to the current goal.
Let k be given.
An exact proof term for the current goal is (swap_last_two_agree_lt e m k HmNat HkIn).
We prove the intermediate
claim HtmS:
SNo tm.
rewrite the current goal using HtmDef0 (from left to right).
An exact proof term for the current goal is Hterm_mS.
We prove the intermediate
claim HtsmS:
SNo tsm.
rewrite the current goal using HtsmDef0 (from left to right).
An exact proof term for the current goal is Hterm_smS.
An
exact proof term for the current goal is
(weighted_sum_S x (swap_last_two e m) m HmNat).
rewrite the current goal using HwsS (from left to right).
rewrite the current goal using Hm_congr (from left to right).
rewrite the current goal using HstepDef (from left to right).
rewrite the current goal using HyDef (from right to left) at position 1.
rewrite the current goal using HyDef (from right to left) at position 1.
rewrite the current goal using HyDef (from left to right).
rewrite the current goal using Hy (from left to right) at position 1.
rewrite the current goal using Hy (from left to right) at position 1.
rewrite the current goal using HtsmDef (from left to right) at position 1.
Use reflexivity.
We prove the intermediate
claim Hws_sm:
weighted_sum x (ordsucc m) e = add_SNo (weighted_sum x m e) tm.
We prove the intermediate
claim HwsS:
weighted_sum x (ordsucc m) e = weighted_step x e m (weighted_sum x m e).
An exact proof term for the current goal is (weighted_sum_S x e m HmNat).
rewrite the current goal using HwsS (from left to right).
Use reflexivity.
An
exact proof term for the current goal is
(weighted_sum_S x (swap_last_two e m) (ordsucc m) HsmNat).
rewrite the current goal using HwsS (from left to right).
rewrite the current goal using Hws_sm_swap (from left to right).
rewrite the current goal using HstepDef (from left to right).
rewrite the current goal using HyDef (from right to left) at position 1.
rewrite the current goal using HyDef (from right to left) at position 1.
We prove the intermediate
claim Hy:
y = apply_fun e m.
rewrite the current goal using HyDef (from left to right).
rewrite the current goal using Hy (from left to right) at position 1.
rewrite the current goal using Hy (from left to right) at position 1.
rewrite the current goal using HtmDef (from left to right) at position 1.
Use reflexivity.
An
exact proof term for the current goal is
(weighted_sum_S x e (ordsucc m) HsmNat).
rewrite the current goal using HwsS (from left to right).
rewrite the current goal using Hws_sm (from left to right).
Use reflexivity.
rewrite the current goal using Hws_ssm_swap (from left to right).
rewrite the current goal using Hws_ssm (from left to right).
We prove the intermediate
claim Hs_tmS:
SNo (add_SNo (weighted_sum x m e) tm).
An
exact proof term for the current goal is
(SNo_add_SNo (weighted_sum x m e) tm HaccS HtmS).
We prove the intermediate
claim Hs_tsmS:
SNo (add_SNo (weighted_sum x m e) tsm).
An
exact proof term for the current goal is
(SNo_add_SNo (weighted_sum x m e) tsm HaccS HtsmS).
An
exact proof term for the current goal is
(add_SNo_com_3b_1_2 (weighted_sum x m e) tsm tm HaccS HtsmS HtmS).
Let x, e and m be given.
We prove the intermediate
claim HwsS:
SNo (weighted_sum x m e).
An
exact proof term for the current goal is
(real_SNo (weighted_sum x m e) HwsR).
An exact proof term for the current goal is (weighted_sum_swap_last_two x e m HmNat HwsS Hterm_mS Hterm_smS).
Let x, e and m be given.
An
exact proof term for the current goal is
(nat_ordsucc m HmNat).
Let k be given.
rewrite the current goal using Hsa (from left to right).
rewrite the current goal using Hsl (from left to right).
Use reflexivity.
rewrite the current goal using Hcongr (from left to right).
An exact proof term for the current goal is (weighted_sum_swap_last_two_real x e m HmNat HwsR Hcoef_mR Hval_mR Hcoef_smR Hval_smR).
Let x, y and z be given.
We prove the intermediate
claim HxS:
SNo x.
An
exact proof term for the current goal is
(real_SNo x HxR).
We prove the intermediate
claim HyS:
SNo y.
An
exact proof term for the current goal is
(real_SNo y HyR).
We prove the intermediate
claim HzS:
SNo z.
An
exact proof term for the current goal is
(real_SNo z HzR).
Let x, e and n be given.
We prove the intermediate
claim HR:
weighted_sum x n e = nat_primrec 0 (weighted_step x e) n.
rewrite the current goal using HL (from left to right).
rewrite the current goal using HR (from left to right).
rewrite the current goal using
(nat_primrec_S 0 (weighted_step x e) n HnNat) (from left to right).
We prove the intermediate
claim HaccR:
acc ∈ R.
rewrite the current goal using HR (from right to left).
An exact proof term for the current goal is HwsR.
We prove the intermediate
claim HaccS:
SNo acc.
An
exact proof term for the current goal is
(real_SNo acc HaccR).
rewrite the current goal using Hval0 (from left to right).
rewrite the current goal using Hterm0 (from left to right).
An
exact proof term for the current goal is
(add_SNo_0R acc HaccS).
Let x, e, k and acc be given.
We prove the intermediate
claim HaccS:
SNo acc.
An
exact proof term for the current goal is
(real_SNo acc HaccR).
rewrite the current goal using Hdef (from left to right).
rewrite the current goal using Hval0 (from left to right).
rewrite the current goal using Hterm0 (from left to right).
An
exact proof term for the current goal is
(add_SNo_0R acc HaccS).
Let x, n and e be given.
Let m be given.
We prove the intermediate
claim HnNat:
nat_p n.
An
exact proof term for the current goal is
(omega_nat_p n HnO).
Set Pws to be the term
λt : set ⇒ t ∈ ordsucc n → weighted_sum x t e ∈ R.
We prove the intermediate
claim Hind:
∀t : set, nat_p t → Pws t.
rewrite the current goal using (weighted_sum_0 x e) (from left to right).
An
exact proof term for the current goal is
real_0.
Let t be given.
Assume IHt: Pws t.
We prove the intermediate
claim HnOrd:
ordinal n.
An
exact proof term for the current goal is
(nat_p_ordinal n HnNat).
We prove the intermediate
claim HnTS:
TransSet n.
We prove the intermediate
claim HtInN:
t ∈ n.
An
exact proof term for the current goal is
(ordsuccE n (ordsucc t) HStIn).
Apply (Hcase (t ∈ n)) to the current goal.
We prove the intermediate
claim Hsub:
ordsucc t ⊆ n.
An
exact proof term for the current goal is
(HnTS (ordsucc t) HStInN).
An
exact proof term for the current goal is
(Hsub t (ordsuccI2 t)).
rewrite the current goal using Heq (from right to left).
An
exact proof term for the current goal is
(ordsuccI2 t).
We prove the intermediate
claim HtInSuccN:
t ∈ ordsucc n.
An
exact proof term for the current goal is
((ordsuccI1 n) t HtInN).
We prove the intermediate
claim HaccR:
weighted_sum x t e ∈ R.
An exact proof term for the current goal is (IHt HtInSuccN).
An exact proof term for the current goal is (HvalR t HtInN).
An exact proof term for the current goal is (HcoefR t HtInN).
We prove the intermediate
claim HwsS:
weighted_sum x (ordsucc t) e = weighted_step x e t (weighted_sum x t e).
An exact proof term for the current goal is (weighted_sum_S x e t HtNat).
We prove the intermediate
claim HstepR:
weighted_step x e t (weighted_sum x t e) ∈ R.
rewrite the current goal using Hdef (from left to right).
We prove the intermediate
claim Hsubst:
∀S T : set, S = T → T ∈ R → S ∈ R.
Let S and T be given.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is HT.
An
exact proof term for the current goal is
(Hsubst (weighted_sum x (ordsucc t) e) (weighted_step x e t (weighted_sum x t e)) HwsS HstepR).
We prove the intermediate
claim HsuccNO:
ordsucc n ∈ ω.
An
exact proof term for the current goal is
(omega_ordsucc n HnO).
We prove the intermediate
claim HsuccNsubO:
ordsucc n ⊆ ω.
We prove the intermediate
claim HmO:
m ∈ ω.
An exact proof term for the current goal is (HsuccNsubO m HmIn).
We prove the intermediate
claim HmNat:
nat_p m.
An
exact proof term for the current goal is
(omega_nat_p m HmO).
An exact proof term for the current goal is (Hind m HmNat HmIn).
Let x, m, F and e be given.
We prove the intermediate
claim HmNat:
nat_p m.
An
exact proof term for the current goal is
(omega_nat_p m HmO).
We prove the intermediate
claim HekP_m:
∀k : set, k ∈ m → apply_fun e k ∈ P.
Let k be given.
We prove the intermediate
claim HkDom:
k ∈ ordsucc m.
An
exact proof term for the current goal is
(ordsuccI1 m k HkM).
We prove the intermediate
claim HkF:
apply_fun e k ∈ F.
An exact proof term for the current goal is (Hefun k HkDom).
An
exact proof term for the current goal is
(HFsubP (apply_fun e k) HkF).
Let k be given.
We prove the intermediate
claim HkDom:
k ∈ ordsucc m.
An
exact proof term for the current goal is
(ordsuccI1 m k HkM).
We prove the intermediate
claim HkF:
apply_fun e k ∈ F.
An exact proof term for the current goal is (Hefun k HkDom).
An
exact proof term for the current goal is
(HvalR (apply_fun e k) HkF).
Let k be given.
We prove the intermediate
claim HkDom:
k ∈ ordsucc m.
An
exact proof term for the current goal is
(ordsuccI1 m k HkM).
We prove the intermediate
claim HkF:
apply_fun e k ∈ F.
An exact proof term for the current goal is (Hefun k HkDom).
An
exact proof term for the current goal is
(HcoefR (apply_fun e k) HkF).
We prove the intermediate
claim HwsRall:
∀t : set, t ∈ ordsucc m → weighted_sum x t e ∈ R.
An exact proof term for the current goal is (weighted_sum_prefix_in_R x m e HxX HmO HekP_m HekValR_m HekCoefR_m).
We prove the intermediate
claim HwsR:
weighted_sum x m e ∈ R.
An
exact proof term for the current goal is
(HwsRall m (ordsuccI2 m)).
We prove the intermediate
claim HmDom:
m ∈ ordsucc m.
An
exact proof term for the current goal is
(ordsuccI2 m).
We prove the intermediate
claim HmF:
apply_fun e m ∈ F.
An exact proof term for the current goal is (Hefun m HmDom).
An
exact proof term for the current goal is
(HcoefR (apply_fun e m) HmF).
An exact proof term for the current goal is (weighted_sum_S_drop_zero x e m HmNat HwsR Hval0 HcoefLastR).
Let x, e and m be given.
We prove the intermediate
claim HmNat:
nat_p m.
An
exact proof term for the current goal is
(omega_nat_p m HmO).
An
exact proof term for the current goal is
(nat_ordsucc m HmNat).
We prove the intermediate
claim HmIn1:
m ∈ ordsucc m.
An
exact proof term for the current goal is
(ordsuccI2 m).
We prove the intermediate
claim Hws_mR:
weighted_sum x m e ∈ R.
An
exact proof term for the current goal is
(weighted_sum_prefix_in_R x (ordsucc (ordsucc m)) e HxX HdomO HekP HvalR HcoefR m HmInS).
An exact proof term for the current goal is (HcoefR m HmIn2).
An exact proof term for the current goal is (HvalR m HmIn2).
An
exact proof term for the current goal is
(HcoefR (ordsucc m) HsmIn2).
An
exact proof term for the current goal is
(HvalR (ordsucc m) HsmIn2).
An exact proof term for the current goal is (weighted_sum_swap_last_two_real x e m HmNat Hws_mR Hcoef_mR Hval_mR Hcoef_smR Hval_smR).
Let k be given.
rewrite the current goal using HkEq (from left to right).
Apply (xm (k = m)) to the current goal.
An
exact proof term for the current goal is
(HekP (ordsucc m) HsmIn2).
An exact proof term for the current goal is (HekP m HmIn2).
An exact proof term for the current goal is (HekP k Hk).
Let k be given.
rewrite the current goal using HkEq (from left to right).
Apply (xm (k = m)) to the current goal.
An
exact proof term for the current goal is
(HvalR (ordsucc m) HsmIn2).
An exact proof term for the current goal is (HvalR m HmIn2).
An exact proof term for the current goal is (HvalR k Hk).
Let k be given.
rewrite the current goal using HkEq (from left to right).
Apply (xm (k = m)) to the current goal.
An
exact proof term for the current goal is
(HcoefR (ordsucc m) HsmIn2).
An exact proof term for the current goal is (HcoefR m HmIn2).
An exact proof term for the current goal is (HcoefR k Hk).
An
exact proof term for the current goal is
(weighted_sum_prefix_in_R x (ordsucc (ordsucc m)) (swap_last_two e m) HxX HdomO HekPswap HvalRswap HcoefRswap (ordsucc m) HsmInS).
rewrite the current goal using Hdef (from left to right).
We prove the intermediate
claim Hneq:
¬ (ordsucc m = m).
We prove the intermediate
claim Hmm:
m ∈ m.
rewrite the current goal using Heq (from right to left) at position 2.
An
exact proof term for the current goal is
(ordsuccI2 m).
An
exact proof term for the current goal is
((In_irref m) Hmm).
An exact proof term for the current goal is Hval0.
rewrite the current goal using Hdef (from left to right).
We prove the intermediate
claim Hneq:
¬ (ordsucc m = m).
We prove the intermediate
claim Hmm:
m ∈ m.
rewrite the current goal using Heq (from right to left) at position 2.
An
exact proof term for the current goal is
(ordsuccI2 m).
An
exact proof term for the current goal is
((In_irref m) Hmm).
An exact proof term for the current goal is Hcoef_mR.
An
exact proof term for the current goal is
(weighted_sum_S_drop_zero x (swap_last_two e m) (ordsucc m) HsmNat Hws_smR' HlastEq HcoefLastR).
rewrite the current goal using Hswap (from right to left).
An exact proof term for the current goal is Hdrop.
Let x, e, n and i be given.
We prove the intermediate
claim HnNat:
nat_p n.
An
exact proof term for the current goal is
(omega_nat_p n HnO).
We prove the intermediate
claim HP0:
Pn 0.
Let e0 and i0 be given.
Apply FalseE to the current goal.
An
exact proof term for the current goal is
(EmptyE i0 Hi0).
We prove the intermediate
claim HPS:
∀t : set, nat_p t → Pn t → Pn (ordsucc t).
Let t be given.
Assume IHt: Pn t.
Let e0 and i0 be given.
We prove the intermediate
claim HtO:
t ∈ ω.
An
exact proof term for the current goal is
(nat_p_omega t HtNat).
We prove the intermediate
claim HitCase:
i0 ∈ t ∨ i0 = t.
An
exact proof term for the current goal is
(ordsuccE t i0 HiS).
We prove the intermediate
claim HiT:
i0 ∈ t.
Apply (HitCase (i0 ∈ t)) to the current goal.
An exact proof term for the current goal is HiInT.
Apply FalseE to the current goal.
rewrite the current goal using HiEq (from right to left) at position 1.
An exact proof term for the current goal is HsiS.
An
exact proof term for the current goal is
(ordsuccE t (ordsucc i0) HsiS).
We prove the intermediate
claim HekP_t:
∀k : set, k ∈ t → apply_fun e0 k ∈ P.
Let k be given.
An
exact proof term for the current goal is
(HekP0 k (ordsuccI1 t k Hk)).
Let k be given.
An
exact proof term for the current goal is
(HcoefR0 k (ordsuccI1 t k Hk)).
Let k be given.
An
exact proof term for the current goal is
(HvalR0 k (ordsuccI1 t k Hk)).
We prove the intermediate
claim HtDom:
t ∈ ordsucc t.
An
exact proof term for the current goal is
(ordsuccI2 t).
An
exact proof term for the current goal is
(weighted_sum_S x (swap_adjacent e0 i0 (ordsucc t)) t HtNat).
We prove the intermediate
claim HwsR:
weighted_sum x (ordsucc t) e0 = weighted_step x e0 t (weighted_sum x t e0).
An exact proof term for the current goal is (weighted_sum_S x e0 t HtNat).
Let k be given.
We prove the intermediate
claim HkS:
k ∈ ordsucc t.
An
exact proof term for the current goal is
(ordsuccI1 t k Hk).
rewrite the current goal using Hsa1 (from left to right).
rewrite the current goal using Hsa2 (from left to right).
Use reflexivity.
We prove the intermediate
claim HaccEq:
weighted_sum x t (swap_adjacent e0 i0 (ordsucc t)) = weighted_sum x t e0.
rewrite the current goal using HcongrDom (from left to right).
An exact proof term for the current goal is (IHt e0 i0 HiT HsiT HekP_t HcoefR_t HvalR_t).
We prove the intermediate
claim HtNei:
¬ (t = i0).
We prove the intermediate
claim HtIn:
t ∈ t.
rewrite the current goal using Heq (from left to right) at position 1.
An exact proof term for the current goal is HiT.
An
exact proof term for the current goal is
((In_irref t) HtIn).
We prove the intermediate
claim HtNesi:
¬ (t = ordsucc i0).
We prove the intermediate
claim HtIn:
t ∈ t.
rewrite the current goal using Heq (from left to right) at position 1.
An exact proof term for the current goal is HsiT.
An
exact proof term for the current goal is
((In_irref t) HtIn).
rewrite the current goal using Hsa (from left to right).
Use reflexivity.
rewrite the current goal using HwsL (from left to right).
rewrite the current goal using HwsR (from left to right).
rewrite the current goal using HaccEq (from left to right).
An
exact proof term for the current goal is
(weighted_step_congr_e_at x (swap_adjacent e0 i0 (ordsucc t)) e0 t (weighted_sum x t e0) Hem).
We prove the intermediate
claim HiO:
i0 ∈ ω.
We prove the intermediate
claim HtSubO:
t ⊆ ω.
An exact proof term for the current goal is (HtSubO i0 HiT).
We prove the intermediate
claim HiNat:
nat_p i0.
An
exact proof term for the current goal is
(omega_nat_p i0 HiO).
We prove the intermediate
claim HwsRall:
∀m : set, m ∈ ordsucc t → weighted_sum x m e0 ∈ R.
An exact proof term for the current goal is (weighted_sum_prefix_in_R x t e0 HxX HtO HekP_t HvalR_t HcoefR_t).
We prove the intermediate
claim HwsR_i:
weighted_sum x i0 e0 ∈ R.
An
exact proof term for the current goal is
(HwsRall i0 (ordsuccI1 t i0 HiT)).
An
exact proof term for the current goal is
(HcoefR0 i0 (ordsuccI1 t i0 HiT)).
An
exact proof term for the current goal is
(HvalR0 i0 (ordsuccI1 t i0 HiT)).
rewrite the current goal using HsiEq (from left to right) at position 1.
An
exact proof term for the current goal is
(HcoefR0 t (ordsuccI2 t)).
rewrite the current goal using HsiEq (from left to right) at position 1.
An
exact proof term for the current goal is
(HvalR0 t (ordsuccI2 t)).
rewrite the current goal using HsiEq (from right to left).
An exact proof term for the current goal is (weighted_sum_swap_adjacent_last_real x e0 i0 HiNat HwsR_i Hcoef_i Hval_i Hcoef_si Hval_si).
We prove the intermediate claim HnP: Pn n.
An
exact proof term for the current goal is
(nat_ind Pn HP0 HPS n HnNat).
An exact proof term for the current goal is (HnP e i HiIn HsiIn HekP HcoefR HvalR).
Let x, e, n and i be given.
Apply andI to the current goal.
We prove the intermediate
claim Hswap:
weighted_sum x n (swap_adjacent e i n) = weighted_sum x n e.
An exact proof term for the current goal is (weighted_sum_swap_adjacent_real x e n i HxX HnO Hi Hsi HekP HcoefR HvalR).
rewrite the current goal using Hswap (from right to left).
Use reflexivity.
rewrite the current goal using Hinner (from left to right).
Use reflexivity.
rewrite the current goal using Houter (from left to right).
An exact proof term for the current goal is Hzero.
Let x, m, F0, e and flast be given.
We prove the intermediate
claim HmNat:
nat_p m.
An
exact proof term for the current goal is
(omega_nat_p m HmO).
We prove the intermediate
claim HP0:
Pm 0.
Let F1, e0 and fl be given.
Set e' to be the term e0.
We use e' to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hbij0.
Apply Hsurj to the current goal.
Let k be given.
Assume Hkpack.
We prove the intermediate
claim HkIn:
k ∈ ordsucc 0.
We prove the intermediate
claim HkEq:
apply_fun e0 k = fl.
We prove the intermediate
claim HkCase:
k ∈ 0 ∨ k = 0.
An
exact proof term for the current goal is
(ordsuccE 0 k HkIn).
We prove the intermediate
claim Hk0:
k = 0.
Apply (HkCase (k = 0)) to the current goal.
Apply FalseE to the current goal.
An
exact proof term for the current goal is
(EmptyE k HkIn0).
An exact proof term for the current goal is HkEq0.
rewrite the current goal using Hk0 (from right to left) at position 1.
An exact proof term for the current goal is HkEq.
We prove the intermediate
claim HPS:
∀t : set, nat_p t → Pm t → Pm (ordsucc t).
Let t be given.
Assume IHt: Pm t.
Let F1, e0 and fl be given.
We prove the intermediate
claim Hm1Def:
m1 = ordsucc t.
We prove the intermediate
claim HtO:
t ∈ ω.
An
exact proof term for the current goal is
(nat_p_omega t HtNat).
We prove the intermediate
claim Hm1Nat:
nat_p m1.
rewrite the current goal using Hm1Def (from left to right).
An
exact proof term for the current goal is
(nat_ordsucc t HtNat).
We prove the intermediate
claim Hm1O2:
m1 ∈ ω.
An
exact proof term for the current goal is
(nat_p_omega m1 Hm1Nat).
We prove the intermediate
claim HlastvalDef:
lastval = apply_fun e0 m1.
We prove the intermediate
claim HlastvalF1:
lastval ∈ F1.
rewrite the current goal using HlastvalDef (from left to right).
An
exact proof term for the current goal is
(He0fun m1 (ordsuccI2 m1)).
Apply (xm (fl = lastval)) to the current goal.
Set e' to be the term e0.
We use e' to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HbijS.
rewrite the current goal using HeqLast (from left to right).
rewrite the current goal using HlastvalDef (from left to right).
Use reflexivity.
We prove the intermediate
claim HflNot:
fl ∉ {lastval}.
We prove the intermediate
claim Heq:
fl = lastval.
An
exact proof term for the current goal is
(SingE lastval fl Hmem).
An exact proof term for the current goal is (HneqLast Heq).
We prove the intermediate
claim HflInDrop:
fl ∈ (F1 ∖ {lastval}).
An
exact proof term for the current goal is
(setminusI F1 {lastval} fl HflF1 HflNot).
rewrite the current goal using Hm1Def (from right to left).
rewrite the current goal using HlastvalDef (from right to left).
We prove the intermediate
claim HbijDrop2:
bijection m1 (F1 ∖ {lastval}) e0.
rewrite the current goal using HlastvalDef (from right to left) at position 1.
An exact proof term for the current goal is HbijDrop.
We prove the intermediate
claim HsubP':
(F1 ∖ {lastval}) ⊆ P.
We prove the intermediate
claim HvalR':
∀f : set, f ∈ (F1 ∖ {lastval}) → apply_fun f x ∈ R.
Let f be given.
An
exact proof term for the current goal is
(HvalR1 f (setminusE1 F1 {lastval} f Hf)).
We prove the intermediate
claim HcoefR':
∀f : set, f ∈ (F1 ∖ {lastval}) → apply_fun coef_of f ∈ R.
Let f be given.
An
exact proof term for the current goal is
(HcoefR1 f (setminusE1 F1 {lastval} f Hf)).
rewrite the current goal using Hm1Def (from right to left) at position 1.
An
exact proof term for the current goal is
(IHt (F1 ∖ {lastval}) e0 fl HtO HsubP' HvalR' HcoefR' HbijDrop2 HflInDrop).
Apply HmoveSmall to the current goal.
Let e1 be given.
Assume He1pack.
We prove the intermediate
claim HwsSmall:
weighted_sum x (ordsucc t) e0 = weighted_sum x (ordsucc t) e1.
We prove the intermediate
claim He1Val:
apply_fun e1 t = fl.
We prove the intermediate
claim HnDef:
n = ordsucc m1.
We prove the intermediate
claim HnO:
n ∈ ω.
rewrite the current goal using HnDef (from left to right).
We prove the intermediate
claim HtInN:
t ∈ n.
rewrite the current goal using HnDef (from left to right).
We prove the intermediate
claim Hm1InN:
m1 ∈ n.
rewrite the current goal using HnDef (from left to right).
An
exact proof term for the current goal is
(ordsuccI2 m1).
We prove the intermediate
claim He2fun:
function_on e2 n F1.
Let j be given.
rewrite the current goal using He2Def (from left to right).
We prove the intermediate
claim HjS:
j ∈ ordsucc m1.
rewrite the current goal using HnDef (from right to left) at position 1.
An exact proof term for the current goal is Hj.
We prove the intermediate
claim HjCase:
j ∈ m1 ∨ j = m1.
An
exact proof term for the current goal is
(ordsuccE m1 j HjS).
Apply (HjCase (apply_fun e2 j ∈ F1)) to the current goal.
rewrite the current goal using He2j (from left to right).
We prove the intermediate
claim Hjne:
¬ (j = m1).
We prove the intermediate
claim Hmm:
m1 ∈ m1.
rewrite the current goal using Heq (from right to left) at position 1.
An exact proof term for the current goal is HjInM1.
An
exact proof term for the current goal is
((In_irref m1) Hmm).
rewrite the current goal using
(If_i_0 (j = m1) lastval (apply_fun e1 j) Hjne) (from left to right).
We prove the intermediate
claim HjInDom:
j ∈ ordsucc t.
rewrite the current goal using Hm1Def (from right to left) at position 1.
An exact proof term for the current goal is HjInM1.
We prove the intermediate
claim HimgDrop:
apply_fun e1 j ∈ (F1 ∖ {lastval}).
An exact proof term for the current goal is (He1fun0 j HjInDom).
rewrite the current goal using He2j (from left to right).
rewrite the current goal using
(If_i_1 (j = m1) lastval (apply_fun e1 j) HjEqM1) (from left to right).
An exact proof term for the current goal is HlastvalF1.
We prove the intermediate
claim He2m1:
apply_fun e2 m1 = lastval.
We prove the intermediate
claim Hm1In:
m1 ∈ n.
An exact proof term for the current goal is Hm1InN.
rewrite the current goal using He2Def (from left to right).
rewrite the current goal using He2m1' (from left to right).
We prove the intermediate
claim Hrefl:
m1 = m1.
rewrite the current goal using
(If_i_1 (m1 = m1) lastval (apply_fun e1 m1) Hrefl) (from left to right).
Use reflexivity.
We prove the intermediate
claim He2t:
apply_fun e2 t = fl.
We prove the intermediate
claim HtIn:
t ∈ n.
An exact proof term for the current goal is HtInN.
rewrite the current goal using He2Def (from left to right).
rewrite the current goal using He2t' (from left to right).
We prove the intermediate
claim HtNe:
¬ (t = m1).
We prove the intermediate
claim Hmm:
m1 ∈ m1.
rewrite the current goal using Heq (from right to left) at position 1.
An
exact proof term for the current goal is
(ordsuccI2 t).
An
exact proof term for the current goal is
((In_irref m1) Hmm).
rewrite the current goal using
(If_i_0 (t = m1) lastval (apply_fun e1 t) HtNe) (from left to right).
rewrite the current goal using He1Val (from left to right).
Use reflexivity.
We prove the intermediate
claim He2bij:
bijection n F1 e2.
Apply andI to the current goal.
An exact proof term for the current goal is He2fun.
Let y be given.
Apply (xm (y = lastval)) to the current goal.
We use m1 to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hm1InN.
rewrite the current goal using HyEq (from left to right).
An exact proof term for the current goal is He2m1.
Let x' be given.
We prove the intermediate
claim Hx'nS:
x' ∈ ordsucc m1.
rewrite the current goal using HnDef (from right to left) at position 1.
An exact proof term for the current goal is Hx'n.
We prove the intermediate
claim Hx'Case:
x' ∈ m1 ∨ x' = m1.
An
exact proof term for the current goal is
(ordsuccE m1 x' Hx'nS).
Apply (Hx'Case (x' = m1)) to the current goal.
Apply FalseE to the current goal.
We prove the intermediate
claim Hx'nm1:
¬ (x' = m1).
We prove the intermediate
claim Hmm:
m1 ∈ m1.
rewrite the current goal using Heq (from right to left) at position 1.
An exact proof term for the current goal is Hx'InM1.
An
exact proof term for the current goal is
((In_irref m1) Hmm).
rewrite the current goal using He2Def (from left to right).
rewrite the current goal using He2x' (from right to left) at position 1.
An exact proof term for the current goal is Hx'Eq.
We prove the intermediate
claim He1EqY:
apply_fun e1 x' = y.
rewrite the current goal using
(If_i_0 (x' = m1) lastval (apply_fun e1 x') Hx'nm1) (from right to left) at position 1.
An exact proof term for the current goal is Hx'EqIf.
We prove the intermediate
claim He1EqLast:
apply_fun e1 x' = lastval.
rewrite the current goal using HyEq (from right to left).
An exact proof term for the current goal is He1EqY.
We prove the intermediate
claim Hx'dom:
x' ∈ ordsucc t.
rewrite the current goal using Hm1Def (from right to left) at position 1.
An exact proof term for the current goal is Hx'InM1.
We prove the intermediate
claim HimgDrop:
apply_fun e1 x' ∈ (F1 ∖ {lastval}).
An exact proof term for the current goal is (He1fun0 x' Hx'dom).
We prove the intermediate
claim HimgNot:
apply_fun e1 x' ∉ {lastval}.
We prove the intermediate
claim Hmem:
apply_fun e1 x' ∈ {lastval}.
rewrite the current goal using He1EqLast (from left to right).
An
exact proof term for the current goal is
(SingI lastval).
An exact proof term for the current goal is (HimgNot Hmem).
An exact proof term for the current goal is Hx'EqM1.
We prove the intermediate
claim HyNot:
y ∉ {lastval}.
We prove the intermediate
claim HyEq2:
y = lastval.
An
exact proof term for the current goal is
(SingE lastval y HyMem).
An exact proof term for the current goal is (HyNeq HyEq2).
We prove the intermediate
claim HyDrop:
y ∈ (F1 ∖ {lastval}).
An
exact proof term for the current goal is
(setminusI F1 {lastval} y HyF1 HyNot).
Apply He1uniq to the current goal.
Let x0 be given.
Assume Hx0pack.
We prove the intermediate
claim Hx0Dom:
x0 ∈ ordsucc t.
We prove the intermediate
claim He1x0:
apply_fun e1 x0 = y.
We prove the intermediate
claim HuniqE1:
∀x'' : set, x'' ∈ ordsucc t → apply_fun e1 x'' = y → x'' = x0.
We prove the intermediate
claim Hx0InM1:
x0 ∈ m1.
rewrite the current goal using Hm1Def (from left to right).
An exact proof term for the current goal is Hx0Dom.
We prove the intermediate
claim Hx0InN:
x0 ∈ n.
rewrite the current goal using HnDef (from left to right).
An
exact proof term for the current goal is
(ordsuccI1 m1 x0 Hx0InM1).
We prove the intermediate
claim Hx0nm1:
¬ (x0 = m1).
We prove the intermediate
claim Hmm:
m1 ∈ m1.
rewrite the current goal using Heq (from right to left) at position 1.
An exact proof term for the current goal is Hx0InM1.
An
exact proof term for the current goal is
((In_irref m1) Hmm).
We use x0 to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hx0InN.
rewrite the current goal using He2Def (from left to right).
rewrite the current goal using He2x0 (from left to right).
rewrite the current goal using
(If_i_0 (x0 = m1) lastval (apply_fun e1 x0) Hx0nm1) (from left to right).
An exact proof term for the current goal is He1x0.
Let x' be given.
We prove the intermediate
claim Hx'nS:
x' ∈ ordsucc m1.
rewrite the current goal using HnDef (from right to left) at position 1.
An exact proof term for the current goal is Hx'n.
We prove the intermediate
claim Hx'Case:
x' ∈ m1 ∨ x' = m1.
An
exact proof term for the current goal is
(ordsuccE m1 x' Hx'nS).
Apply (Hx'Case (x' = x0)) to the current goal.
We prove the intermediate
claim Hx'nm1:
¬ (x' = m1).
We prove the intermediate
claim Hmm:
m1 ∈ m1.
rewrite the current goal using Heq (from right to left) at position 1.
An exact proof term for the current goal is Hx'InM1.
An
exact proof term for the current goal is
((In_irref m1) Hmm).
rewrite the current goal using He2Def (from left to right).
rewrite the current goal using He2x_x' (from right to left) at position 1.
An exact proof term for the current goal is Hx'Eq.
We prove the intermediate
claim He1EqY:
apply_fun e1 x' = y.
rewrite the current goal using
(If_i_0 (x' = m1) lastval (apply_fun e1 x') Hx'nm1) (from right to left) at position 1.
An exact proof term for the current goal is Hx'EqIf.
We prove the intermediate
claim Hx'dom:
x' ∈ ordsucc t.
rewrite the current goal using Hm1Def (from right to left) at position 1.
An exact proof term for the current goal is Hx'InM1.
An exact proof term for the current goal is (HuniqE1 x' Hx'dom He1EqY).
Apply FalseE to the current goal.
rewrite the current goal using He2Def (from left to right).
rewrite the current goal using He2x_m1 (from right to left) at position 1.
An exact proof term for the current goal is Hx'Eq.
We prove the intermediate
claim HyEq2:
y = lastval.
We prove the intermediate
claim Htmp:
lastval = y.
rewrite the current goal using
(If_i_1 (x' = m1) lastval (apply_fun e1 x') Hx'EqM1) (from right to left) at position 1.
An exact proof term for the current goal is Hx'EqIf_m1.
Use symmetry.
An exact proof term for the current goal is Htmp.
An exact proof term for the current goal is (HyNeq HyEq2).
We prove the intermediate
claim Hws_m1_e2e1:
weighted_sum x m1 e2 = weighted_sum x m1 e1.
Apply (weighted_sum_congr x m1 e2 e1 Hm1Nat) to the current goal.
Let k be given.
We prove the intermediate
claim HkInN:
k ∈ n.
rewrite the current goal using HnDef (from left to right).
An
exact proof term for the current goal is
(ordsuccI1 m1 k HkIn).
rewrite the current goal using He2Def (from left to right).
We prove the intermediate
claim Hkne:
¬ (k = m1).
We prove the intermediate
claim Hmm:
m1 ∈ m1.
rewrite the current goal using Heq (from right to left) at position 1.
An exact proof term for the current goal is HkIn.
An
exact proof term for the current goal is
((In_irref m1) Hmm).
rewrite the current goal using He2k (from left to right).
rewrite the current goal using
(If_i_0 (k = m1) lastval (apply_fun e1 k) Hkne) (from left to right).
Use reflexivity.
We prove the intermediate
claim Hws_m1_e0e2:
weighted_sum x m1 e0 = weighted_sum x m1 e2.
rewrite the current goal using HwsSmall (from left to right).
rewrite the current goal using Hws_m1_e2e1 (from right to left) at position 1.
Use reflexivity.
We prove the intermediate
claim Hws_e0_e2:
weighted_sum x n e0 = weighted_sum x n e2.
rewrite the current goal using HnDef (from left to right).
We prove the intermediate
claim Hws0:
weighted_sum x (ordsucc m1) e0 = weighted_step x e0 m1 (weighted_sum x m1 e0).
An exact proof term for the current goal is (weighted_sum_S x e0 m1 Hm1Nat).
We prove the intermediate
claim Hws2:
weighted_sum x (ordsucc m1) e2 = weighted_step x e2 m1 (weighted_sum x m1 e2).
An exact proof term for the current goal is (weighted_sum_S x e2 m1 Hm1Nat).
rewrite the current goal using Hws0 (from left to right).
rewrite the current goal using Hws2 (from left to right).
We prove the intermediate
claim Hacc:
weighted_sum x m1 e0 = weighted_sum x m1 e2.
An exact proof term for the current goal is Hws_m1_e0e2.
We prove the intermediate
claim HstepAcc:
weighted_step x e0 m1 (weighted_sum x m1 e0) = weighted_step x e0 m1 (weighted_sum x m1 e2).
An exact proof term for the current goal is (weighted_step_congr_acc x e0 m1 (weighted_sum x m1 e0) (weighted_sum x m1 e2) Hacc).
rewrite the current goal using HstepAcc (from left to right).
rewrite the current goal using He2m1 (from left to right).
rewrite the current goal using HlastvalDef (from right to left) at position 1.
Use reflexivity.
An exact proof term for the current goal is (weighted_step_congr_e_at x e0 e2 m1 (weighted_sum x m1 e2) Hem).
We prove the intermediate
claim He2kP:
∀k : set, k ∈ n → apply_fun e2 k ∈ P.
Let k be given.
We prove the intermediate
claim HkF1:
apply_fun e2 k ∈ F1.
An exact proof term for the current goal is (He2fun k Hk).
An
exact proof term for the current goal is
(HF1subP (apply_fun e2 k) HkF1).
Let k be given.
We prove the intermediate
claim HkF1:
apply_fun e2 k ∈ F1.
An exact proof term for the current goal is (He2fun k Hk).
An
exact proof term for the current goal is
(HcoefR1 (apply_fun e2 k) HkF1).
Let k be given.
We prove the intermediate
claim HkF1:
apply_fun e2 k ∈ F1.
An exact proof term for the current goal is (He2fun k Hk).
An
exact proof term for the current goal is
(HvalR1 (apply_fun e2 k) HkF1).
We use e' to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
We prove the intermediate
claim Hswap:
weighted_sum x n e' = weighted_sum x n e2.
An exact proof term for the current goal is (weighted_sum_swap_adjacent_real x e2 n t HxX HnO HtInN Hm1InN He2kP He2coefR He2valR).
We prove the intermediate
claim HswapInv:
weighted_sum x n e2 = weighted_sum x n e'.
rewrite the current goal using Hswap (from right to left).
Use reflexivity.
An
exact proof term for the current goal is
(eq_i_tra (weighted_sum x n e0) (weighted_sum x n e2) (weighted_sum x n e') Hws_e0_e2 HswapInv).
rewrite the current goal using He'Def (from left to right).
We prove the intermediate
claim HstInN:
ordsucc t ∈ n.
rewrite the current goal using Hm1Def (from right to left) at position 1.
An exact proof term for the current goal is Hm1InN.
rewrite the current goal using Hm1Def (from left to right) at position 1.
rewrite the current goal using Hsa (from left to right).
We prove the intermediate
claim Hneq:
¬ (ordsucc t = t).
We prove the intermediate
claim Htt:
t ∈ t.
rewrite the current goal using Heq (from right to left) at position 2.
An
exact proof term for the current goal is
(ordsuccI2 t).
An
exact proof term for the current goal is
((In_irref t) Htt).
An exact proof term for the current goal is He2t.
We prove the intermediate claim HmP: Pm m.
An
exact proof term for the current goal is
(nat_ind Pm HP0 HPS m HmNat).
An exact proof term for the current goal is (HmP F0 e flast HmO HF0subP HvalR0 HcoefR0 Hbij HflastF0).
Let x, m, F, e and f be given.
An exact proof term for the current goal is (weighted_sum_bijection_move_value_to_last_real x m F e f HxX HmO HFsubP HvalR HcoefR Hbij HfF).
Apply Hmove to the current goal.
Let e2 be given.
Assume He2pack.
We prove the intermediate
claim HwsEq:
weighted_sum x (ordsucc m) e = weighted_sum x (ordsucc m) e2.
We prove the intermediate
claim He2m:
apply_fun e2 m = f.
rewrite the current goal using He2m (from left to right).
An exact proof term for the current goal is Hfx0.
We prove the intermediate
claim Hdrop:
weighted_sum x (ordsucc m) e2 = weighted_sum x m e2.
An exact proof term for the current goal is (weighted_sum_drop_last_of_bijection_zero_real x m F e2 HxX HmO HFsubP HvalR HcoefR Hbij2 Hval0last).
We prove the intermediate
claim HbijDrop:
bijection m (F ∖ {f}) e2.
rewrite the current goal using He2m (from right to left).
An exact proof term for the current goal is HbijDrop0.
We use e2 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HbijDrop.
rewrite the current goal using HwsEq (from left to right).
An exact proof term for the current goal is Hdrop.
We prove the intermediate
claim weighted_sum_bijection_indep_real:
∀x n F e1 e2 : set, x ∈ X → n ∈ ω → F ⊆ P → (∀f : set, f ∈ F → apply_fun f x ∈ R) → (∀f : set, f ∈ F → apply_fun coef_of f ∈ R) → bijection n F e1 → bijection n F e2 → weighted_sum x n e1 = weighted_sum x n e2.
Let x, n, F, e1 and e2 be given.
We prove the intermediate
claim HnNat:
nat_p n.
An
exact proof term for the current goal is
(omega_nat_p n HnO).
Set Pws to be the term
λt : set ⇒ ∀F0 eA eB : set, F0 ⊆ P → (∀f : set, f ∈ F0 → apply_fun f x ∈ R) → (∀f : set, f ∈ F0 → apply_fun coef_of f ∈ R) → bijection t F0 eA → bijection t F0 eB → weighted_sum x t eA = weighted_sum x t eB.
We prove the intermediate
claim HP0:
Pws 0.
Let F0, eA and eB be given.
rewrite the current goal using (weighted_sum_0 x eA) (from left to right).
rewrite the current goal using (weighted_sum_0 x eB) (from left to right).
Use reflexivity.
We prove the intermediate
claim HPS:
∀m : set, nat_p m → Pws m → Pws (ordsucc m).
Let m be given.
Assume IHm: Pws m.
Let F0, eA and eB be given.
We prove the intermediate
claim HmO:
m ∈ ω.
An
exact proof term for the current goal is
(nat_p_omega m HmNat).
We prove the intermediate
claim HflastDef:
flast = apply_fun eA m.
We prove the intermediate
claim HflastF0:
flast ∈ F0.
An
exact proof term for the current goal is
(HeAfun m (ordsuccI2 m)).
An exact proof term for the current goal is (weighted_sum_bijection_move_value_to_last_real x m F0 eB flast HxX HmO HF0subP HvalR0 HcoefR0 HbijB HflastF0).
Apply Hmove to the current goal.
Let eB' be given.
Assume HB'pack.
We prove the intermediate
claim HwsBB':
weighted_sum x (ordsucc m) eB = weighted_sum x (ordsucc m) eB'.
We prove the intermediate
claim HlastEq:
apply_fun eB' m = flast.
We prove the intermediate
claim HsubP':
(F0 ∖ {flast}) ⊆ P.
We prove the intermediate
claim HvalR':
∀f : set, f ∈ (F0 ∖ {flast}) → apply_fun f x ∈ R.
Let f be given.
An
exact proof term for the current goal is
(HvalR0 f (setminusE1 F0 {flast} f Hf)).
We prove the intermediate
claim HcoefR':
∀f : set, f ∈ (F0 ∖ {flast}) → apply_fun coef_of f ∈ R.
Let f be given.
An
exact proof term for the current goal is
(HcoefR0 f (setminusE1 F0 {flast} f Hf)).
We prove the intermediate
claim HbijA0:
bijection m (F0 ∖ {flast}) eA.
rewrite the current goal using HflastDef (from left to right).
We prove the intermediate
claim HbijB0:
bijection m (F0 ∖ {flast}) eB'.
rewrite the current goal using HlastEq (from right to left).
We prove the intermediate
claim HaccEq:
weighted_sum x m eA = weighted_sum x m eB'.
An
exact proof term for the current goal is
(IHm (F0 ∖ {flast}) eA eB' HsubP' HvalR' HcoefR' HbijA0 HbijB0).
We prove the intermediate
claim HgoalB':
weighted_sum x (ordsucc m) eA = weighted_sum x (ordsucc m) eB'.
We prove the intermediate
claim HwsA:
weighted_sum x (ordsucc m) eA = weighted_step x eA m (weighted_sum x m eA).
An exact proof term for the current goal is (weighted_sum_S x eA m HmNat).
We prove the intermediate
claim HwsB:
weighted_sum x (ordsucc m) eB' = weighted_step x eB' m (weighted_sum x m eB').
An exact proof term for the current goal is (weighted_sum_S x eB' m HmNat).
rewrite the current goal using HwsA (from left to right).
rewrite the current goal using HwsB (from left to right).
rewrite the current goal using HflastDef (from right to left) at position 1.
rewrite the current goal using HlastEq (from left to right).
Use reflexivity.
We prove the intermediate
claim HstepAcc:
weighted_step x eA m (weighted_sum x m eA) = weighted_step x eA m (weighted_sum x m eB').
An exact proof term for the current goal is (weighted_step_congr_acc x eA m (weighted_sum x m eA) (weighted_sum x m eB') HaccEq).
We prove the intermediate
claim HstepE:
weighted_step x eA m (weighted_sum x m eB') = weighted_step x eB' m (weighted_sum x m eB').
An exact proof term for the current goal is (weighted_step_congr_e_at x eA eB' m (weighted_sum x m eB') HeqEm).
rewrite the current goal using HstepAcc (from left to right).
rewrite the current goal using HstepE (from left to right).
Use reflexivity.
We prove the intermediate
claim Hsubst:
∀S T : set, S = T → weighted_sum x (ordsucc m) eA = T → weighted_sum x (ordsucc m) eA = S.
Let S and T be given.
We will
prove weighted_sum x (ordsucc m) eA = S.
rewrite the current goal using HeqST (from left to right).
An exact proof term for the current goal is HT.
An
exact proof term for the current goal is
(Hsubst (weighted_sum x (ordsucc m) eB) (weighted_sum x (ordsucc m) eB') HwsBB' HgoalB').
We prove the intermediate claim HnP: Pws n.
An
exact proof term for the current goal is
(nat_ind Pws HP0 HPS n HnNat).
An exact proof term for the current goal is (HnP F e1 e2 HFsubP HvalR_F HcoefR_F Hbij1 Hbij2).
Let A, x, F, n, e and p be given.
We prove the intermediate
claim HepsA:
epsA ∈ R ∧ Rlt 0 epsA.
An exact proof term for the current goal is (Heps A HA).
We prove the intermediate
claim HepsAR:
epsA ∈ R.
An
exact proof term for the current goal is
(andEL (epsA ∈ R) (Rlt 0 epsA) HepsA).
We prove the intermediate
claim HepsAS:
SNo epsA.
An
exact proof term for the current goal is
(real_SNo epsA HepsAR).
We prove the intermediate
claim HeFun:
function_on e n F.
We prove the intermediate
claim HekF:
∀k : set, k ∈ n → apply_fun e k ∈ F.
Let k be given.
An exact proof term for the current goal is (HeFun k Hk).
We prove the intermediate
claim HekP:
∀k : set, k ∈ n → apply_fun e k ∈ P.
Let k be given.
An
exact proof term for the current goal is
(HFsubP (apply_fun e k) (HekF k Hk)).
Let k be given.
An
exact proof term for the current goal is
(HPval_in_R (apply_fun e k) x (HekP k Hk) HxX).
Let k be given.
An
exact proof term for the current goal is
(HPval_nonneg (apply_fun e k) x (HekP k Hk) HxX).
We prove the intermediate
claim HcoefR:
∀f : set, f ∈ P → apply_fun coef_of f ∈ R.
Let k be given.
Apply (xm (vk = 0)) to the current goal.
We prove the intermediate
claim HfkP:
fk ∈ P.
An exact proof term for the current goal is (HekP k Hk).
We prove the intermediate
claim HcoefS:
SNo (apply_fun coef_of fk).
An
exact proof term for the current goal is
(real_SNo (apply_fun coef_of fk) (HcoefR fk HfkP)).
We prove the intermediate
claim HvkR:
vk ∈ R.
An exact proof term for the current goal is (HvalR k Hk).
rewrite the current goal using Hv0 (from left to right).
rewrite the current goal using
(mul_SNo_zeroR epsA HepsAS) (from left to right).
We prove the intermediate
claim HfkP:
fk ∈ P.
An exact proof term for the current goal is (HekP k Hk).
We prove the intermediate
claim HvNe:
apply_fun fk x ≠ 0.
An exact proof term for the current goal is HvNe0.
We prove the intermediate
claim HcoefLe:
Rle (apply_fun coef_of fk) epsA.
An exact proof term for the current goal is (Hcoef_le_on_point fk A x HfkP HA HxX HxA HvNe).
We prove the intermediate
claim HvkNN:
Rle 0 vk.
An exact proof term for the current goal is (HvalNN k Hk).
We prove the intermediate
claim HcoefLeS:
apply_fun coef_of fk ≤ epsA.
We prove the intermediate
claim HvkNNS:
0 ≤ vk.
An
exact proof term for the current goal is
(SNoLe_of_Rle 0 vk HvkNN).
We prove the intermediate
claim HcoefS:
SNo (apply_fun coef_of fk).
An
exact proof term for the current goal is
(real_SNo (apply_fun coef_of fk) (HcoefR fk HfkP)).
We prove the intermediate
claim HvkS:
SNo vk.
An
exact proof term for the current goal is
(real_SNo vk (HvalR k Hk)).
An
exact proof term for the current goal is
(nonneg_mul_SNo_Le vk (apply_fun coef_of fk) epsA HvkS HvkNNS HcoefS HepsAS HcoefLeS).
An
exact proof term for the current goal is
(mul_SNo_com epsA vk HepsAS HvkS).
rewrite the current goal using Hcomm1 (from left to right).
rewrite the current goal using Hcomm2 (from left to right).
We prove the intermediate
claim Hmain:
Rle (weighted_sum x n e) (mul_SNo epsA (apply_fun p n)).
We prove the intermediate
claim HnNat:
nat_p n.
An
exact proof term for the current goal is
(omega_nat_p n HnO).
We prove the intermediate
claim Hind:
∀m : set, nat_p m → Pbound m.
rewrite the current goal using (weighted_sum_0 x e) (from left to right).
We prove the intermediate
claim H0E:
0 = Empty.
rewrite the current goal using H0E (from left to right).
rewrite the current goal using Hp0 (from left to right).
rewrite the current goal using
(mul_SNo_zeroR epsA HepsAS) (from left to right).
Let m be given.
Assume IHm: Pbound m.
We prove the intermediate
claim HnNat2:
nat_p n.
An
exact proof term for the current goal is
(omega_nat_p n HnO).
We prove the intermediate
claim HnOrd:
ordinal n.
An
exact proof term for the current goal is
(nat_p_ordinal n HnNat2).
We prove the intermediate
claim HnTS:
TransSet n.
An
exact proof term for the current goal is
(HsuccTS (ordsucc m) HSmIn).
We prove the intermediate
claim HmInSuccN:
m ∈ ordsucc n.
An
exact proof term for the current goal is
(HsubSm m (ordsuccI2 m)).
We prove the intermediate
claim HmCase:
m ∈ n ∨ m = n.
An
exact proof term for the current goal is
(ordsuccE n m HmInSuccN).
An exact proof term for the current goal is (IHm HmInSuccN).
An exact proof term for the current goal is (HtermLe m HmInN).
We prove the intermediate
claim HwsEq:
weighted_sum x (ordsucc m) e = weighted_step x e m (weighted_sum x m e).
An exact proof term for the current goal is (weighted_sum_S x e m HmNat).
rewrite the current goal using HwsEq (from left to right).
rewrite the current goal using HstepDef (from left to right).
rewrite the current goal using (HpStep m HmInN) (from left to right).
Set rhs2 to be the term
mul_SNo epsA vm.
Set rhs1 to be the term
mul_SNo epsA pm.
We prove the intermediate
claim HwsR:
weighted_sum x m e ∈ R.
An
exact proof term for the current goal is
(RleE_left (weighted_sum x m e) (mul_SNo epsA pm) HI).
We prove the intermediate
claim Hrhs1R:
rhs1 ∈ R.
An
exact proof term for the current goal is
(RleE_right (weighted_sum x m e) (mul_SNo epsA pm) HI).
We prove the intermediate
claim HtermR:
term ∈ R.
An
exact proof term for the current goal is
(RleE_left term rhs2 Hterm).
We prove the intermediate
claim Hrhs2R:
rhs2 ∈ R.
An
exact proof term for the current goal is
(RleE_right term rhs2 Hterm).
We prove the intermediate
claim HpmR:
pm ∈ R.
An exact proof term for the current goal is (HpFun m HmInSuccN).
We prove the intermediate
claim HvmR:
vm ∈ R.
An exact proof term for the current goal is (HvalR m HmInN).
We prove the intermediate
claim HpmS:
SNo pm.
An
exact proof term for the current goal is
(real_SNo pm HpmR).
We prove the intermediate
claim HvmS:
SNo vm.
An
exact proof term for the current goal is
(real_SNo vm HvmR).
An
exact proof term for the current goal is
(mul_SNo_distrL epsA pm vm HepsAS HpmS HvmS).
rewrite the current goal using Hdist (from left to right).
We prove the intermediate
claim Hstep2:
Rle (add_SNo (weighted_sum x m e) term) (add_SNo (weighted_sum x m e) rhs2).
An
exact proof term for the current goal is
(Rle_add_SNo_2 (weighted_sum x m e) term rhs2 HwsR HtermR Hrhs2R Hterm).
We prove the intermediate
claim Hstep1:
Rle (add_SNo (weighted_sum x m e) rhs2) (add_SNo rhs1 rhs2).
An
exact proof term for the current goal is
(Rle_add_SNo_1 (weighted_sum x m e) rhs1 rhs2 HwsR Hrhs1R Hrhs2R HI).
An
exact proof term for the current goal is
(Rle_tra (add_SNo (weighted_sum x m e) term) (add_SNo (weighted_sum x m e) rhs2) (add_SNo rhs1 rhs2) Hstep2 Hstep1).
We prove the intermediate
claim HnNat3:
nat_p n.
An
exact proof term for the current goal is
(omega_nat_p n HnO).
We prove the intermediate
claim HnotInSelf:
∀k : set, nat_p k → ¬ (k ∈ k).
Let k be given.
Set Q to be the term
λt : set ⇒ ¬ (t ∈ t).
We prove the intermediate
claim HQ0:
Q 0.
An
exact proof term for the current goal is
(EmptyE 0 H0In).
We prove the intermediate
claim HQS:
∀t : set, nat_p t → Q t → Q (ordsucc t).
Let t be given.
Apply (Hcase False) to the current goal.
We prove the intermediate
claim HtOrd:
ordinal t.
An
exact proof term for the current goal is
(nat_p_ordinal t HtNat).
We prove the intermediate
claim HtTS:
TransSet t.
We prove the intermediate
claim Hsub:
ordsucc t ⊆ t.
An
exact proof term for the current goal is
(HtTS (ordsucc t) HInT).
An
exact proof term for the current goal is
(IHt (Hsub t (ordsuccI2 t))).
We prove the intermediate
claim Htt:
t ∈ t.
rewrite the current goal using Heq (from right to left) at position 2.
An
exact proof term for the current goal is
(ordsuccI2 t).
An exact proof term for the current goal is (IHt Htt).
An
exact proof term for the current goal is
(nat_ind Q HQ0 HQS k HkNat).
We prove the intermediate
claim HnNotIn:
¬ (n ∈ n).
An exact proof term for the current goal is (HnotInSelf n HnNat3).
rewrite the current goal using HmEqN (from right to left) at position 1.
An exact proof term for the current goal is HSmIn.
An
exact proof term for the current goal is
(ordsuccE n (ordsucc n) HsuccInSucc).
We prove the intermediate
claim HnInN:
n ∈ n.
Apply (HcaseN (n ∈ n)) to the current goal.
We prove the intermediate
claim HnOrd:
ordinal n.
An
exact proof term for the current goal is
(nat_p_ordinal n HnNat3).
We prove the intermediate
claim HnTS2:
TransSet n.
We prove the intermediate
claim Hsub:
ordsucc n ⊆ n.
An
exact proof term for the current goal is
(HnTS2 (ordsucc n) HsuccIn).
An
exact proof term for the current goal is
(Hsub n (ordsuccI2 n)).
rewrite the current goal using Heq (from right to left) at position 2.
An
exact proof term for the current goal is
(ordsuccI2 n).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HnNotIn HnInN).
We prove the intermediate
claim HnIn:
n ∈ ordsucc n.
An
exact proof term for the current goal is
(ordsuccI2 n).
An exact proof term for the current goal is (Hind n HnNat HnIn).
rewrite the current goal using Hpn1 (from left to right).
An
exact proof term for the current goal is
(mul_SNo_oneR epsA HepsAS).
rewrite the current goal using HrhsEq (from right to left).
An exact proof term for the current goal is Hmain.
We prove the intermediate
claim weighted_sum_bijection_zero_outside_real:
∀x n0 F0 e0 n F e : set, x ∈ X → n0 ∈ ω → finite F → F0 ⊆ F → F ⊆ P → F0 ⊆ P → (∀f : set, f ∈ F0 → apply_fun f x ∈ R) → (∀f : set, f ∈ F0 → apply_fun coef_of f ∈ R) → (∀f : set, f ∈ F → ¬ (f ∈ F0) → apply_fun f x = 0) → bijection n0 F0 e0 → n ∈ ω → bijection n F e → weighted_sum x n0 e0 = weighted_sum x n e.
Let x, n0, F0, e0, n, F and e be given.
Set D to be the term
F ∖ F0.
We prove the intermediate
claim HDsubF:
D ⊆ F.
An
exact proof term for the current goal is
(setminus_Subq F F0).
We prove the intermediate
claim HDfin:
finite D.
An
exact proof term for the current goal is
(Subq_finite F HFfin D HDsubF).
We prove the intermediate
claim HDsubP:
D ⊆ P.
An
exact proof term for the current goal is
(Subq_tra D F P HDsubF HFsubP).
We prove the intermediate
claim HDnotF0:
∀f : set, f ∈ D → ¬ (f ∈ F0).
Let f be given.
An
exact proof term for the current goal is
(setminusE2 F F0 f HfD).
We prove the intermediate
claim HzeroD:
∀f : set, f ∈ D → apply_fun f x = 0.
Let f be given.
We prove the intermediate
claim HfF:
f ∈ F.
An
exact proof term for the current goal is
(setminusE1 F F0 f HfD).
An exact proof term for the current goal is (HzeroOut f HfF (HDnotF0 f HfD)).
We prove the intermediate
claim HeqFD:
F = F0 ∪ D.
Let u be given.
Apply (xm (u ∈ F0)) to the current goal.
An
exact proof term for the current goal is
(binunionI1 F0 D u HuF0).
We prove the intermediate
claim HuD:
u ∈ D.
An
exact proof term for the current goal is
(setminusI F F0 u HuF HnotF0).
An
exact proof term for the current goal is
(binunionI2 F0 D u HuD).
Let u be given.
Apply (binunionE F0 D u HuU) to the current goal.
An exact proof term for the current goal is (HF0subF u HuF0).
An exact proof term for the current goal is (HDsubF u HuD).
We prove the intermediate
claim HbijU:
bijection n (F0 ∪ D) e.
rewrite the current goal using HeqFD (from right to left).
An exact proof term for the current goal is Hbij.
Set Pdrop to be the term
λT : set ⇒ ∀nT eT : set, T ⊆ P → (∀f : set, f ∈ T → ¬ (f ∈ F0)) → (∀f : set, f ∈ T → apply_fun f x = 0) → nT ∈ ω → bijection nT (F0 ∪ T) eT → weighted_sum x n0 e0 = weighted_sum x nT eT.
We prove the intermediate
claim HP0:
Pdrop Empty.
Let nT and eT be given.
We prove the intermediate
claim HeqU:
(F0 ∪ Empty) = F0.
Let u be given.
An exact proof term for the current goal is HuF0.
Apply FalseE to the current goal.
An
exact proof term for the current goal is
(EmptyE u HuE).
We prove the intermediate
claim HbijF0:
bijection nT F0 eT.
rewrite the current goal using HeqU (from right to left).
An exact proof term for the current goal is HbijT.
We prove the intermediate
claim Heq_n0F0:
equip n0 F0.
We prove the intermediate
claim Heq_nTF0:
equip nT F0.
We prove the intermediate
claim Heq_n0nT:
equip n0 nT.
An
exact proof term for the current goal is
(equip_tra n0 F0 nT Heq_n0F0 (equip_sym nT F0 Heq_nTF0)).
We prove the intermediate
claim Hn0Eq:
n0 = nT.
An
exact proof term for the current goal is
(equip_omega_eq n0 nT Hn0O HnTO Heq_n0nT).
We prove the intermediate
claim HbijF0n0:
bijection n0 F0 eT.
rewrite the current goal using Hn0Eq (from left to right).
An exact proof term for the current goal is HbijF0.
rewrite the current goal using Hn0Eq (from right to left).
An exact proof term for the current goal is (weighted_sum_bijection_indep_real x n0 F0 e0 eT HxX Hn0O HF0subP HvalR0 HcoefR0 Hbij0 HbijF0n0).
We prove the intermediate
claim HPS:
∀T y : set, finite T → y ∉ T → Pdrop T → Pdrop (T ∪ {y}).
Let T and y be given.
Assume IH: Pdrop T.
We will
prove Pdrop (T ∪ {y}).
Let nT and eT be given.
We prove the intermediate
claim HyP:
y ∈ P.
An
exact proof term for the current goal is
(HsubP y (binunionI2 T {y} y (SingI y))).
We prove the intermediate
claim HyNotF0:
¬ (y ∈ F0).
An
exact proof term for the current goal is
(HnotF0Ty y (binunionI2 T {y} y (SingI y))).
We prove the intermediate
claim Hy0:
apply_fun y x = 0.
An
exact proof term for the current goal is
(HzeroTy y (binunionI2 T {y} y (SingI y))).
We prove the intermediate
claim HnTnat:
nat_p nT.
An
exact proof term for the current goal is
(omega_nat_p nT HnTO).
An
exact proof term for the current goal is
(nat_inv nT HnTnat).
Apply (Hcase (weighted_sum x n0 e0 = weighted_sum x nT eT)) to the current goal.
Apply FalseE to the current goal.
We prove the intermediate
claim HyInCod:
y ∈ (F0 ∪ (T ∪ {y})).
We prove the intermediate
claim Hbij0Ty:
bijection 0 (F0 ∪ (T ∪ {y})) eT.
rewrite the current goal using Hn0 (from right to left).
An exact proof term for the current goal is HbijTy.
We prove the intermediate
claim Hexk:
∃k : set, k ∈ 0 ∧ apply_fun eT k = y.
An
exact proof term for the current goal is
(bijection_surj 0 (F0 ∪ (T ∪ {y})) eT y Hbij0Ty HyInCod).
Apply Hexk to the current goal.
Let k be given.
Assume Hkpair.
We prove the intermediate
claim Hk0:
k ∈ 0.
An
exact proof term for the current goal is
(andEL (k ∈ 0) (apply_fun eT k = y) Hkpair).
An
exact proof term for the current goal is
(EmptyE k Hk0).
Apply Hexm to the current goal.
Let m be given.
We prove the intermediate
claim HmNat:
nat_p m.
We prove the intermediate
claim HnTEq:
nT = ordsucc m.
We prove the intermediate
claim HmO:
m ∈ ω.
An
exact proof term for the current goal is
(nat_p_omega m HmNat).
We prove the intermediate
claim HFsubP_all:
(F0 ∪ (T ∪ {y})) ⊆ P.
Let u be given.
An exact proof term for the current goal is (HF0subP u HuF0).
An exact proof term for the current goal is (HsubP u HuT).
We prove the intermediate
claim HvalR_all:
∀g : set, g ∈ (F0 ∪ (T ∪ {y})) → apply_fun g x ∈ R.
Let g be given.
We prove the intermediate
claim HgP:
g ∈ P.
An exact proof term for the current goal is (HFsubP_all g HgU).
An exact proof term for the current goal is (HPval_in_R g x HgP HxX).
We prove the intermediate
claim HcoefR_all:
∀g : set, g ∈ (F0 ∪ (T ∪ {y})) → apply_fun coef_of g ∈ R.
Let g be given.
We prove the intermediate
claim HgP:
g ∈ P.
An exact proof term for the current goal is (HFsubP_all g HgU).
We prove the intermediate
claim Hpos:
Rlt 0 (apply_fun coef_of g).
An exact proof term for the current goal is (Hcoef_pos g HgP).
rewrite the current goal using HnTEq (from right to left).
An exact proof term for the current goal is HbijTy.
We prove the intermediate
claim HyInU:
y ∈ (F0 ∪ (T ∪ {y})).
We prove the intermediate
claim Hrem:
∃e' : set, bijection m ((F0 ∪ (T ∪ {y})) ∖ {y}) e' ∧ weighted_sum x (ordsucc m) eT = weighted_sum x m e'.
An
exact proof term for the current goal is
(weighted_sum_bijection_remove_one_zero_real x m (F0 ∪ (T ∪ {y})) eT y HxX HmO HFsubP_all HvalR_all HcoefR_all HbijS HyInU Hy0).
Apply Hrem to the current goal.
Let e' be given.
Assume He'pack.
We prove the intermediate
claim HbijE':
bijection m ((F0 ∪ (T ∪ {y})) ∖ {y}) e'.
An
exact proof term for the current goal is
(andEL (bijection m ((F0 ∪ (T ∪ {y})) ∖ {y}) e') (weighted_sum x (ordsucc m) eT = weighted_sum x m e') He'pack).
We prove the intermediate
claim HwsEq:
weighted_sum x (ordsucc m) eT = weighted_sum x m e'.
An
exact proof term for the current goal is
(andER (bijection m ((F0 ∪ (T ∪ {y})) ∖ {y}) e') (weighted_sum x (ordsucc m) eT = weighted_sum x m e') He'pack).
We prove the intermediate
claim HeqRem:
((F0 ∪ (T ∪ {y})) ∖ {y}) = (F0 ∪ T).
Let u be given.
We prove the intermediate
claim HuPair:
u ∈ (F0 ∪ (T ∪ {y})) ∧ u ∉ {y}.
An
exact proof term for the current goal is
(setminusE (F0 ∪ (T ∪ {y})) {y} u Hu).
We prove the intermediate
claim HuIn:
u ∈ (F0 ∪ (T ∪ {y})).
An
exact proof term for the current goal is
(andEL (u ∈ (F0 ∪ (T ∪ {y}))) (u ∉ {y}) HuPair).
We prove the intermediate
claim HuNotY:
u ∉ {y}.
An
exact proof term for the current goal is
(andER (u ∈ (F0 ∪ (T ∪ {y}))) (u ∉ {y}) HuPair).
An
exact proof term for the current goal is
(binunionI1 F0 T u HuF0).
An
exact proof term for the current goal is
(binunionI2 F0 T u HuT0).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HuNotY HuY).
Let u be given.
We will
prove u ∈ ((F0 ∪ (T ∪ {y})) ∖ {y}).
We prove the intermediate
claim HuIn:
u ∈ (F0 ∪ (T ∪ {y})).
Apply (binunionE F0 T u Hu) to the current goal.
An
exact proof term for the current goal is
(binunionI1 F0 (T ∪ {y}) u HuF0).
We prove the intermediate
claim HuNotY:
u ∉ {y}.
We prove the intermediate
claim HuEq:
u = y.
An
exact proof term for the current goal is
(SingE y u HuY).
We prove the intermediate
claim HyU:
y ∈ (F0 ∪ T).
rewrite the current goal using HuEq (from right to left).
An exact proof term for the current goal is Hu.
Apply (binunionE F0 T y HyU) to the current goal.
Apply HyNotF0 to the current goal.
An exact proof term for the current goal is HyF0.
Apply HyNot to the current goal.
An exact proof term for the current goal is HyT.
An
exact proof term for the current goal is
(setminusI (F0 ∪ (T ∪ {y})) {y} u HuIn HuNotY).
We prove the intermediate
claim HbijSmall:
bijection m (F0 ∪ T) e'.
rewrite the current goal using HeqRem (from right to left).
An exact proof term for the current goal is HbijE'.
We prove the intermediate
claim HTsubP:
T ⊆ P.
Let u be given.
We prove the intermediate
claim HuTU:
u ∈ (T ∪ {y}).
An
exact proof term for the current goal is
(binunionI1 T {y} u HuT).
An exact proof term for the current goal is (HsubP u HuTU).
We prove the intermediate
claim HTnotF0:
∀f : set, f ∈ T → ¬ (f ∈ F0).
Let f be given.
We prove the intermediate
claim HfTU:
f ∈ (T ∪ {y}).
An
exact proof term for the current goal is
(binunionI1 T {y} f HfT).
An exact proof term for the current goal is (HnotF0Ty f HfTU).
We prove the intermediate
claim HzeroT:
∀f : set, f ∈ T → apply_fun f x = 0.
Let f be given.
We prove the intermediate
claim HfTU:
f ∈ (T ∪ {y}).
An
exact proof term for the current goal is
(binunionI1 T {y} f HfT).
An exact proof term for the current goal is (HzeroTy f HfTU).
We prove the intermediate
claim Hrec:
weighted_sum x n0 e0 = weighted_sum x m e'.
An exact proof term for the current goal is (IH m e' HTsubP HTnotF0 HzeroT HmO HbijSmall).
rewrite the current goal using HnTEq (from left to right).
rewrite the current goal using HwsEq (from left to right).
An exact proof term for the current goal is Hrec.
We prove the intermediate claim HdropD: Pdrop D.
An
exact proof term for the current goal is
(finite_ind Pdrop HP0 HPS D HDfin).
An exact proof term for the current goal is (HdropD n e HDsubP HDnotF0 HzeroD HnO HbijU).
Let x, F, n, e and p be given.
We will
prove Rlt 0 (weighted_sum x n e).
We prove the intermediate
claim HnNat:
nat_p n.
An
exact proof term for the current goal is
(omega_nat_p n HnO).
We prove the intermediate
claim HeFun:
function_on e n F.
We prove the intermediate
claim HekF:
∀k : set, k ∈ n → apply_fun e k ∈ F.
Let k be given.
An exact proof term for the current goal is (HeFun k Hk).
We prove the intermediate
claim HekP:
∀k : set, k ∈ n → apply_fun e k ∈ P.
Let k be given.
An
exact proof term for the current goal is
(HFsubP (apply_fun e k) (HekF k Hk)).
Let k be given.
An
exact proof term for the current goal is
(HPval_in_R (apply_fun e k) x (HekP k Hk) HxX).
Let k be given.
An
exact proof term for the current goal is
(HPval_nonneg (apply_fun e k) x (HekP k Hk) HxX).
Apply Hex to the current goal.
Let k0 be given.
We prove the intermediate
claim Hk0In:
k0 ∈ n.
We prove the intermediate
claim Hvk0Ne0:
vk0 ≠ 0.
We prove the intermediate
claim Hvk0R:
vk0 ∈ R.
An exact proof term for the current goal is (HvalR k0 Hk0In).
We prove the intermediate
claim Hvk0NN:
Rle 0 vk0.
An exact proof term for the current goal is (HvalNN k0 Hk0In).
We prove the intermediate
claim Hvk0pos:
Rlt 0 vk0.
We prove the intermediate
claim H0R:
0 ∈ R.
An
exact proof term for the current goal is
real_0.
We prove the intermediate
claim H0S:
SNo 0.
An
exact proof term for the current goal is
SNo_0.
We prove the intermediate
claim Hvk0S:
SNo vk0.
An
exact proof term for the current goal is
(real_SNo vk0 Hvk0R).
We prove the intermediate
claim Hnlt:
¬ (Rlt vk0 0).
An
exact proof term for the current goal is
(RleE_nlt 0 vk0 Hvk0NN).
Apply FalseE to the current goal.
An
exact proof term for the current goal is
(Hnlt (RltI vk0 0 Hvk0R H0R Hvlt0)).
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hvk0Ne0 Hveq0).
An
exact proof term for the current goal is
(RltI 0 vk0 H0R Hvk0R H0ltv).
We prove the intermediate
claim Hfk0P:
fk0 ∈ P.
An exact proof term for the current goal is (HekP k0 Hk0In).
We prove the intermediate
claim HcoefPos:
Rlt 0 (apply_fun coef_of fk0).
An exact proof term for the current goal is (Hcoef_pos fk0 Hfk0P).
We prove the intermediate
claim HcoefR:
apply_fun coef_of fk0 ∈ R.
We prove the intermediate
claim HcoefS:
SNo (apply_fun coef_of fk0).
An
exact proof term for the current goal is
(real_SNo (apply_fun coef_of fk0) HcoefR).
We prove the intermediate
claim Hvk0S2:
SNo vk0.
An
exact proof term for the current goal is
(real_SNo vk0 Hvk0R).
We prove the intermediate
claim HcoefLt0S:
0 < apply_fun coef_of fk0.
An
exact proof term for the current goal is
(RltE_lt 0 (apply_fun coef_of fk0) HcoefPos).
We prove the intermediate
claim Hvk0Lt0S:
0 < vk0.
An
exact proof term for the current goal is
(RltE_lt 0 vk0 Hvk0pos).
An
exact proof term for the current goal is
(mul_SNo_pos_pos (apply_fun coef_of fk0) vk0 HcoefS Hvk0S2 HcoefLt0S Hvk0Lt0S).
We prove the intermediate
claim HtermLe:
Rle (mul_SNo (apply_fun coef_of fk0) vk0) (weighted_sum x n e).
We prove the intermediate
claim HwsRall:
∀m : set, m ∈ ordsucc n → weighted_sum x m e ∈ R.
Set Pws to be the term
λm : set ⇒ m ∈ ordsucc n → weighted_sum x m e ∈ R.
We prove the intermediate
claim Hind:
∀m : set, nat_p m → Pws m.
rewrite the current goal using (weighted_sum_0 x e) (from left to right).
An
exact proof term for the current goal is
real_0.
Let m be given.
Assume IHm: Pws m.
We prove the intermediate
claim HnOrd:
ordinal n.
An
exact proof term for the current goal is
(nat_p_ordinal n HnNat).
We prove the intermediate
claim HnTS:
TransSet n.
We prove the intermediate
claim HmInN:
m ∈ n.
An
exact proof term for the current goal is
(ordsuccE n (ordsucc m) HSmIn).
Apply (HmCase (m ∈ n)) to the current goal.
We prove the intermediate
claim Hsub:
ordsucc m ⊆ n.
An
exact proof term for the current goal is
(HnTS (ordsucc m) HSmInN).
An
exact proof term for the current goal is
(Hsub m (ordsuccI2 m)).
rewrite the current goal using Heq (from right to left).
An
exact proof term for the current goal is
(ordsuccI2 m).
We prove the intermediate
claim HmInSuccN:
m ∈ ordsucc n.
An
exact proof term for the current goal is
((ordsuccI1 n) m HmInN).
We prove the intermediate
claim HaccR:
weighted_sum x m e ∈ R.
An exact proof term for the current goal is (IHm HmInSuccN).
We prove the intermediate
claim HkP:
apply_fun e m ∈ P.
An exact proof term for the current goal is (HekP m HmInN).
An exact proof term for the current goal is (HvalR m HmInN).
An
exact proof term for the current goal is
(Hcoef_pos (apply_fun e m) HkP).
An
exact proof term for the current goal is
(nat_primrec_S 0 (weighted_step x e) m HmNat).
rewrite the current goal using HprimS (from left to right).
We prove the intermediate
claim HdefM:
nat_primrec 0 (weighted_step x e) m = weighted_sum x m e.
rewrite the current goal using HdefM (from left to right).
rewrite the current goal using HstepDef (from left to right).
Let m be given.
We prove the intermediate
claim HsuccNO:
ordsucc n ∈ ω.
An
exact proof term for the current goal is
(omega_ordsucc n HnO).
We prove the intermediate
claim HsuccNsubO:
ordsucc n ⊆ ω.
We prove the intermediate
claim HmO:
m ∈ ω.
An exact proof term for the current goal is (HsuccNsubO m HmInSuccN).
We prove the intermediate
claim HmNat:
nat_p m.
An
exact proof term for the current goal is
(omega_nat_p m HmO).
An exact proof term for the current goal is (Hind m HmNat HmInSuccN).
We prove the intermediate
claim HwsNNall:
∀m : set, m ∈ ordsucc n → 0 ≤ weighted_sum x m e.
Set Pnn to be the term
λm : set ⇒ m ∈ ordsucc n → 0 ≤ weighted_sum x m e.
We prove the intermediate
claim Hind:
∀m : set, nat_p m → Pnn m.
rewrite the current goal using (weighted_sum_0 x e) (from left to right).
An
exact proof term for the current goal is
(SNoLe_ref 0).
Let m be given.
Assume IHm: Pnn m.
We prove the intermediate
claim HnOrd:
ordinal n.
An
exact proof term for the current goal is
(nat_p_ordinal n HnNat).
We prove the intermediate
claim HnTS:
TransSet n.
We prove the intermediate
claim HmInN:
m ∈ n.
An
exact proof term for the current goal is
(ordsuccE n (ordsucc m) HSmIn).
Apply (HmCase (m ∈ n)) to the current goal.
We prove the intermediate
claim Hsub:
ordsucc m ⊆ n.
An
exact proof term for the current goal is
(HnTS (ordsucc m) HSmInN).
An
exact proof term for the current goal is
(Hsub m (ordsuccI2 m)).
rewrite the current goal using Heq (from right to left).
An
exact proof term for the current goal is
(ordsuccI2 m).
We prove the intermediate
claim HmInSuccN:
m ∈ ordsucc n.
An
exact proof term for the current goal is
((ordsuccI1 n) m HmInN).
We prove the intermediate
claim HaccNN:
0 ≤ weighted_sum x m e.
An exact proof term for the current goal is (IHm HmInSuccN).
We prove the intermediate
claim HaccR:
weighted_sum x m e ∈ R.
An exact proof term for the current goal is (HwsRall m HmInSuccN).
We prove the intermediate
claim HaccS:
SNo (weighted_sum x m e).
An
exact proof term for the current goal is
(real_SNo (weighted_sum x m e) HaccR).
We prove the intermediate
claim HkP:
apply_fun e m ∈ P.
An exact proof term for the current goal is (HekP m HmInN).
An exact proof term for the current goal is (HvalR m HmInN).
An exact proof term for the current goal is (HvalNN m HmInN).
An
exact proof term for the current goal is
(Hcoef_pos (apply_fun e m) HkP).
An
exact proof term for the current goal is
(nat_primrec_S 0 (weighted_step x e) m HmNat).
rewrite the current goal using HprimS (from left to right).
We prove the intermediate
claim HdefM:
nat_primrec 0 (weighted_step x e) m = weighted_sum x m e.
rewrite the current goal using HdefM (from left to right).
rewrite the current goal using HstepDef (from left to right).
An exact proof term for the current goal is HsumNN.
Let m be given.
We prove the intermediate
claim HsuccNO:
ordsucc n ∈ ω.
An
exact proof term for the current goal is
(omega_ordsucc n HnO).
We prove the intermediate
claim HsuccNsubO:
ordsucc n ⊆ ω.
We prove the intermediate
claim HmO:
m ∈ ω.
An exact proof term for the current goal is (HsuccNsubO m HmInSuccN).
We prove the intermediate
claim HmNat:
nat_p m.
An
exact proof term for the current goal is
(omega_nat_p m HmO).
An exact proof term for the current goal is (Hind m HmNat HmInSuccN).
We prove the intermediate
claim HnIn:
n ∈ ordsucc n.
An
exact proof term for the current goal is
(ordsuccI2 n).
We prove the intermediate
claim HwsRn:
weighted_sum x n e ∈ R.
An exact proof term for the current goal is (HwsRall n HnIn).
We prove the intermediate
claim HleS:
term0 ≤ weighted_sum x n e.
Set Q to be the term
λt : set ⇒ t ∈ ordsucc n → k0 ∈ t → term0 ≤ weighted_sum x t e.
We prove the intermediate
claim HQ0:
Q 0.
Apply FalseE to the current goal.
An
exact proof term for the current goal is
(EmptyE k0 Hk0In0).
We prove the intermediate
claim HQS:
∀t : set, nat_p t → Q t → Q (ordsucc t).
Let t be given.
We prove the intermediate
claim Hcases:
k0 ∈ t ∨ k0 = t.
An
exact proof term for the current goal is
(ordsuccE t k0 Hk0InSt).
Apply (Hcases (term0 ≤ weighted_sum x (ordsucc t) e)) to the current goal.
We prove the intermediate
claim HtInSuccN:
t ∈ ordsucc n.
We prove the intermediate
claim HnOrd2:
ordinal n.
An
exact proof term for the current goal is
(nat_p_ordinal n HnNat).
We prove the intermediate
claim HnTS2:
TransSet n.
An
exact proof term for the current goal is
(HsuccTS2 (ordsucc t) HStIn).
An
exact proof term for the current goal is
(HsubSt t (ordsuccI2 t)).
We prove the intermediate
claim HleT:
term0 ≤ weighted_sum x t e.
An exact proof term for the current goal is (IHt HtInSuccN Hk0InT).
We prove the intermediate
claim HtR:
weighted_sum x t e ∈ R.
An exact proof term for the current goal is (HwsRall t HtInSuccN).
We prove the intermediate
claim HtS:
SNo (weighted_sum x t e).
An
exact proof term for the current goal is
(real_SNo (weighted_sum x t e) HtR).
We prove the intermediate
claim Hmono:
weighted_sum x t e ≤ weighted_sum x (ordsucc t) e.
We prove the intermediate
claim HtInN:
t ∈ n.
We prove the intermediate
claim HnOrd2:
ordinal n.
An
exact proof term for the current goal is
(nat_p_ordinal n HnNat).
We prove the intermediate
claim HnTS2:
TransSet n.
An
exact proof term for the current goal is
(ordsuccE n (ordsucc t) HStIn).
Apply (HtCase (t ∈ n)) to the current goal.
We prove the intermediate
claim Hsub:
ordsucc t ⊆ n.
An
exact proof term for the current goal is
(HnTS2 (ordsucc t) HStInN).
An
exact proof term for the current goal is
(Hsub t (ordsuccI2 t)).
rewrite the current goal using Heq (from right to left).
An
exact proof term for the current goal is
(ordsuccI2 t).
An
exact proof term for the current goal is
(Hcoef_pos (apply_fun e t) (HekP t HtInN)).
An exact proof term for the current goal is (HvalR t HtInN).
An exact proof term for the current goal is (HvalNN t HtInN).
We prove the intermediate
claim HwsEq:
weighted_sum x (ordsucc t) e = weighted_step x e t (weighted_sum x t e).
An exact proof term for the current goal is (weighted_sum_S x e t HtNat).
rewrite the current goal using HwsEq (from left to right).
rewrite the current goal using HstepDef (from left to right).
We prove the intermediate
claim HtInSuccN:
t ∈ ordsucc n.
We prove the intermediate
claim HnOrd2:
ordinal n.
An
exact proof term for the current goal is
(nat_p_ordinal n HnNat).
We prove the intermediate
claim HnTS2:
TransSet n.
An
exact proof term for the current goal is
(HsuccTS2 (ordsucc t) HStIn).
An
exact proof term for the current goal is
(HsubSt t (ordsuccI2 t)).
We prove the intermediate
claim HwsNN:
0 ≤ weighted_sum x t e.
An exact proof term for the current goal is (HwsNNall t HtInSuccN).
We prove the intermediate
claim HwsR:
weighted_sum x t e ∈ R.
An exact proof term for the current goal is (HwsRall t HtInSuccN).
We prove the intermediate
claim HwsS:
SNo (weighted_sum x t e).
An
exact proof term for the current goal is
(real_SNo (weighted_sum x t e) HwsR).
We prove the intermediate
claim HtInN:
t ∈ n.
We prove the intermediate
claim HnOrd2:
ordinal n.
An
exact proof term for the current goal is
(nat_p_ordinal n HnNat).
We prove the intermediate
claim HnTS2:
TransSet n.
An
exact proof term for the current goal is
(ordsuccE n (ordsucc t) HStIn).
Apply (HtCase (t ∈ n)) to the current goal.
We prove the intermediate
claim Hsub:
ordsucc t ⊆ n.
An
exact proof term for the current goal is
(HnTS2 (ordsucc t) HStInN).
An
exact proof term for the current goal is
(Hsub t (ordsuccI2 t)).
rewrite the current goal using Heq (from right to left).
An
exact proof term for the current goal is
(ordsuccI2 t).
rewrite the current goal using Hk0EqT (from right to left).
Use reflexivity.
An
exact proof term for the current goal is
(Hcoef_pos (apply_fun e t) (HekP t HtInN)).
An exact proof term for the current goal is (HvalR t HtInN).
We prove the intermediate
claim HwsEq:
weighted_sum x (ordsucc t) e = weighted_step x e t (weighted_sum x t e).
An exact proof term for the current goal is (weighted_sum_S x e t HtNat).
rewrite the current goal using HwsEq (from left to right).
rewrite the current goal using HstepDef (from left to right).
rewrite the current goal using HaddCom (from left to right).
rewrite the current goal using HttermEq (from left to right).
An
exact proof term for the current goal is
(nat_ind Q HQ0 HQS n HnNat HnIn Hk0In).
An
exact proof term for the current goal is
(Rle_of_SNoLe term0 (weighted_sum x n e) HtermR HwsRn HleS).
We will
prove Rlt 0 (weighted_sum x n e).
Apply FalseE to the current goal.
Let k be given.
An exact proof term for the current goal is (λH ⇒ H).
Apply FalseE to the current goal.
Apply Hnone to the current goal.
We use k to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hk.
An exact proof term for the current goal is (Hneq0 Heq).
We prove the intermediate
claim Hp0n:
apply_fun p n = 0.
We prove the intermediate
claim Hind:
∀m : set, nat_p m → Pp m.
We prove the intermediate
claim H0E:
0 = Empty.
rewrite the current goal using H0E (from left to right).
An exact proof term for the current goal is Hp0.
Let m be given.
Assume IHm: Pp m.
We prove the intermediate
claim HnOrd:
ordinal n.
An
exact proof term for the current goal is
(nat_p_ordinal n HnNat).
We prove the intermediate
claim HnTS:
TransSet n.
An
exact proof term for the current goal is
(HsuccTS (ordsucc m) HSmIn).
We prove the intermediate
claim HmInSuccN:
m ∈ ordsucc n.
An
exact proof term for the current goal is
(HsubSm m (ordsuccI2 m)).
We prove the intermediate
claim HmInN:
m ∈ n.
An
exact proof term for the current goal is
(ordsuccE n (ordsucc m) HSmIn).
Apply (Hcase (m ∈ n)) to the current goal.
We prove the intermediate
claim Hsub:
ordsucc m ⊆ n.
An
exact proof term for the current goal is
(HnTS (ordsucc m) HIn).
An
exact proof term for the current goal is
(Hsub m (ordsuccI2 m)).
rewrite the current goal using Heq (from right to left).
An
exact proof term for the current goal is
(ordsuccI2 m).
rewrite the current goal using (HpStep m HmInN) (from left to right).
We prove the intermediate
claim HpM:
apply_fun p m = 0.
An exact proof term for the current goal is (IHm HmInSuccN).
rewrite the current goal using HpM (from left to right).
rewrite the current goal using (Hval0 m HmInN) (from left to right).
Use reflexivity.
We prove the intermediate
claim HnIn:
n ∈ ordsucc n.
An
exact proof term for the current goal is
(ordsuccI2 n).
An exact proof term for the current goal is (Hind n HnNat HnIn).
We prove the intermediate
claim H10:
1 = 0.
rewrite the current goal using Hpn1 (from right to left).
An exact proof term for the current goal is Hp0n.
An
exact proof term for the current goal is
(neq_1_0 H10).
Set w_of to be the term
λx : set ⇒ Eps_i (λy : set ⇒ Pval x y).
Set f to be the term
graph X w_of.
We prove the intermediate
claim Hw_of:
∀x : set, x ∈ X → Pval x (w_of x).
Let x be given.
Set Q to be the term λy : set ⇒ Pval x y.
We prove the intermediate
claim Hex:
∃y : set, Q y.
Apply HexPack to the current goal.
Let F be given.
Assume HFpack.
We prove the intermediate
claim HfinSub:
finite F ∧ F ⊆ P.
We prove the intermediate
claim Hsupp:
∀f : set, f ∈ P → apply_fun f x ≠ 0 → f ∈ F.
We prove the intermediate
claim HFfin:
finite F.
An
exact proof term for the current goal is
(andEL (finite F) (F ⊆ P) HfinSub).
We prove the intermediate
claim HFsubP:
F ⊆ P.
An
exact proof term for the current goal is
(andER (finite F) (F ⊆ P) HfinSub).
Apply Hexn to the current goal.
Let n be given.
Assume Hnpack.
We prove the intermediate
claim HnO:
n ∈ ω.
Apply Hexe to the current goal.
Let e be given.
Assume Hepack.
We prove the intermediate
claim Hbij:
bijection n F e.
Apply Hexp to the current goal.
Let p be given.
Assume Hppack.
We prove the intermediate
claim Hpn1:
apply_fun p n = 1.
We use (weighted_sum x n e) to witness the existential quantifier.
We will
prove Q (weighted_sum x n e).
We prove the intermediate
claim HQ:
Q (weighted_sum x n e) = Pval x (weighted_sum x n e).
rewrite the current goal using HQ (from left to right).
rewrite the current goal using HPdef (from left to right).
We use F to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HFfin.
An exact proof term for the current goal is HFsubP.
An exact proof term for the current goal is Hsupp.
We use n to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HnO.
We use e to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hbij.
We use p to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HpFun.
An exact proof term for the current goal is Hp0.
An exact proof term for the current goal is HpStep.
An exact proof term for the current goal is Hpn1.
Apply Hex to the current goal.
Let y be given.
An
exact proof term for the current goal is
(Eps_i_ax Q y Hy).
We prove the intermediate
claim HfPos:
∀x : set, x ∈ X → Rlt 0 (apply_fun f x).
Let x be given.
We prove the intermediate
claim Hfdef:
f = graph X w_of.
We prove the intermediate
claim Hfxeq:
apply_fun f x = w_of x.
rewrite the current goal using Hfdef (from left to right).
An
exact proof term for the current goal is
(apply_fun_graph X w_of x HxX).
rewrite the current goal using Hfxeq (from left to right).
We prove the intermediate claim Hw: Pval x (w_of x).
An exact proof term for the current goal is (Hw_of x HxX).
Apply Hw to the current goal.
Let F be given.
Assume HFpack.
We prove the intermediate
claim HfinSub:
finite F ∧ F ⊆ P.
We prove the intermediate
claim Hsupp:
∀f : set, f ∈ P → apply_fun f x ≠ 0 → f ∈ F.
We prove the intermediate
claim HFfin:
finite F.
An
exact proof term for the current goal is
(andEL (finite F) (F ⊆ P) HfinSub).
We prove the intermediate
claim HFsubP:
F ⊆ P.
An
exact proof term for the current goal is
(andER (finite F) (F ⊆ P) HfinSub).
Apply Hexn to the current goal.
Let n be given.
Assume Hnpack.
We prove the intermediate
claim HnO:
n ∈ ω.
Apply Hexe to the current goal.
Let e be given.
Assume Hepack.
We prove the intermediate
claim Hbij:
bijection n F e.
Apply Hexp to the current goal.
Let p be given.
Assume Hppack.
We prove the intermediate
claim HyEq:
w_of x = weighted_sum x n e.
We prove the intermediate
claim Hpn1:
apply_fun p n = 1.
We prove the intermediate
claim Hpos:
Rlt 0 (weighted_sum x n e).
An exact proof term for the current goal is (weighted_sum_pos_on_point x F n e p HxX HFfin HFsubP Hsupp HnO Hbij HpFun Hp0 HpStep Hpn1).
rewrite the current goal using HyEq (from left to right).
An exact proof term for the current goal is Hpos.
Let c and x be given.
We prove the intermediate
claim HxX:
x ∈ X.
We prove the intermediate
claim HcPow:
c ∈ 𝒫 X.
An exact proof term for the current goal is (HCsubPow c HcC).
We prove the intermediate
claim HcSubX:
c ⊆ X.
An
exact proof term for the current goal is
(PowerE X c HcPow).
An exact proof term for the current goal is (HcSubX x Hxc).
We prove the intermediate
claim Hfdef:
f = graph X w_of.
We prove the intermediate
claim Hfxeq:
apply_fun f x = w_of x.
rewrite the current goal using Hfdef (from left to right).
An
exact proof term for the current goal is
(apply_fun_graph X w_of x HxX).
rewrite the current goal using Hfxeq (from left to right).
We prove the intermediate claim Hw: Pval x (w_of x).
An exact proof term for the current goal is (Hw_of x HxX).
Apply Hw to the current goal.
Let F be given.
Assume HFpack.
We prove the intermediate
claim HfinSub:
finite F ∧ F ⊆ P.
We prove the intermediate
claim Hsupp:
∀f : set, f ∈ P → apply_fun f x ≠ 0 → f ∈ F.
We prove the intermediate
claim HFfin:
finite F.
An
exact proof term for the current goal is
(andEL (finite F) (F ⊆ P) HfinSub).
We prove the intermediate
claim HFsubP:
F ⊆ P.
An
exact proof term for the current goal is
(andER (finite F) (F ⊆ P) HfinSub).
Apply Hexn to the current goal.
Let n be given.
Assume Hnpack.
We prove the intermediate
claim HnO:
n ∈ ω.
Apply Hexe to the current goal.
Let e be given.
Assume Hepack.
We prove the intermediate
claim Hbij:
bijection n F e.
Apply Hexp to the current goal.
Let p be given.
Assume Hppack.
We prove the intermediate
claim HyEq:
w_of x = weighted_sum x n e.
We prove the intermediate
claim Hpn1:
apply_fun p n = 1.
We prove the intermediate
claim Hle:
Rle (weighted_sum x n e) (apply_fun eps c).
An exact proof term for the current goal is (weighted_sum_le_eps_on_point c x F n e p HcC HxX Hxc HFfin HFsubP Hsupp HnO Hbij HpFun Hp0 HpStep Hpn1).
rewrite the current goal using HyEq (from left to right) at position 1.
An exact proof term for the current goal is Hle.
We use f to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
We prove the intermediate
claim HcrAll:
((((L0 ∧ L1) ∧ L2) ∧ L3) ∧ L4) ∧ L5.
We prove the intermediate claim Hlocal_rule: L5.
An
exact proof term for the current goal is
(andER ((((L0 ∧ L1) ∧ L2) ∧ L3) ∧ L4) L5 HcrAll).
We prove the intermediate
claim HpickN:
∀x : set, x ∈ X → pickN x ∈ Tx ∧ x ∈ pickN x ∧ ∃F0 : set, finite F0 ∧ F0 ⊆ P ∧ ∀ff : set, ff ∈ P → support_of X Tx ff ∩ pickN x ≠ Empty → ff ∈ F0.
Let x be given.
Apply Hex to the current goal.
Let N be given.
Set UFam to be the term
Repl X (λx : set ⇒ pickN x).
We use UFam to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
Let N be given.
Apply (ReplE X (λx0 : set ⇒ pickN x0) N HN) to the current goal.
Let x be given.
We prove the intermediate
claim HxX:
x ∈ X.
An
exact proof term for the current goal is
(andEL (x ∈ X) (N = pickN x) Hx).
We prove the intermediate
claim Heq:
N = pickN x.
An
exact proof term for the current goal is
(andER (x ∈ X) (N = pickN x) Hx).
rewrite the current goal using Heq (from left to right).
We prove the intermediate
claim HNprop:
pickN x ∈ Tx ∧ x ∈ pickN x ∧ ∃F0 : set, finite F0 ∧ F0 ⊆ P ∧ ∀ff : set, ff ∈ P → support_of X Tx ff ∩ pickN x ≠ Empty → ff ∈ F0.
An exact proof term for the current goal is (HpickN x HxX).
We prove the intermediate
claim HNpair:
pickN x ∈ Tx ∧ x ∈ pickN x.
An
exact proof term for the current goal is
(andEL (pickN x ∈ Tx ∧ x ∈ pickN x) (∃F0 : set, finite F0 ∧ F0 ⊆ P ∧ ∀ff : set, ff ∈ P → support_of X Tx ff ∩ pickN x ≠ Empty → ff ∈ F0) HNprop).
An
exact proof term for the current goal is
(andEL (pickN x ∈ Tx) (x ∈ pickN x) HNpair).
Let y be given.
Apply (UnionE UFam y Hy) to the current goal.
Let N be given.
We prove the intermediate
claim HyN:
y ∈ N.
An
exact proof term for the current goal is
(andEL (y ∈ N) (N ∈ UFam) HNy).
We prove the intermediate
claim HNU:
N ∈ UFam.
An
exact proof term for the current goal is
(andER (y ∈ N) (N ∈ UFam) HNy).
We prove the intermediate
claim HNTx:
N ∈ Tx.
Apply (ReplE X (λx0 : set ⇒ pickN x0) N HNU) to the current goal.
Let x be given.
We prove the intermediate
claim HxX:
x ∈ X.
An
exact proof term for the current goal is
(andEL (x ∈ X) (N = pickN x) Hx).
We prove the intermediate
claim Heq:
N = pickN x.
An
exact proof term for the current goal is
(andER (x ∈ X) (N = pickN x) Hx).
rewrite the current goal using Heq (from left to right).
We prove the intermediate
claim HNprop:
pickN x ∈ Tx ∧ x ∈ pickN x ∧ ∃F0 : set, finite F0 ∧ F0 ⊆ P ∧ ∀ff : set, ff ∈ P → support_of X Tx ff ∩ pickN x ≠ Empty → ff ∈ F0.
An exact proof term for the current goal is (HpickN x HxX).
We prove the intermediate
claim HNpair:
pickN x ∈ Tx ∧ x ∈ pickN x.
An
exact proof term for the current goal is
(andEL (pickN x ∈ Tx ∧ x ∈ pickN x) (∃F0 : set, finite F0 ∧ F0 ⊆ P ∧ ∀ff : set, ff ∈ P → support_of X Tx ff ∩ pickN x ≠ Empty → ff ∈ F0) HNprop).
An
exact proof term for the current goal is
(andEL (pickN x ∈ Tx) (x ∈ pickN x) HNpair).
We prove the intermediate
claim HsubPow:
Tx ⊆ 𝒫 X.
We prove the intermediate
claim HNPow:
N ∈ 𝒫 X.
An exact proof term for the current goal is (HsubPow N HNTx).
We prove the intermediate
claim HNsubX:
N ⊆ X.
An
exact proof term for the current goal is
(PowerE X N HNPow).
An exact proof term for the current goal is (HNsubX y HyN).
Let y be given.
Set N to be the term pickN y.
We prove the intermediate
claim HNinU:
N ∈ UFam.
An
exact proof term for the current goal is
(ReplI X (λx0 : set ⇒ pickN x0) y HyX).
We prove the intermediate
claim HNy:
y ∈ N.
We prove the intermediate
claim HNprop:
pickN y ∈ Tx ∧ y ∈ pickN y ∧ ∃F0 : set, finite F0 ∧ F0 ⊆ P ∧ ∀ff : set, ff ∈ P → support_of X Tx ff ∩ pickN y ≠ Empty → ff ∈ F0.
An exact proof term for the current goal is (HpickN y HyX).
We prove the intermediate
claim HNpair:
pickN y ∈ Tx ∧ y ∈ pickN y.
An
exact proof term for the current goal is
(andEL (pickN y ∈ Tx ∧ y ∈ pickN y) (∃F0 : set, finite F0 ∧ F0 ⊆ P ∧ ∀ff : set, ff ∈ P → support_of X Tx ff ∩ pickN y ≠ Empty → ff ∈ F0) HNprop).
An
exact proof term for the current goal is
(andER (pickN y ∈ Tx) (y ∈ pickN y) HNpair).
An
exact proof term for the current goal is
(UnionI UFam y N HNy HNinU).
Let U0 be given.
Apply (ReplE X (λx0 : set ⇒ pickN x0) U0 HU0) to the current goal.
Let x be given.
We prove the intermediate
claim HxX:
x ∈ X.
An
exact proof term for the current goal is
(andEL (x ∈ X) (U0 = pickN x) Hx).
We prove the intermediate
claim HU0eq:
U0 = pickN x.
An
exact proof term for the current goal is
(andER (x ∈ X) (U0 = pickN x) Hx).
rewrite the current goal using HU0eq (from left to right).
We prove the intermediate
claim HNprop:
pickN x ∈ Tx ∧ x ∈ pickN x ∧ ∃F0 : set, finite F0 ∧ F0 ⊆ P ∧ ∀ff : set, ff ∈ P → support_of X Tx ff ∩ pickN x ≠ Empty → ff ∈ F0.
An exact proof term for the current goal is (HpickN x HxX).
An
exact proof term for the current goal is
(andER (pickN x ∈ Tx ∧ x ∈ pickN x) (∃F0 : set, finite F0 ∧ F0 ⊆ P ∧ ∀ff : set, ff ∈ P → support_of X Tx ff ∩ pickN x ≠ Empty → ff ∈ F0) HNprop).
Apply HexF0 to the current goal.
Let F0 be given.
We prove the intermediate
claim HF0left:
finite F0 ∧ F0 ⊆ P.
We prove the intermediate
claim HF0hit:
∀ff : set, ff ∈ P → support_of X Tx ff ∩ pickN x ≠ Empty → ff ∈ F0.
We prove the intermediate
claim HF0fin:
finite F0.
An
exact proof term for the current goal is
(andEL (finite F0) (F0 ⊆ P) HF0left).
We prove the intermediate
claim HF0subP:
F0 ⊆ P.
An
exact proof term for the current goal is
(andER (finite F0) (F0 ⊆ P) HF0left).
We prove the intermediate
claim Hexne0:
∃n0 e0 : set, n0 ∈ ω ∧ bijection n0 F0 e0.
We prove the intermediate
claim HNsubX:
pickN x ⊆ X.
We prove the intermediate
claim HsubPow:
Tx ⊆ 𝒫 X.
We prove the intermediate
claim HNpair:
pickN x ∈ Tx ∧ x ∈ pickN x.
An
exact proof term for the current goal is
(andEL (pickN x ∈ Tx ∧ x ∈ pickN x) (∃F0 : set, finite F0 ∧ F0 ⊆ P ∧ ∀ff : set, ff ∈ P → support_of X Tx ff ∩ pickN x ≠ Empty → ff ∈ F0) HNprop).
We prove the intermediate
claim HNtx:
pickN x ∈ Tx.
An
exact proof term for the current goal is
(andEL (pickN x ∈ Tx) (x ∈ pickN x) HNpair).
We prove the intermediate
claim HNPow:
pickN x ∈ 𝒫 X.
An exact proof term for the current goal is (HsubPow (pickN x) HNtx).
An
exact proof term for the current goal is
(PowerE X (pickN x) HNPow).
We prove the intermediate
claim Hzero_on_N:
∀y ff : set, y ∈ pickN x → ff ∈ P → ¬ (ff ∈ F0) → apply_fun ff y = 0.
Let y and ff be given.
An exact proof term for the current goal is H0.
Apply FalseE to the current goal.
We prove the intermediate
claim HyX:
y ∈ X.
An exact proof term for the current goal is (HNsubX y HyN).
We prove the intermediate
claim HyNZ:
apply_fun ff y ≠ 0.
An exact proof term for the current goal is Hne0.
We prove the intermediate
claim HyA0:
y ∈ A0.
An exact proof term for the current goal is HyNZ.
We prove the intermediate
claim HA0subX:
A0 ⊆ X.
Let z be given.
An
exact proof term for the current goal is
(SepE1 X (λz0 : set ⇒ apply_fun ff z0 ≠ 0) z Hz).
We prove the intermediate
claim HA0subcl:
A0 ⊆ closure_of X Tx A0.
We prove the intermediate
claim HySupp:
y ∈ support_of X Tx ff.
rewrite the current goal using HsuppDef (from left to right).
An exact proof term for the current goal is (HA0subcl y HyA0).
We prove the intermediate
claim HyCap:
y ∈ support_of X Tx ff ∩ pickN x.
We prove the intermediate
claim HyEmp:
y ∈ Empty.
rewrite the current goal using Hcap0 (from right to left).
An exact proof term for the current goal is HyCap.
An
exact proof term for the current goal is
(EmptyE y HyEmp).
We prove the intermediate
claim HffF0:
ff ∈ F0.
An exact proof term for the current goal is (HF0hit ff HffP Hhit).
An exact proof term for the current goal is (HffNot HffF0).
We prove the intermediate
claim Hnonzero_in_F0:
∀y ff : set, y ∈ pickN x → ff ∈ P → apply_fun ff y ≠ 0 → ff ∈ F0.
Let y and ff be given.
Apply (xm (ff ∈ F0)) to the current goal.
An exact proof term for the current goal is HffF0.
Apply FalseE to the current goal.
We prove the intermediate
claim H0:
apply_fun ff y = 0.
An exact proof term for the current goal is (Hzero_on_N y ff HyN HffP Hnot).
An exact proof term for the current goal is (Hne0 H0).
Apply Hexne0 to the current goal.
Let n0 be given.
Apply Hexe0 to the current goal.
Let e0 be given.
We prove the intermediate
claim Hn0O:
n0 ∈ ω.
An
exact proof term for the current goal is
(andEL (n0 ∈ ω) (bijection n0 F0 e0) Hne0).
We prove the intermediate
claim Hbij0:
bijection n0 F0 e0.
An
exact proof term for the current goal is
(andER (n0 ∈ ω) (bijection n0 F0 e0) Hne0).
Set g to be the term
graph (pickN x) (λy0 : set ⇒ weighted_sum y0 n0 e0).
Set A to be the term pickN x.
We prove the intermediate
claim Hn0Nat:
nat_p n0.
An
exact proof term for the current goal is
(omega_nat_p n0 Hn0O).
We prove the intermediate
claim Hbase:
Pw 0.
We prove the intermediate
claim Hg0fun:
function_on (graph A (λy0 : set ⇒ weighted_sum y0 0 e0)) A R.
Let y0 be given.
We prove the intermediate
claim Happ:
apply_fun (graph A (λy1 : set ⇒ weighted_sum y1 0 e0)) y0 = weighted_sum y0 0 e0.
An
exact proof term for the current goal is
(apply_fun_graph A (λy1 : set ⇒ weighted_sum y1 0 e0) y0 Hy0A).
rewrite the current goal using Happ (from left to right).
We prove the intermediate
claim Hws0:
weighted_sum y0 0 e0 = 0.
An exact proof term for the current goal is (weighted_sum_0 y0 e0).
rewrite the current goal using Hws0 (from left to right) at position 1.
An
exact proof term for the current goal is
real_0.
Let y0 be given.
rewrite the current goal using Hconst (from left to right).
We prove the intermediate
claim Happ:
apply_fun (graph A (λy1 : set ⇒ weighted_sum y1 0 e0)) y0 = weighted_sum y0 0 e0.
An
exact proof term for the current goal is
(apply_fun_graph A (λy1 : set ⇒ weighted_sum y1 0 e0) y0 Hy0A).
rewrite the current goal using Happ (from left to right).
We prove the intermediate
claim Hws0:
weighted_sum y0 0 e0 = 0.
An exact proof term for the current goal is (weighted_sum_0 y0 e0).
rewrite the current goal using Hws0 (from left to right) at position 1.
Use reflexivity.
We prove the intermediate
claim Hstep:
∀n : set, nat_p n → Pw n → Pw (ordsucc n).
Let n be given.
Assume IH: Pw n.
We prove the intermediate
claim Hsub:
ordsucc n ⊆ n0.
We prove the intermediate
claim HnInN0:
n ∈ n0.
An
exact proof term for the current goal is
(Hsub n (ordsuccI2 n)).
We prove the intermediate
claim HnInSuccN0:
n ∈ ordsucc n0.
An
exact proof term for the current goal is
(ordsuccI1 n0 n HnInN0).
An exact proof term for the current goal is (IH HnInSuccN0).
We prove the intermediate
claim HeFun:
function_on e0 n0 F0.
Apply Hbij0 to the current goal.
Assume Hfun.
Assume _.
An exact proof term for the current goal is Hfun.
We prove the intermediate
claim HfkF0:
apply_fun e0 n ∈ F0.
An exact proof term for the current goal is (HeFun n HnInN0).
We prove the intermediate
claim HfkP:
apply_fun e0 n ∈ P.
An
exact proof term for the current goal is
(HF0subP (apply_fun e0 n) HfkF0).
An
exact proof term for the current goal is
(HPcont (apply_fun e0 n) HfkP).
An
exact proof term for the current goal is
(Hcoef_pos (apply_fun e0 n) HfkP).
Let y0 be given.
We prove the intermediate
claim Hwsnfun:
function_on (graph A (λy1 : set ⇒ weighted_sum y1 n e0)) A R.
We prove the intermediate
claim HwsnR:
apply_fun (graph A (λy1 : set ⇒ weighted_sum y1 n e0)) y0 ∈ R.
An exact proof term for the current goal is (Hwsnfun y0 Hy0A).
An exact proof term for the current goal is (Htermfun y0 Hy0A).
rewrite the current goal using Hadd (from left to right).
We prove the intermediate
claim Happwsn:
apply_fun (graph A (λy1 : set ⇒ weighted_sum y1 n e0)) y0 = weighted_sum y0 n e0.
An
exact proof term for the current goal is
(apply_fun_graph A (λy1 : set ⇒ weighted_sum y1 n e0) y0 Hy0A).
rewrite the current goal using Happwsn (from left to right).
rewrite the current goal using HconstEq (from left to right).
An exact proof term for the current goal is HcR.
An exact proof term for the current goal is (Hfkfun y0 Hy0A).
rewrite the current goal using Hmul (from left to right).
rewrite the current goal using HconstEq2 (from left to right).
An
exact proof term for the current goal is
(apply_fun_graph A (λy1 : set ⇒ weighted_sum y1 (ordsucc n) e0) y0 Hy0A).
rewrite the current goal using HappS (from left to right).
We prove the intermediate
claim HwsS:
weighted_sum y0 (ordsucc n) e0 = weighted_step y0 e0 n (weighted_sum y0 n e0).
An exact proof term for the current goal is (weighted_sum_S y0 e0 n HnNat).
rewrite the current goal using HwsS (from left to right).
rewrite the current goal using HstepDef (from left to right).
Use reflexivity.
Let y0 be given.
An
exact proof term for the current goal is
(apply_fun_graph A (λy1 : set ⇒ weighted_sum y1 (ordsucc n) e0) y0 Hy0A).
rewrite the current goal using HappS (from left to right).
We prove the intermediate
claim HwsS:
weighted_sum y0 (ordsucc n) e0 = weighted_step y0 e0 n (weighted_sum y0 n e0).
An exact proof term for the current goal is (weighted_sum_S y0 e0 n HnNat).
rewrite the current goal using HwsS (from left to right).
We prove the intermediate
claim Hwsnfun:
function_on (graph A (λy1 : set ⇒ weighted_sum y1 n e0)) A R.
We prove the intermediate
claim Happn:
apply_fun (graph A (λy1 : set ⇒ weighted_sum y1 n e0)) y0 = weighted_sum y0 n e0.
An
exact proof term for the current goal is
(apply_fun_graph A (λy1 : set ⇒ weighted_sum y1 n e0) y0 Hy0A).
We prove the intermediate
claim HaccR:
weighted_sum y0 n e0 ∈ R.
rewrite the current goal using Happn (from right to left).
An exact proof term for the current goal is (Hwsnfun y0 Hy0A).
We prove the intermediate
claim Hy0X:
y0 ∈ X.
An exact proof term for the current goal is (HNsubX y0 Hy0A).
An
exact proof term for the current goal is
(HPval_in_R (apply_fun e0 n) y0 HfkP Hy0X).
rewrite the current goal using HstepDef (from left to right).
We prove the intermediate claim Hwsn0: Pw n0.
An
exact proof term for the current goal is
(nat_ind Pw Hbase Hstep n0 Hn0Nat).
We prove the intermediate
claim Hn0In:
n0 ∈ ordsucc n0.
An
exact proof term for the current goal is
(ordsuccI2 n0).
An exact proof term for the current goal is (Hwsn0 Hn0In).
We prove the intermediate
claim HfFunN:
function_on f (pickN x) R.
Let y1 be given.
We prove the intermediate
claim Hy1X:
y1 ∈ X.
An exact proof term for the current goal is (HNsubX y1 Hy1N).
We prove the intermediate
claim Hfdef:
f = graph X w_of.
We prove the intermediate
claim Hfy1:
apply_fun f y1 = w_of y1.
rewrite the current goal using Hfdef (from left to right).
An
exact proof term for the current goal is
(apply_fun_graph X w_of y1 Hy1X).
rewrite the current goal using Hfy1 (from left to right).
We prove the intermediate claim Hw: Pval y1 (w_of y1).
An exact proof term for the current goal is (Hw_of y1 Hy1X).
Apply Hw to the current goal.
Let F be given.
Assume HFpack.
We prove the intermediate
claim Hleft:
(finite F ∧ F ⊆ P) ∧ (∀f0 : set, f0 ∈ P → apply_fun f0 y1 ≠ 0 → f0 ∈ F).
We prove the intermediate
claim HfinSub:
finite F ∧ F ⊆ P.
We prove the intermediate
claim Hsupp:
∀f0 : set, f0 ∈ P → apply_fun f0 y1 ≠ 0 → f0 ∈ F.
We prove the intermediate
claim HFfin:
finite F.
An
exact proof term for the current goal is
(andEL (finite F) (F ⊆ P) HfinSub).
We prove the intermediate
claim HFsubP:
F ⊆ P.
An
exact proof term for the current goal is
(andER (finite F) (F ⊆ P) HfinSub).
Apply Hexn to the current goal.
Let n be given.
Assume Hnpack.
We prove the intermediate
claim HnO:
n ∈ ω.
Apply Hexe to the current goal.
Let e be given.
Assume Hepack.
We prove the intermediate
claim Hbij:
bijection n F e.
Apply Hexp to the current goal.
Let p be given.
Assume Hppack.
We prove the intermediate
claim HyEq:
w_of y1 = weighted_sum y1 n e.
We prove the intermediate
claim Hpn1:
apply_fun p n = 1.
We prove the intermediate
claim Hpos:
Rlt 0 (weighted_sum y1 n e).
An exact proof term for the current goal is (weighted_sum_pos_on_point y1 F n e p Hy1X HFfin HFsubP Hsupp HnO Hbij HpFun Hp0 HpStep Hpn1).
We prove the intermediate
claim HwsR:
weighted_sum y1 n e ∈ R.
An
exact proof term for the current goal is
(RltE_right 0 (weighted_sum y1 n e) Hpos).
rewrite the current goal using HyEq (from left to right).
An exact proof term for the current goal is HwsR.
Let y0 be given.
We prove the intermediate
claim Hy0X:
y0 ∈ X.
An exact proof term for the current goal is (HNsubX y0 Hy0N).
We prove the intermediate
claim Hgdef:
g = graph (pickN x) (λy0 : set ⇒ weighted_sum y0 n0 e0).
We prove the intermediate
claim Hfdef:
f = graph X w_of.
We prove the intermediate
claim Hg0:
apply_fun g y0 = weighted_sum y0 n0 e0.
rewrite the current goal using Hgdef (from left to right) at position 1.
An
exact proof term for the current goal is
(apply_fun_graph (pickN x) (λy0 : set ⇒ weighted_sum y0 n0 e0) y0 Hy0N).
We prove the intermediate
claim Hf0:
apply_fun f y0 = w_of y0.
rewrite the current goal using Hfdef (from left to right) at position 1.
An
exact proof term for the current goal is
(apply_fun_graph X w_of y0 Hy0X).
rewrite the current goal using Hg0 (from left to right).
rewrite the current goal using Hf0 (from left to right).
We prove the intermediate claim HwP: Pval y0 (w_of y0).
An exact proof term for the current goal is (Hw_of y0 Hy0X).
Apply HwP to the current goal.
Let F1 be given.
Assume HF1pack.
We prove the intermediate
claim HF1core:
(finite F1 ∧ F1 ⊆ P) ∧ (∀f1 : set, f1 ∈ P → apply_fun f1 y0 ≠ 0 → f1 ∈ F1).
Apply Hexn1 to the current goal.
Let n1 be given.
Assume Hn1pack.
We prove the intermediate
claim Hn1O:
n1 ∈ ω.
Apply Hexe1 to the current goal.
Let e1 be given.
Assume He1pack.
We prove the intermediate
claim He1bij:
bijection n1 F1 e1.
Apply Hexp1 to the current goal.
Let p1 be given.
Assume Hp1pack.
We prove the intermediate
claim HwEq:
w_of y0 = weighted_sum y0 n1 e1.
rewrite the current goal using HwEq (from left to right).
We prove the intermediate
claim HF1finSub:
finite F1 ∧ F1 ⊆ P.
An
exact proof term for the current goal is
(andEL (finite F1 ∧ F1 ⊆ P) (∀f1 : set, f1 ∈ P → apply_fun f1 y0 ≠ 0 → f1 ∈ F1) HF1core).
We prove the intermediate
claim HF1subP:
F1 ⊆ P.
An
exact proof term for the current goal is
(andER (finite F1) (F1 ⊆ P) HF1finSub).
We prove the intermediate
claim He1fun:
function_on e1 n1 F1.
We prove the intermediate
claim He1uniq:
∀y : set, y ∈ F1 → ∃x0 : set, x0 ∈ n1 ∧ apply_fun e1 x0 = y ∧ (∀x' : set, x' ∈ n1 → apply_fun e1 x' = y → x' = x0).
We prove the intermediate
claim HekP:
∀k : set, k ∈ n1 → apply_fun e1 k ∈ P.
Let k be given.
We prove the intermediate
claim HkF1:
apply_fun e1 k ∈ F1.
An exact proof term for the current goal is (He1fun k Hk).
An
exact proof term for the current goal is
(HF1subP (apply_fun e1 k) HkF1).
Let k be given.
An
exact proof term for the current goal is
(Hzero_on_N y0 (apply_fun e1 k) Hy0N (HekP k Hk) HnotF0).
We prove the intermediate
claim He0fun:
function_on e0 n0 F0.
We prove the intermediate
claim He0uniq:
∀y : set, y ∈ F0 → ∃x0 : set, x0 ∈ n0 ∧ apply_fun e0 x0 = y ∧ (∀x' : set, x' ∈ n0 → apply_fun e0 x' = y → x' = x0).
We prove the intermediate
claim He0kP:
∀k : set, k ∈ n0 → apply_fun e0 k ∈ P.
Let k be given.
We prove the intermediate
claim HkF0:
apply_fun e0 k ∈ F0.
An exact proof term for the current goal is (He0fun k Hk).
An
exact proof term for the current goal is
(HF0subP (apply_fun e0 k) HkF0).
We prove the intermediate
claim HF1covers_nonzero:
∀f1 : set, f1 ∈ P → apply_fun f1 y0 ≠ 0 → f1 ∈ F1.
An
exact proof term for the current goal is
(andER (finite F1 ∧ F1 ⊆ P) (∀f1 : set, f1 ∈ P → apply_fun f1 y0 ≠ 0 → f1 ∈ F1) HF1core).
Let k be given.
An exact proof term for the current goal is Heq0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hneq0 Heq0).
We prove the intermediate
claim HkF1:
apply_fun e0 k ∈ F1.
An
exact proof term for the current goal is
(HF1covers_nonzero (apply_fun e0 k) (He0kP k Hk) Hne0).
An exact proof term for the current goal is (HnotF1 HkF1).
We prove the intermediate
claim HF1diff0:
∀f : set, f ∈ F1 → ¬ (f ∈ F0) → apply_fun f y0 = 0.
Let f be given.
We prove the intermediate
claim HfP:
f ∈ P.
An exact proof term for the current goal is (HF1subP f HfF1).
An exact proof term for the current goal is (Hzero_on_N y0 f Hy0N HfP HnotF0).
We prove the intermediate
claim HF0diff1:
∀f : set, f ∈ F0 → ¬ (f ∈ F1) → apply_fun f y0 = 0.
Let f be given.
An exact proof term for the current goal is Heq0.
Apply FalseE to the current goal.
We prove the intermediate
claim HfP:
f ∈ P.
An exact proof term for the current goal is (HF0subP f HfF0).
We prove the intermediate
claim Hne0:
apply_fun f y0 ≠ 0.
An exact proof term for the current goal is (Hneq0 Heq0).
We prove the intermediate
claim HfF1:
f ∈ F1.
An exact proof term for the current goal is (HF1covers_nonzero f HfP Hne0).
An exact proof term for the current goal is (HnotF1 HfF1).
We prove the intermediate
claim Hsum_indep:
weighted_sum y0 n0 e0 = weighted_sum y0 n1 e1.
We prove the intermediate
claim HF1fin:
finite F1.
We prove the intermediate
claim HF1finSub:
finite F1 ∧ F1 ⊆ P.
An
exact proof term for the current goal is
(andEL (finite F1 ∧ F1 ⊆ P) (∀f1 : set, f1 ∈ P → apply_fun f1 y0 ≠ 0 → f1 ∈ F1) HF1core).
An
exact proof term for the current goal is
(andEL (finite F1) (F1 ⊆ P) HF1finSub).
Set FU to be the term
F0 ∪ F1.
We prove the intermediate
claim HFUfin:
finite FU.
An
exact proof term for the current goal is
(binunion_finite F0 HF0fin F1 HF1fin).
We prove the intermediate
claim HexneU:
∃nU eU : set, nU ∈ ω ∧ bijection nU FU eU.
Apply HexneU to the current goal.
Let nU be given.
Apply HexeU to the current goal.
Let eU be given.
We prove the intermediate
claim Hsum0U:
weighted_sum y0 n0 e0 = weighted_sum y0 nU eU.
We prove the intermediate
claim HFUdiff0_zero:
∀f : set, f ∈ FU → ¬ (f ∈ F0) → apply_fun f y0 = 0.
Let f be given.
We prove the intermediate
claim HfCase:
f ∈ F0 ∨ f ∈ F1.
An
exact proof term for the current goal is
(binunionE F0 F1 f HfFU).
Apply (HfCase (apply_fun f y0 = 0)) to the current goal.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HnotF0 HfF0).
An exact proof term for the current goal is (HF1diff0 f HfF1 HnotF0).
We prove the intermediate
claim HeUfun:
function_on eU nU FU.
Let k be given.
We prove the intermediate
claim HkFU:
apply_fun eU k ∈ FU.
An exact proof term for the current goal is (HeUfun k Hk).
An
exact proof term for the current goal is
(HFUdiff0_zero (apply_fun eU k) HkFU HnotF0).
Set D to be the term
FU ∖ F0.
Apply (xm (D = Empty)) to the current goal.
We prove the intermediate
claim HFUsubF0:
FU ⊆ F0.
Let u be given.
Apply (xm (u ∈ F0)) to the current goal.
An exact proof term for the current goal is HuF0.
Apply FalseE to the current goal.
We prove the intermediate
claim HuD:
u ∈ D.
An
exact proof term for the current goal is
(setminusI FU F0 u HuFU HnotF0).
We prove the intermediate
claim HuEmpty:
u ∈ Empty.
rewrite the current goal using HDEmpty (from right to left) at position 1.
An exact proof term for the current goal is HuD.
An
exact proof term for the current goal is
(EmptyE u HuEmpty).
We prove the intermediate
claim HF1subF0:
F1 ⊆ F0.
Let u be given.
We prove the intermediate
claim HuFU:
u ∈ FU.
An
exact proof term for the current goal is
(binunionI2 F0 F1 u HuF1).
An exact proof term for the current goal is (HFUsubF0 u HuFU).
We prove the intermediate
claim HF0subFU:
F0 ⊆ FU.
Let u be given.
An
exact proof term for the current goal is
(binunionI1 F0 F1 u HuF0).
We prove the intermediate
claim HeqFU:
FU = F0.
An exact proof term for the current goal is HFUsubF0.
An exact proof term for the current goal is HF0subFU.
We prove the intermediate
claim HnUO:
nU ∈ ω.
An
exact proof term for the current goal is
(andEL (nU ∈ ω) (bijection nU FU eU) HneU).
We prove the intermediate
claim HbijU:
bijection nU FU eU.
An
exact proof term for the current goal is
(andER (nU ∈ ω) (bijection nU FU eU) HneU).
We prove the intermediate
claim HbijUF0:
bijection nU F0 eU.
rewrite the current goal using HeqFU (from right to left).
An exact proof term for the current goal is HbijU.
We prove the intermediate
claim Heq_n0F0:
equip n0 F0.
We prove the intermediate
claim Heq_nUF0:
equip nU F0.
We prove the intermediate
claim Heq_n0nU:
equip n0 nU.
An
exact proof term for the current goal is
(equip_tra n0 F0 nU Heq_n0F0 (equip_sym nU F0 Heq_nUF0)).
We prove the intermediate
claim HnEq:
n0 = nU.
An
exact proof term for the current goal is
(equip_omega_eq n0 nU Hn0O HnUO Heq_n0nU).
rewrite the current goal using HnEq (from right to left).
We prove the intermediate
claim HbijU0:
bijection n0 F0 eU.
rewrite the current goal using HnEq (from left to right).
An exact proof term for the current goal is HbijUF0.
We prove the intermediate
claim HvalR0:
∀f : set, f ∈ F0 → apply_fun f y0 ∈ R.
Let f be given.
We prove the intermediate
claim HfP:
f ∈ P.
An exact proof term for the current goal is (HF0subP f HfF0).
An exact proof term for the current goal is (HPval_in_R f y0 HfP Hy0X).
We prove the intermediate
claim HcoefR0:
∀f : set, f ∈ F0 → apply_fun coef_of f ∈ R.
Let f be given.
We prove the intermediate
claim HfP:
f ∈ P.
An exact proof term for the current goal is (HF0subP f HfF0).
We prove the intermediate
claim Hpos:
Rlt 0 (apply_fun coef_of f).
An exact proof term for the current goal is (Hcoef_pos f HfP).
An exact proof term for the current goal is (weighted_sum_bijection_indep_real y0 n0 F0 e0 eU Hy0X Hn0O HF0subP HvalR0 HcoefR0 Hbij0 HbijU0).
We prove the intermediate
claim HDnon:
D ≠ Empty.
An exact proof term for the current goal is (HDne Heq).
We prove the intermediate
claim Hexf:
∃f : set, f ∈ D.
Apply Hexf to the current goal.
Let f be given.
We prove the intermediate
claim HfFU:
f ∈ FU.
An
exact proof term for the current goal is
(setminusE1 FU F0 f HfD).
We prove the intermediate
claim HfnotF0:
¬ (f ∈ F0).
An
exact proof term for the current goal is
(setminusE2 FU F0 f HfD).
We prove the intermediate
claim Hfy0:
apply_fun f y0 = 0.
An exact proof term for the current goal is (HFUdiff0_zero f HfFU HfnotF0).
We prove the intermediate
claim HnUO:
nU ∈ ω.
An
exact proof term for the current goal is
(andEL (nU ∈ ω) (bijection nU FU eU) HneU).
We prove the intermediate
claim HbijU:
bijection nU FU eU.
An
exact proof term for the current goal is
(andER (nU ∈ ω) (bijection nU FU eU) HneU).
We prove the intermediate
claim HnUNat:
nat_p nU.
An
exact proof term for the current goal is
(omega_nat_p nU HnUO).
An
exact proof term for the current goal is
(nat_inv nU HnUNat).
Apply (HnUcase (weighted_sum y0 n0 e0 = weighted_sum y0 nU eU)) to the current goal.
Apply FalseE to the current goal.
We prove the intermediate
claim Hbij0:
bijection 0 FU eU.
rewrite the current goal using HnU0 (from right to left).
An exact proof term for the current goal is HbijU.
We prove the intermediate
claim Hexk:
∃k : set, k ∈ 0 ∧ apply_fun eU k = f.
An
exact proof term for the current goal is
(bijection_surj 0 FU eU f Hbij0 HfFU).
Apply Hexk to the current goal.
Let k be given.
Assume Hkpair.
We prove the intermediate
claim Hk0:
k ∈ 0.
An
exact proof term for the current goal is
(andEL (k ∈ 0) (apply_fun eU k = f) Hkpair).
An
exact proof term for the current goal is
(EmptyE k Hk0).
Apply Hexm to the current goal.
Let m be given.
We prove the intermediate
claim HmNat:
nat_p m.
We prove the intermediate
claim HnUEq:
nU = ordsucc m.
We prove the intermediate
claim HmO:
m ∈ ω.
An
exact proof term for the current goal is
(nat_p_omega m HmNat).
We prove the intermediate
claim HF0subFU:
F0 ⊆ FU.
Let u be given.
An
exact proof term for the current goal is
(binunionI1 F0 F1 u Hu).
We prove the intermediate
claim HFUsubP:
FU ⊆ P.
Let u be given.
Apply (binunionE F0 F1 u Hu) to the current goal.
An exact proof term for the current goal is (HF0subP u Hu0).
An exact proof term for the current goal is (HF1subP u Hu1).
We prove the intermediate
claim HvalFU:
∀g : set, g ∈ FU → apply_fun g y0 ∈ R.
Let g be given.
We prove the intermediate
claim HgP:
g ∈ P.
An exact proof term for the current goal is (HFUsubP g HgFU).
An exact proof term for the current goal is (HPval_in_R g y0 HgP Hy0X).
We prove the intermediate
claim HcoefFU:
∀g : set, g ∈ FU → apply_fun coef_of g ∈ R.
Let g be given.
We prove the intermediate
claim HgP:
g ∈ P.
An exact proof term for the current goal is (HFUsubP g HgFU).
We prove the intermediate
claim Hpos:
Rlt 0 (apply_fun coef_of g).
An exact proof term for the current goal is (Hcoef_pos g HgP).
rewrite the current goal using HnUEq (from right to left).
An exact proof term for the current goal is HbijU.
We prove the intermediate
claim Hremove:
∃eU' : set, bijection m (FU ∖ {f}) eU' ∧ weighted_sum y0 (ordsucc m) eU = weighted_sum y0 m eU'.
An exact proof term for the current goal is (weighted_sum_bijection_remove_one_zero_real y0 m FU eU f Hy0X HmO HFUsubP HvalFU HcoefFU HbijU2 HfFU Hfy0).
Apply Hremove to the current goal.
Let eU' be given.
Assume HeU'pack.
We prove the intermediate
claim HwsU:
weighted_sum y0 (ordsucc m) eU = weighted_sum y0 m eU'.
An
exact proof term for the current goal is
(andER (bijection m (FU ∖ {f}) eU') (weighted_sum y0 (ordsucc m) eU = weighted_sum y0 m eU') HeU'pack).
We prove the intermediate
claim Hrec:
weighted_sum y0 n0 e0 = weighted_sum y0 m eU'.
We prove the intermediate
claim HbijU':
bijection m (FU ∖ {f}) eU'.
An
exact proof term for the current goal is
(andEL (bijection m (FU ∖ {f}) eU') (weighted_sum y0 (ordsucc m) eU = weighted_sum y0 m eU') HeU'pack).
We prove the intermediate
claim HFminsub:
(FU ∖ {f}) ⊆ FU.
We prove the intermediate
claim HFminfin:
finite (FU ∖ {f}).
An
exact proof term for the current goal is
(Subq_finite FU HFUfin (FU ∖ {f}) HFminsub).
We prove the intermediate
claim HFminsubP:
(FU ∖ {f}) ⊆ P.
An
exact proof term for the current goal is
(Subq_tra (FU ∖ {f}) FU P HFminsub HFUsubP).
We prove the intermediate
claim HF0subFmin:
F0 ⊆ (FU ∖ {f}).
Let u be given.
We prove the intermediate
claim HuFU:
u ∈ FU.
An exact proof term for the current goal is (HF0subFU u HuF0).
We prove the intermediate
claim HuNot:
u ∉ {f}.
We prove the intermediate
claim HuEqF:
u = f.
An
exact proof term for the current goal is
(SingE f u HuEq).
Apply HfnotF0 to the current goal.
rewrite the current goal using HuEqF (from right to left).
An exact proof term for the current goal is HuF0.
An
exact proof term for the current goal is
(setminusI FU {f} u HuFU HuNot).
We prove the intermediate
claim HvalR0:
∀g : set, g ∈ F0 → apply_fun g y0 ∈ R.
Let g be given.
We prove the intermediate
claim HgP:
g ∈ P.
An exact proof term for the current goal is (HF0subP g HgF0).
An exact proof term for the current goal is (HPval_in_R g y0 HgP Hy0X).
We prove the intermediate
claim HcoefR0:
∀g : set, g ∈ F0 → apply_fun coef_of g ∈ R.
Let g be given.
We prove the intermediate
claim HgP:
g ∈ P.
An exact proof term for the current goal is (HF0subP g HgF0).
We prove the intermediate
claim Hpos:
Rlt 0 (apply_fun coef_of g).
An exact proof term for the current goal is (Hcoef_pos g HgP).
We prove the intermediate
claim HzeroOut:
∀g : set, g ∈ (FU ∖ {f}) → ¬ (g ∈ F0) → apply_fun g y0 = 0.
Let g be given.
We prove the intermediate
claim HgFU:
g ∈ FU.
An
exact proof term for the current goal is
(setminusE1 FU {f} g HgF).
An exact proof term for the current goal is (HFUdiff0_zero g HgFU HgNot0).
An
exact proof term for the current goal is
(weighted_sum_bijection_zero_outside_real y0 n0 F0 e0 m (FU ∖ {f}) eU' Hy0X Hn0O HFminfin HF0subFmin HFminsubP HF0subP HvalR0 HcoefR0 HzeroOut Hbij0 HmO HbijU').
rewrite the current goal using HnUEq (from left to right).
rewrite the current goal using HwsU (from left to right).
An exact proof term for the current goal is Hrec.
We prove the intermediate
claim Hsum1U:
weighted_sum y0 n1 e1 = weighted_sum y0 nU eU.
We prove the intermediate
claim HFUdiff1_zero:
∀f : set, f ∈ FU → ¬ (f ∈ F1) → apply_fun f y0 = 0.
Let f be given.
We prove the intermediate
claim HfCase:
f ∈ F0 ∨ f ∈ F1.
An
exact proof term for the current goal is
(binunionE F0 F1 f HfFU).
Apply (HfCase (apply_fun f y0 = 0)) to the current goal.
An exact proof term for the current goal is (HF0diff1 f HfF0 HnotF1).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HnotF1 HfF1).
We prove the intermediate
claim HeUfun:
function_on eU nU FU.
Let k be given.
We prove the intermediate
claim HkFU:
apply_fun eU k ∈ FU.
An exact proof term for the current goal is (HeUfun k Hk).
An
exact proof term for the current goal is
(HFUdiff1_zero (apply_fun eU k) HkFU HnotF1).
Set D to be the term
FU ∖ F1.
Apply (xm (D = Empty)) to the current goal.
We prove the intermediate
claim HFUsubF1:
FU ⊆ F1.
Let u be given.
Apply (xm (u ∈ F1)) to the current goal.
An exact proof term for the current goal is HuF1.
Apply FalseE to the current goal.
We prove the intermediate
claim HuD:
u ∈ D.
An
exact proof term for the current goal is
(setminusI FU F1 u HuFU HnotF1).
We prove the intermediate
claim HuEmpty:
u ∈ Empty.
rewrite the current goal using HDEmpty (from right to left) at position 1.
An exact proof term for the current goal is HuD.
An
exact proof term for the current goal is
(EmptyE u HuEmpty).
We prove the intermediate
claim HF0subF1:
F0 ⊆ F1.
Let u be given.
We prove the intermediate
claim HuFU:
u ∈ FU.
An
exact proof term for the current goal is
(binunionI1 F0 F1 u HuF0).
An exact proof term for the current goal is (HFUsubF1 u HuFU).
We prove the intermediate
claim HF1subFU:
F1 ⊆ FU.
Let u be given.
An
exact proof term for the current goal is
(binunionI2 F0 F1 u HuF1).
We prove the intermediate
claim HeqFU:
FU = F1.
An exact proof term for the current goal is HFUsubF1.
An exact proof term for the current goal is HF1subFU.
We prove the intermediate
claim HnUO:
nU ∈ ω.
An
exact proof term for the current goal is
(andEL (nU ∈ ω) (bijection nU FU eU) HneU).
We prove the intermediate
claim HbijU:
bijection nU FU eU.
An
exact proof term for the current goal is
(andER (nU ∈ ω) (bijection nU FU eU) HneU).
We prove the intermediate
claim HbijUF1:
bijection nU F1 eU.
rewrite the current goal using HeqFU (from right to left).
An exact proof term for the current goal is HbijU.
We prove the intermediate
claim Heq_n1F1:
equip n1 F1.
We prove the intermediate
claim Heq_nUF1:
equip nU F1.
We prove the intermediate
claim Heq_n1nU:
equip n1 nU.
An
exact proof term for the current goal is
(equip_tra n1 F1 nU Heq_n1F1 (equip_sym nU F1 Heq_nUF1)).
We prove the intermediate
claim HnEq:
n1 = nU.
An
exact proof term for the current goal is
(equip_omega_eq n1 nU Hn1O HnUO Heq_n1nU).
rewrite the current goal using HnEq (from right to left).
We prove the intermediate
claim HbijU1:
bijection n1 F1 eU.
rewrite the current goal using HnEq (from left to right).
An exact proof term for the current goal is HbijUF1.
We prove the intermediate
claim HvalR1:
∀f : set, f ∈ F1 → apply_fun f y0 ∈ R.
Let f be given.
We prove the intermediate
claim HfP:
f ∈ P.
An exact proof term for the current goal is (HF1subP f HfF1).
An exact proof term for the current goal is (HPval_in_R f y0 HfP Hy0X).
We prove the intermediate
claim HcoefR1:
∀f : set, f ∈ F1 → apply_fun coef_of f ∈ R.
Let f be given.
We prove the intermediate
claim HfP:
f ∈ P.
An exact proof term for the current goal is (HF1subP f HfF1).
We prove the intermediate
claim Hpos:
Rlt 0 (apply_fun coef_of f).
An exact proof term for the current goal is (Hcoef_pos f HfP).
An exact proof term for the current goal is (weighted_sum_bijection_indep_real y0 n1 F1 e1 eU Hy0X Hn1O HF1subP HvalR1 HcoefR1 He1bij HbijU1).
We prove the intermediate
claim HDnon:
D ≠ Empty.
An exact proof term for the current goal is (HDne Heq).
We prove the intermediate
claim Hexf:
∃f : set, f ∈ D.
Apply Hexf to the current goal.
Let f be given.
We prove the intermediate
claim HfFU:
f ∈ FU.
An
exact proof term for the current goal is
(setminusE1 FU F1 f HfD).
We prove the intermediate
claim HfnotF1:
¬ (f ∈ F1).
An
exact proof term for the current goal is
(setminusE2 FU F1 f HfD).
We prove the intermediate
claim Hfy0:
apply_fun f y0 = 0.
An exact proof term for the current goal is (HFUdiff1_zero f HfFU HfnotF1).
We prove the intermediate
claim HnUO:
nU ∈ ω.
An
exact proof term for the current goal is
(andEL (nU ∈ ω) (bijection nU FU eU) HneU).
We prove the intermediate
claim HbijU:
bijection nU FU eU.
An
exact proof term for the current goal is
(andER (nU ∈ ω) (bijection nU FU eU) HneU).
We prove the intermediate
claim HnUNat:
nat_p nU.
An
exact proof term for the current goal is
(omega_nat_p nU HnUO).
An
exact proof term for the current goal is
(nat_inv nU HnUNat).
Apply (HnUcase (weighted_sum y0 n1 e1 = weighted_sum y0 nU eU)) to the current goal.
Apply FalseE to the current goal.
We prove the intermediate
claim Hbij0:
bijection 0 FU eU.
rewrite the current goal using HnU0 (from right to left).
An exact proof term for the current goal is HbijU.
We prove the intermediate
claim Hexk:
∃k : set, k ∈ 0 ∧ apply_fun eU k = f.
An
exact proof term for the current goal is
(bijection_surj 0 FU eU f Hbij0 HfFU).
Apply Hexk to the current goal.
Let k be given.
Assume Hkpair.
We prove the intermediate
claim Hk0:
k ∈ 0.
An
exact proof term for the current goal is
(andEL (k ∈ 0) (apply_fun eU k = f) Hkpair).
An
exact proof term for the current goal is
(EmptyE k Hk0).
Apply Hexm to the current goal.
Let m be given.
We prove the intermediate
claim HmNat:
nat_p m.
We prove the intermediate
claim HnUEq:
nU = ordsucc m.
We prove the intermediate
claim HmO:
m ∈ ω.
An
exact proof term for the current goal is
(nat_p_omega m HmNat).
We prove the intermediate
claim HF1subFU:
F1 ⊆ FU.
Let u be given.
An
exact proof term for the current goal is
(binunionI2 F0 F1 u Hu).
We prove the intermediate
claim HFUsubP:
FU ⊆ P.
Let u be given.
Apply (binunionE F0 F1 u Hu) to the current goal.
An exact proof term for the current goal is (HF0subP u Hu0).
An exact proof term for the current goal is (HF1subP u Hu1).
We prove the intermediate
claim HvalFU:
∀g : set, g ∈ FU → apply_fun g y0 ∈ R.
Let g be given.
We prove the intermediate
claim HgP:
g ∈ P.
An exact proof term for the current goal is (HFUsubP g HgFU).
An exact proof term for the current goal is (HPval_in_R g y0 HgP Hy0X).
We prove the intermediate
claim HcoefFU:
∀g : set, g ∈ FU → apply_fun coef_of g ∈ R.
Let g be given.
We prove the intermediate
claim HgP:
g ∈ P.
An exact proof term for the current goal is (HFUsubP g HgFU).
We prove the intermediate
claim Hpos:
Rlt 0 (apply_fun coef_of g).
An exact proof term for the current goal is (Hcoef_pos g HgP).
rewrite the current goal using HnUEq (from right to left).
An exact proof term for the current goal is HbijU.
We prove the intermediate
claim Hremove:
∃eU' : set, bijection m (FU ∖ {f}) eU' ∧ weighted_sum y0 (ordsucc m) eU = weighted_sum y0 m eU'.
An exact proof term for the current goal is (weighted_sum_bijection_remove_one_zero_real y0 m FU eU f Hy0X HmO HFUsubP HvalFU HcoefFU HbijU2 HfFU Hfy0).
Apply Hremove to the current goal.
Let eU' be given.
Assume HeU'pack.
We prove the intermediate
claim HwsU:
weighted_sum y0 (ordsucc m) eU = weighted_sum y0 m eU'.
An
exact proof term for the current goal is
(andER (bijection m (FU ∖ {f}) eU') (weighted_sum y0 (ordsucc m) eU = weighted_sum y0 m eU') HeU'pack).
We prove the intermediate
claim Hrec:
weighted_sum y0 n1 e1 = weighted_sum y0 m eU'.
We prove the intermediate
claim HbijU':
bijection m (FU ∖ {f}) eU'.
An
exact proof term for the current goal is
(andEL (bijection m (FU ∖ {f}) eU') (weighted_sum y0 (ordsucc m) eU = weighted_sum y0 m eU') HeU'pack).
We prove the intermediate
claim HFminsub:
(FU ∖ {f}) ⊆ FU.
We prove the intermediate
claim HFminfin:
finite (FU ∖ {f}).
An
exact proof term for the current goal is
(Subq_finite FU HFUfin (FU ∖ {f}) HFminsub).
We prove the intermediate
claim HFminsubP:
(FU ∖ {f}) ⊆ P.
An
exact proof term for the current goal is
(Subq_tra (FU ∖ {f}) FU P HFminsub HFUsubP).
We prove the intermediate
claim HF1subFU:
F1 ⊆ FU.
Let u be given.
An
exact proof term for the current goal is
(binunionI2 F0 F1 u HuF1).
We prove the intermediate
claim HF1subFmin:
F1 ⊆ (FU ∖ {f}).
Let u be given.
We prove the intermediate
claim HuFU:
u ∈ FU.
An exact proof term for the current goal is (HF1subFU u HuF1).
We prove the intermediate
claim HuNot:
u ∉ {f}.
We prove the intermediate
claim HuEqF:
u = f.
An
exact proof term for the current goal is
(SingE f u HuEq).
Apply HfnotF1 to the current goal.
rewrite the current goal using HuEqF (from right to left).
An exact proof term for the current goal is HuF1.
An
exact proof term for the current goal is
(setminusI FU {f} u HuFU HuNot).
We prove the intermediate
claim HvalR1:
∀g : set, g ∈ F1 → apply_fun g y0 ∈ R.
Let g be given.
We prove the intermediate
claim HgP:
g ∈ P.
An exact proof term for the current goal is (HF1subP g HgF1).
An exact proof term for the current goal is (HPval_in_R g y0 HgP Hy0X).
We prove the intermediate
claim HcoefR1:
∀g : set, g ∈ F1 → apply_fun coef_of g ∈ R.
Let g be given.
We prove the intermediate
claim HgP:
g ∈ P.
An exact proof term for the current goal is (HF1subP g HgF1).
We prove the intermediate
claim Hpos:
Rlt 0 (apply_fun coef_of g).
An exact proof term for the current goal is (Hcoef_pos g HgP).
We prove the intermediate
claim HzeroOut:
∀g : set, g ∈ (FU ∖ {f}) → ¬ (g ∈ F1) → apply_fun g y0 = 0.
Let g be given.
We prove the intermediate
claim HgFU:
g ∈ FU.
An
exact proof term for the current goal is
(setminusE1 FU {f} g HgF).
An exact proof term for the current goal is (HFUdiff1_zero g HgFU HgNot1).
An
exact proof term for the current goal is
(weighted_sum_bijection_zero_outside_real y0 n1 F1 e1 m (FU ∖ {f}) eU' Hy0X Hn1O HFminfin HF1subFmin HFminsubP HF1subP HvalR1 HcoefR1 HzeroOut He1bij HmO HbijU').
rewrite the current goal using HnUEq (from left to right).
rewrite the current goal using HwsU (from left to right).
An exact proof term for the current goal is Hrec.
rewrite the current goal using Hsum0U (from left to right).
rewrite the current goal using Hsum1U (from right to left).
Use reflexivity.
An exact proof term for the current goal is Hsum_indep.
An exact proof term for the current goal is (Hlocal_rule f Hlocal).
An exact proof term for the current goal is Hf_cont.
Let x be given.
An exact proof term for the current goal is (HfPos x HxX).
An exact proof term for the current goal is HfLe.
∎