Step
*
2
2
2
of Lemma
odd-lsum-of-odd
1. T : Type
2. n : ℕ
3. u : T
4. u1 : T
5. u2 : T
6. v : T List
7. ∀L1:T List
(||L1|| < ||[u; u1; [u2 / v]]||
⇒ ∀[f:{x:T| (x ∈ L1)} ⟶ ℤ]. ↑isOdd(Σ(f[x] | x ∈ L1)) supposing (∀x∈L1.↑isOdd(f[x])) supposing ↑isOdd(||L1||))
8. ↑isOdd(||[u; u1; [u2 / v]]||)
9. f : {x:T| (x ∈ [u; u1; [u2 / v]])} ⟶ ℤ
10. (∀x∈[u; u1; [u2 / v]].↑isOdd(f[x]))
⊢ ↑isOdd(Σ(f[x] | x ∈ [u; u1; [u2 / v]]))
BY
{ (InstHyp [⌜[u2 / v]⌝;⌜f⌝] 7⋅
THENA (Auto
THEN Try (((D 0 THENA Auto)
THEN D -2 With ⌜i + 2⌝
THEN Auto
THEN (Subst' i + 2 ~ (i + 1) + 1 -1 THENA Auto)
THEN RWW "select_cons_tl_sq2" (-1)
THEN Auto))
)
) }
1
1. T : Type
2. n : ℕ
3. u : T
4. u1 : T
5. u2 : T
6. v : T List
7. ∀L1:T List
(||L1|| < ||[u; u1; [u2 / v]]||
⇒ ∀[f:{x:T| (x ∈ L1)} ⟶ ℤ]. ↑isOdd(Σ(f[x] | x ∈ L1)) supposing (∀x∈L1.↑isOdd(f[x])) supposing ↑isOdd(||L1||))
8. ↑isOdd(||[u; u1; [u2 / v]]||)
9. f : {x:T| (x ∈ [u; u1; [u2 / v]])} ⟶ ℤ
10. (∀x∈[u; u1; [u2 / v]].↑isOdd(f[x]))
⊢ ↑isOdd(||v|| + 1)
2
1. T : Type
2. n : ℕ
3. u : T
4. u1 : T
5. u2 : T
6. v : T List
7. ∀L1:T List
(||L1|| < ||[u; u1; [u2 / v]]||
⇒ ∀[f:{x:T| (x ∈ L1)} ⟶ ℤ]. ↑isOdd(Σ(f[x] | x ∈ L1)) supposing (∀x∈L1.↑isOdd(f[x])) supposing ↑isOdd(||L1||))
8. ↑isOdd(||[u; u1; [u2 / v]]||)
9. f : {x:T| (x ∈ [u; u1; [u2 / v]])} ⟶ ℤ
10. (∀x∈[u; u1; [u2 / v]].↑isOdd(f[x]))
11. ↑isOdd(Σ(f[x] | x ∈ [u2 / v]))
⊢ ↑isOdd(Σ(f[x] | x ∈ [u; u1; [u2 / v]]))
Latex:
Latex:
1. T : Type
2. n : \mBbbN{}
3. u : T
4. u1 : T
5. u2 : T
6. v : T List
7. \mforall{}L1:T List
(||L1|| < ||[u; u1; [u2 / v]]||
{}\mRightarrow{} \mforall{}[f:\{x:T| (x \mmember{} L1)\} {}\mrightarrow{} \mBbbZ{}]. \muparrow{}isOdd(\mSigma{}(f[x] | x \mmember{} L1)) supposing (\mforall{}x\mmember{}L1.\muparrow{}isOdd(f[x]))
supposing \muparrow{}isOdd(||L1||))
8. \muparrow{}isOdd(||[u; u1; [u2 / v]]||)
9. f : \{x:T| (x \mmember{} [u; u1; [u2 / v]])\} {}\mrightarrow{} \mBbbZ{}
10. (\mforall{}x\mmember{}[u; u1; [u2 / v]].\muparrow{}isOdd(f[x]))
\mvdash{} \muparrow{}isOdd(\mSigma{}(f[x] | x \mmember{} [u; u1; [u2 / v]]))
By
Latex:
(InstHyp [\mkleeneopen{}[u2 / v]\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}] 7\mcdot{}
THENA (Auto
THEN Try (((D 0 THENA Auto)
THEN D -2 With \mkleeneopen{}i + 2\mkleeneclose{}
THEN Auto
THEN (Subst' i + 2 \msim{} (i + 1) + 1 -1 THENA Auto)
THEN RWW "select\_cons\_tl\_sq2" (-1)
THEN Auto))
)
)
Home
Index