Nuprl Rule : exceptionCompactness

H z:(exception(u; v) ≤ F fix(f)), J ⊢ C ext !((!\\x.g) Ax)

  BY exceptionCompactness #$i j x ()
  
  H z:(exception(u; v) ≤ F fix(f)), [j:ℕ], x:(exception(u; v) ≤ F (f^j ⊥)), J ⊢ C ext g

Latex:
H  z:(exception(u;  v)  \mleq{}  F  fix(f)),  J  \mvdash{}  C  ext  !((!\mbackslash{}\mbackslash{}x.g)  Ax)

    BY  exceptionCompactness  \#\$i  j  x  ()
   
    H  z:(exception(u;  v)  \mleq{}  F  fix(f)),  [j:\mBbbN{}],  x:(exception(u;  v)  \mleq{}  F  (f\^{}j  \mbot{})),  J  \mvdash{}  C  ext  g


Date html generated: 2019_06_20-PM-04_12_11
Last ObjectModification: 2015_04_18-AM-11_22_40

Theory : rules


Home Index