Nuprl Rule : fixpointLeast
H ⊢ F[fix(f)/z] ≤ t
BY fixpointLeast F z f j ()
H j:ℕ ⊢ F[f^j ⊥/z] ≤ t
Definitions occuring in rule :
fix: fix(F),
nat: ℕ,
sqle: s ≤ t,
apply: f a,
fun_exp: f^n,
bottom: ⊥,
axiom: Ax
Latex:
H \mvdash{} F[fix(f)/z] \mleq{} t
BY fixpointLeast F z f j ()
H j:\mBbbN{} \mvdash{} F[f\^{}j \mbot{}/z] \mleq{} t
Date html generated:
2019_06_20-PM-04_12_01
Last ObjectModification:
2015_11_24-PM-01_52_05
Theory : rules
Home
Index