Nuprl Rule : compactness
H z:(F fix(f))↓, J ⊢ C ext !((!\\x.g) Ax)
BY compactness #$i j x ()
H z:(F fix(f))↓, [j:ℕ], x:(F (f^j ⊥))↓, J ⊢ C ext g
Definitions occuring in rule :
axiom: Ax,
fix: fix(F),
nat: ℕ,
has-value: (a)↓,
apply: f a,
fun_exp: f^n,
bottom: ⊥
Latex:
H z:(F fix(f))\mdownarrow{}, J \mvdash{} C ext !((!\mbackslash{}\mbackslash{}x.g) Ax)
BY compactness \#\$i j x ()
H z:(F fix(f))\mdownarrow{}, [j:\mBbbN{}], x:(F (f\^{}j \mbot{}))\mdownarrow{}, J \mvdash{} C ext g
Date html generated:
2019_06_20-PM-04_12_03
Last ObjectModification:
2015_11_23-PM-03_41_56
Theory : rules
Home
Index