---

Step * 2 1 2 1 1 1 1 1 1 1 2 2 of Lemma fan-bar-sep


1. T : Type
2. t : T
3. size : ℕ
4. T ~ ℕsize
5. A : n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹
6. B : n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹
7. jbar(A;B)
8. k : ℕ
9. ℕ(k ÷ 2) + 1 ⟶ T ~ ℕsize^((k ÷ 2) + 1)
10. f1 : ℕ(k ÷ 2) + 1 ⟶ T
11. ¬(∃n:ℕ(k ÷ 2) + 1. (↑(A n f1)))
12. f : ℕ(k ÷ 2) + 1 ⟶ T
13. n : ℕk
14. i : ℕn ÷ 2
15. ↑(B i 
      (λk@0.if ((2 * k@0) + 1 rem 2 =z 0)
              then if ((2 * k@0) + 1) ÷ 2 <z (k ÷ 2) + 1 then f1 (((2 * k@0) + 1) ÷ 2) else t fi 
            if ((2 * k@0) + 1) ÷ 2 <z (k ÷ 2) + 1 then f (((2 * k@0) + 1) ÷ 2)
            else t
            fi ))
⊢ ↑(B i f)
BY
{ ((Subst' (λk@0.if ((2 * k@0) + 1 rem 2 =z 0)
                   then if ((2 * k@0) + 1) ÷ 2 <z (k ÷ 2) + 1 then f1 (((2 * k@0) + 1) ÷ 2) else t fi 
                 if ((2 * k@0) + 1) ÷ 2 <z (k ÷ 2) + 1 then f (((2 * k@0) + 1) ÷ 2)
                 else t
                 fi )
    = f
    ∈ (ℕi ⟶ T) -1
    THENW Auto
    )
   THEN Try (Trivial)
   THEN (FunExt THENW Auto)
   THEN Reduce 0
   THEN ((Subst' (2 * x) + 1 rem 2 ~ 1 0 THENA Auto) THEN (Subst' ((2 * x) + 1) ÷ 2 ~ x 0 THENA Auto))
   THEN Reduce 0) }

1
1. T : Type
2. t : T
3. size : ℕ
4. T ~ ℕsize
5. A : n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹
6. B : n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹
7. jbar(A;B)
8. k : ℕ
9. ℕ(k ÷ 2) + 1 ⟶ T ~ ℕsize^((k ÷ 2) + 1)
10. f1 : ℕ(k ÷ 2) + 1 ⟶ T
11. ¬(∃n:ℕ(k ÷ 2) + 1. (↑(A n f1)))
12. f : ℕ(k ÷ 2) + 1 ⟶ T
13. n : ℕk
14. i : ℕn ÷ 2
15. ↑(B i 
      (λk@0.if ((2 * k@0) + 1 rem 2 =z 0)
              then if ((2 * k@0) + 1) ÷ 2 <z (k ÷ 2) + 1 then f1 (((2 * k@0) + 1) ÷ 2) else t fi 
            if ((2 * k@0) + 1) ÷ 2 <z (k ÷ 2) + 1 then f (((2 * k@0) + 1) ÷ 2)
            else t
            fi ))
16. x : ℕi
⊢ ((2 * x) + 1 rem 2) = 1 ∈ ℤ

2
1. T : Type
2. t : T
3. size : ℕ
4. T ~ ℕsize
5. A : n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹
6. B : n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹
7. jbar(A;B)
8. k : ℕ
9. ℕ(k ÷ 2) + 1 ⟶ T ~ ℕsize^((k ÷ 2) + 1)
10. f1 : ℕ(k ÷ 2) + 1 ⟶ T
11. ¬(∃n:ℕ(k ÷ 2) + 1. (↑(A n f1)))
12. f : ℕ(k ÷ 2) + 1 ⟶ T
13. n : ℕk
14. i : ℕn ÷ 2
15. ↑(B i 
      (λk@0.if ((2 * k@0) + 1 rem 2 =z 0)
              then if ((2 * k@0) + 1) ÷ 2 <z (k ÷ 2) + 1 then f1 (((2 * k@0) + 1) ÷ 2) else t fi 
            if ((2 * k@0) + 1) ÷ 2 <z (k ÷ 2) + 1 then f (((2 * k@0) + 1) ÷ 2)
            else t
            fi ))
16. x : ℕi
⊢ if x <z (k ÷ 2) + 1 then f x else t fi  = (f x) ∈ T

---

Latex:

---

Latex:

1.  T  :  Type
2.  t  :  T
3.  size  :  \mBbbN{}
4.  T  \msim{}  \mBbbN{}size
5.  A  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbB{}
6.  B  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbB{}
7.  jbar(A;B)
8.  k  :  \mBbbN{}
9.  \mBbbN{}(k  \mdiv{}  2)  +  1  {}\mrightarrow{}  T  \msim{}  \mBbbN{}size\^{}((k  \mdiv{}  2)  +  1)
10.  f1  :  \mBbbN{}(k  \mdiv{}  2)  +  1  {}\mrightarrow{}  T
11.  \mneg{}(\mexists{}n:\mBbbN{}(k  \mdiv{}  2)  +  1.  (\muparrow{}(A  n  f1)))
12.  f  :  \mBbbN{}(k  \mdiv{}  2)  +  1  {}\mrightarrow{}  T
13.  n  :  \mBbbN{}k
14.  i  :  \mBbbN{}n  \mdiv{}  2
15.  \muparrow{}(B  i 
            (\mlambda{}k@0.if  ((2  *  k@0)  +  1  rem  2  =\msubz{}  0)
                            then  if  ((2  *  k@0)  +  1)  \mdiv{}  2  <z  (k  \mdiv{}  2)  +  1  then  f1  (((2  *  k@0)  +  1)  \mdiv{}  2)  else  t  fi 
                        if  ((2  *  k@0)  +  1)  \mdiv{}  2  <z  (k  \mdiv{}  2)  +  1  then  f  (((2  *  k@0)  +  1)  \mdiv{}  2)
                        else  t
                        fi  ))
\mvdash{}  \muparrow{}(B  i  f)


By

---

Latex:
((Subst'  (\mlambda{}k@0.if  ((2  *  k@0)  +  1  rem  2  =\msubz{}  0)
                                  then  if  ((2  *  k@0)  +  1)  \mdiv{}  2  <z  (k  \mdiv{}  2)  +  1  then  f1  (((2  *  k@0)  +  1)  \mdiv{}  2)  else  t  fi 
                              if  ((2  *  k@0)  +  1)  \mdiv{}  2  <z  (k  \mdiv{}  2)  +  1  then  f  (((2  *  k@0)  +  1)  \mdiv{}  2)
                              else  t
                              fi  )
    =  f  -1
    THENW  Auto
    )
  THEN  Try  (Trivial)
  THEN  (FunExt  THENW  Auto)
  THEN  Reduce  0
  THEN  ((Subst'  (2  *  x)  +  1  rem  2  \msim{}  1  0  THENA  Auto)  THEN  (Subst'  ((2  *  x)  +  1)  \mdiv{}  2  \msim{}  x  0  THENA  Auto))
  THEN  Reduce  0)

---

Home Index