---

Step * 1 of Lemma fan-implies-PFan


1. Fan
⊢ PFan{i:l}()
BY
{ (D 0
   THEN (Auto
         THEN Unfold `fan` 1
         THEN InstHyp [⌜λa.(((2 * n) ≤ ||a||) ∧ (∀i:ℕn. ((¬a[2 * i] = a[(2 * i) + 1]) ⇒ (ss unshuffle(a)))))⌝] 1⋅)
   THEN TACTIC:(All Reduce THEN UnivCD THEN Try (Complete (Auto)))) }

1
1. ∀A:(𝔹 List) ⟶ ℙ
     ((∀as:𝔹 List. Dec(A as)) ⇒ (∀f:ℕ ⟶ 𝔹. ∃n:ℕ. (A map(f;upto(n)))) ⇒ (∃k:ℕ. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. (A map(f;upto(n)))))
2. n : ℕ@i
3. ss : ((𝔹 × 𝔹) List) ⟶ ℙ@i'
4. ∀bc:(𝔹 × 𝔹) List. Dec(ss bc)
5. ∀bc,bc':(𝔹 × 𝔹) List.  (bc ≤ bc' ⇒ (ss bc) ⇒ (ss bc'))
6. ∀gh:ℕ ⟶ (𝔹 × 𝔹)
     ((¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List))) ⇒ (∃m:ℕ. (ss map(gh;upto(m)))))
7. f : ℕ ⟶ 𝔹@i
⊢ ∃n@0:ℕ
   (((2 * n) ≤ ||map(f;upto(n@0))||)
   ∧ (∀i:ℕn. ((¬map(f;upto(n@0))[2 * i] = map(f;upto(n@0))[(2 * i) + 1]) ⇒ (ss unshuffle(map(f;upto(n@0)))))))

2
1. ∀A:(𝔹 List) ⟶ ℙ
     ((∀as:𝔹 List. Dec(A as)) ⇒ (∀f:ℕ ⟶ 𝔹. ∃n:ℕ. (A map(f;upto(n)))) ⇒ (∃k:ℕ. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. (A map(f;upto(n)))))
2. n : ℕ@i
3. ss : ((𝔹 × 𝔹) List) ⟶ ℙ@i'
4. ∀bc:(𝔹 × 𝔹) List. Dec(ss bc)
5. ∀bc,bc':(𝔹 × 𝔹) List.  (bc ≤ bc' ⇒ (ss bc) ⇒ (ss bc'))
6. ∀gh:ℕ ⟶ (𝔹 × 𝔹)
     ((¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List))) ⇒ (∃m:ℕ. (ss map(gh;upto(m)))))
7. ∃k:ℕ
    ∀f:ℕ ⟶ 𝔹
      ∃n@0:ℕk
       (((2 * n) ≤ ||map(f;upto(n@0))||)
       ∧ (∀i:ℕn. ((¬map(f;upto(n@0))[2 * i] = map(f;upto(n@0))[(2 * i) + 1]) ⇒ (ss unshuffle(map(f;upto(n@0)))))))
⊢ ∃k:ℕ
   ∀gh:ℕ ⟶ (𝔹 × 𝔹)
     ((¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List))) ⇒ (ss map(gh;upto(k))))

---

Latex:

---

Latex:

1.  Fan
\mvdash{}  PFan\{i:l\}()


By

---

Latex:
(D  0
  THEN  (Auto
              THEN  Unfold  `fan`  1
              THEN  InstHyp  [\mkleeneopen{}\mlambda{}a.(((2  *  n)  \mleq{}  ||a||)
                                                  \mwedge{}  (\mforall{}i:\mBbbN{}n.  ((\mneg{}a[2  *  i]  =  a[(2  *  i)  +  1])  {}\mRightarrow{}  (ss  unshuffle(a)))))\mkleeneclose{}]  1\mcdot{})
  THEN  TACTIC:(All  Reduce  THEN  UnivCD  THEN  Try  (Complete  (Auto))))

---

Home Index