Nuprl Rule : orFunctionality

H x:(P ∨ Q) @lvl, J ⊢ A ∨ B ext experimental{orFunctionality}(case x of inl(v) => inl a | inr(v) => inr b )

  BY orFunctionality #$i v w ()
  
  H v:P @lvl, J ⊢ A ext a
  H v:Q @lvl, J ⊢ B ext b
  H v:(Q ∈ 𝕌{lvl}), w:(P ∈ 𝕌{lvl}), J ⊢ A ∈ 𝕌{lvl}
  H v:(P ∈ 𝕌{lvl}), w:(Q ∈ 𝕌{lvl}), J ⊢ B ∈ 𝕌{lvl}

Latex:
H  x:(P  \mvee{}  Q)  @lvl,  J
      \mvdash{}  A  \mvee{}  B  ext  experimental\{orFunctionality\}(case  x  of  inl(v)  =>  inl  a  |  inr(v)  =>  inr  b  )

    BY  orFunctionality  \#\$i  v  w  ()
   
    H  v:P  @lvl,  J  \mvdash{}  A  ext  a
    H  v:Q  @lvl,  J  \mvdash{}  B  ext  b
    H  v:(Q  \mmember{}  \mBbbU{}\{lvl\}),  w:(P  \mmember{}  \mBbbU{}\{lvl\}),  J  \mvdash{}  A  \mmember{}  \mBbbU{}\{lvl\}
    H  v:(P  \mmember{}  \mBbbU{}\{lvl\}),  w:(Q  \mmember{}  \mBbbU{}\{lvl\}),  J  \mvdash{}  B  \mmember{}  \mBbbU{}\{lvl\}


Date html generated: 2019_06_20-PM-04_11_52
Last ObjectModification: 2016_01_12-PM-01_16_33

Theory : rules


Home Index