Nuprl Lemma : not-btrue-sqle-bfalse

¬(tt ≤ ff)


Proof




Definitions occuring in Statement :  bfalse: ff btrue: tt not: ¬A sqle: s ≤ t
Definitions unfolded in proof :  not: ¬A implies:  Q member: t ∈ T uall: [x:A]. B[x] ifthenelse: if then else fi  btrue: tt bfalse: ff uimplies: supposing a false: False prop:
Lemmas referenced :  sqle_wf_base bottom_diverge int-value-type value-type-has-value has-value-monotonic is-exception_wf has-value_wf_base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut divergentSqle sqleRule sqleReflexivity lemma_by_obid sqequalHypSubstitution isectElimination thin baseClosed hypothesis sqequalRule independent_isectElimination intEquality natural_numberEquality independent_functionElimination voidElimination

Latex:
\mneg{}(tt  \mleq{}  ff)



Date html generated: 2016_05_13-PM-03_46_25
Last ObjectModification: 2016_01_14-PM-07_11_09

Theory : call!by!value_2


Home Index