Nuprl Rule : divergentSqle
This rule proved as lemma rule_convergence_true3 in file rules/rules_squiggle3.v
at https://github.com/vrahli/NuprlInCoq
H ⊢ a ≤ b
BY divergentSqle y !parameter{i:l} ()
H y:(a)↓ ⊢ a ≤ b
H y:is-exception(a) ⊢ a ≤ b
H ⊢ (a)↓ ∈ ℙ
H ⊢ is-exception(a) ∈ ℙ
Definitions occuring in rule :
sqle: s ≤ t,
has-value: (a)↓,
member: t ∈ T,
prop: ℙ,
is-exception: is-exception(t),
axiom: Ax
Latex:
H \mvdash{} a \mleq{} b
BY divergentSqle y !parameter\{i:l\} ()
H y:(a)\mdownarrow{} \mvdash{} a \mleq{} b
H y:is-exception(a) \mvdash{} a \mleq{} b
H \mvdash{} (a)\mdownarrow{} \mmember{} \mBbbP{}
H \mvdash{} is-exception(a) \mmember{} \mBbbP{}
Date html generated:
2019_06_20-PM-04_11_57
Last ObjectModification:
2016_07_08-PM-03_49_00
Theory : rules
Home
Index