Step * 2 of Lemma l-first-when-none


1. Type
2. T ⟶ 𝔹
3. T
4. ¬↑f[u]
5. List
6. rec-case(v) of [] => inr x.Ax)  x::xs => r.if f[x] then inl else fi  inr x.Ax)  supposing (∀x∈v.¬↑f[x])
7. (∀x∈[u v].¬↑f[x])
⊢ rec-case(v) of
  [] => inr x.Ax) 
  h::t =>
   r.if f[h] then inl else fi  inr x.Ax) 
BY
BackThruSomeHyp }

1
1. Type
2. T ⟶ 𝔹
3. T
4. ¬↑f[u]
5. List
6. rec-case(v) of [] => inr x.Ax)  x::xs => r.if f[x] then inl else fi  inr x.Ax)  supposing (∀x∈v.¬↑f[x])
7. (∀x∈[u v].¬↑f[x])
⊢ (∀x∈v.¬↑f[x])


Latex:


Latex:

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    \msim{}  inr  (\mlambda{}x.Ax)   
      supposing  (\mforall{}x\mmember{}v.\mneg{}\muparrow{}f[x])
7.  (\mforall{}x\mmember{}[u  /  v].\mneg{}\muparrow{}f[x])
\mvdash{}  rec-case(v)  of
    []  =>  inr  (\mlambda{}x.Ax) 
    h::t  =>
      r.if  f[h]  then  inl  h  else  r  fi    \msim{}  inr  (\mlambda{}x.Ax) 


By


Latex:
BackThruSomeHyp




Home Index