Nuprl Rule : divergentSqlen
H ⊢ a ≤n b
BY divergentSqlen y !parameter{i:l} ()
H y:(a)↓ ⊢ a ≤n b
H y:is-exception(a) ⊢ a ≤n b
H ⊢ (a)↓ ∈ ℙ
Definitions occuring in rule :
is-exception: is-exception(t),
sqle_n: s ≤n t,
member: t ∈ T,
prop: ℙ,
has-value: (a)↓,
axiom: Ax
Latex:
H \mvdash{} a \mleq{}n b
BY divergentSqlen y !parameter\{i:l\} ()
H y:(a)\mdownarrow{} \mvdash{} a \mleq{}n b
H y:is-exception(a) \mvdash{} a \mleq{}n b
H \mvdash{} (a)\mdownarrow{} \mmember{} \mBbbP{}
Date html generated:
2019_06_20-PM-04_12_05
Last ObjectModification:
2015_11_23-PM-03_41_59
Theory : rules
Home
Index