Nuprl Rule : SquashedBarInduction
H ⊢ ↓P 0 seq-normalize(0;t)
BY SquashedBarInduction !parameter{i:l} B n s m x w ()
n,s can not occur free in B
H n:ℕ, s:(ℕn ⟶ ℕ) ⊢ B n s ∈ Type
H s:(ℕ ⟶ ℕ) ⊢ ↓∃n:ℕ. (B n seq-normalize(n;s))
H n:ℕ, s:(ℕn ⟶ ℕ), w:B n s ⊢ P n s
H n:ℕ, s:(ℕn ⟶ ℕ), w:(∀m:ℕ. (P (n + 1) (λx.if x=n then m else (s x)))) ⊢ P n s
Definitions occuring in rule :
member: t ∈ T,
universe: Type,
squash: ↓T,
exists: ∃x:A. B[x],
seq-normalize: seq-normalize(n;s),
function: x:A ⟶ B[x],
int_seg: {i..j-},
all: ∀x:A. B[x],
nat: ℕ,
add: n + m,
natural_number: $n,
lambda: λx.A[x],
int_eq: if a=b then c else d,
apply: f a,
axiom: Ax
Latex:
H \mvdash{} \mdownarrow{}P 0 seq-normalize(0;t)
BY SquashedBarInduction !parameter\{i:l\} B n s m x w ()
n,s can not occur free in B
H n:\mBbbN{}, s:(\mBbbN{}n {}\mrightarrow{} \mBbbN{}) \mvdash{} B n s \mmember{} Type
H s:(\mBbbN{} {}\mrightarrow{} \mBbbN{}) \mvdash{} \mdownarrow{}\mexists{}n:\mBbbN{}. (B n seq-normalize(n;s))
H n:\mBbbN{}, s:(\mBbbN{}n {}\mrightarrow{} \mBbbN{}), w:B n s \mvdash{} P n s
H n:\mBbbN{}, s:(\mBbbN{}n {}\mrightarrow{} \mBbbN{}), w:(\mforall{}m:\mBbbN{}. (P (n + 1) (\mlambda{}x.if x=n then m else (s x)))) \mvdash{} P n s
Date html generated:
2019_06_20-PM-04_12_08
Last ObjectModification:
2016_01_29-PM-08_06_41
Theory : rules
Home
Index