---

Step * 1 of Lemma l-first_wf

.....wf..... 
1. T : Type
2. f : T ⟶ 𝔹
3. u : T
4. ¬↑f[u]
5. v : T List
6. rec-case(v) of
   [] => inr (λx.Ax) 
   x::xs =>
    r.if f[x] then inl x else r fi  ∈ (∃x:{T| ((x ∈ v) ∧ (↑f[x]))}) ∨ (∀x∈v.¬↑f[x])
7. rec-case(v) of
   [] => inr (λx.Ax) 
   h::t =>
    r.if f[h] then inl h else r fi 
= rec-case(v) of
  [] => inr (λx.Ax) 
  h::t =>
   r.if f[h] then inl h else r fi 
∈ ((∃x:{T| ((x ∈ v) ∧ (↑f[x]))}) ∨ (∀x∈v.¬↑f[x]))
8. x : ∃x:{T| ((x ∈ v) ∧ (↑f[x]))} + (∀x∈v.¬↑f[x])
⊢ x ∈ ∃x:{T| ((x ∈ [u / v]) ∧ (↑f[x]))} + (∀x∈[u / v].¬↑f[x])
BY
{ (D -1 THEN Auto) }

1
1. T : Type
2. f : T ⟶ 𝔹
3. u : T
4. ¬↑f[u]
5. v : T List
6. rec-case(v) of
   [] => inr (λx.Ax) 
   x::xs =>
    r.if f[x] then inl x else r fi  ∈ (∃x:{T| ((x ∈ v) ∧ (↑f[x]))}) ∨ (∀x∈v.¬↑f[x])
7. rec-case(v) of
   [] => inr (λx.Ax) 
   h::t =>
    r.if f[h] then inl h else r fi 
= rec-case(v) of
  [] => inr (λx.Ax) 
  h::t =>
   r.if f[h] then inl h else r fi 
∈ ((∃x:{T| ((x ∈ v) ∧ (↑f[x]))}) ∨ (∀x∈v.¬↑f[x]))
8. y : (∀x∈v.¬↑f[x])
⊢ y ∈ (∀x∈[u / v].¬↑f[x])

---

Latex:

---

Latex:
.....wf..... 
1.  T  :  Type
2.  f  :  T  {}\mrightarrow{}  \mBbbB{}
3.  u  :  T
4.  \mneg{}\muparrow{}f[u]
5.  v  :  T  List
6.  rec-case(v)  of
      []  =>  inr  (\mlambda{}x.Ax) 
      x::xs  =>
        r.if  f[x]  then  inl  x  else  r  fi    \mmember{}  (\mexists{}x:\{T|  ((x  \mmember{}  v)  \mwedge{}  (\muparrow{}f[x]))\})  \mvee{}  (\mforall{}x\mmember{}v.\mneg{}\muparrow{}f[x])
7.  rec-case(v)  of
      []  =>  inr  (\mlambda{}x.Ax) 
      h::t  =>
        r.if  f[h]  then  inl  h  else  r  fi 
=  rec-case(v)  of
    []  =>  inr  (\mlambda{}x.Ax) 
    h::t  =>
      r.if  f[h]  then  inl  h  else  r  fi 
8.  x  :  \mexists{}x:\{T|  ((x  \mmember{}  v)  \mwedge{}  (\muparrow{}f[x]))\}  +  (\mforall{}x\mmember{}v.\mneg{}\muparrow{}f[x])
\mvdash{}  x  \mmember{}  \mexists{}x:\{T|  ((x  \mmember{}  [u  /  v])  \mwedge{}  (\muparrow{}f[x]))\}  +  (\mforall{}x\mmember{}[u  /  v].\mneg{}\muparrow{}f[x])


By

---

Latex:
(D  -1  THEN  Auto)

---

Home Index