Nuprl Rule : impliesFunctionality

H f:(P ⇒ Q) @lvl, J ⊢ A ⇒ B ext experimental{impliesFunctionality}(λa.!((!\\w.h) f g))

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

Latex:
H  f:(P  {}\mRightarrow{}  Q)  @lvl,  J  \mvdash{}  A  {}\mRightarrow{}  B  ext  experimental\{impliesFunctionality\}(\mlambda{}a.!((!\mbackslash{}\mbackslash{}w.h)  f  g))

    BY  impliesFunctionality  \#\$i  a  w  ()
   
    H  a:A  @lvl,  J  \mvdash{}  P  ext  g
    H  a:A  @lvl,  w:Q  @lvl,  J  \mvdash{}  B  ext  h
    H  a:(P  \mmember{}  \mBbbU{}\{lvl\}),  J  \mvdash{}  A  \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