Nuprl Lemma : sqequalIffSqle

a,b:Base.  ((a b)  ((a ≤ b) ∧ (b ≤ a)))


Proof




Definitions occuring in Statement :  all: x:A. B[x] implies:  Q and: P ∧ Q base: Base sqle: s ≤ t sqequal: t
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q and: P ∧ Q cand: c∧ B member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  has-value_wf_base is-exception_wf base_sq base_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut divergentSqle sqequalRule hypothesis sqleReflexivity lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality independent_pairFormation sqequalIntensionalEquality

Latex:
\mforall{}a,b:Base.    ((a  \msim{}  b)  {}\mRightarrow{}  ((a  \mleq{}  b)  \mwedge{}  (b  \mleq{}  a)))



Date html generated: 2016_05_13-PM-03_45_54
Last ObjectModification: 2015_12_26-AM-09_58_46

Theory : call!by!value_2


Home Index