Nuprl Rule : bottomDiverges

This rule proved as lemma rule_bottom_diverges_true3 in file rules/rules_false.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ ¬(⊥)↓

  BY bottomDiverges ()
  
  No Subgoals



Definitions occuring in rule :  not: ¬A has-value: (a)↓ bottom: axiom: Ax

Latex:
H    \mvdash{}  \mneg{}(\mbot{})\mdownarrow{}

    BY  bottomDiverges  ()
   
    No  Subgoals



Date html generated: 2019_06_20-PM-04_12_28
Last ObjectModification: 2018_09_17-PM-04_44_34

Theory : rules


Home Index