Nuprl Rule : barInduction
H ⊢ f [] ∈ X []
BY barInduction T R !parameter{i:l} a s x n t ()
H ⊢ T ∈ Type
H s:(T List) ⊢ (R s) ∨ (¬(R s))
H a:(ℕ ⟶ T) ⊢ ↓∃n:ℕ. (R map(a;upto(n)))
H s:(T List), x:R s ⊢ f s ∈ X s
H s:(T List), x:(∀t:T. (f (s @ [t]) ∈ X (s @ [t]))) ⊢ f s ∈ X s
Definitions occuring in rule :
universe: Type,
or: P ∨ Q,
not: ¬A,
function: x:A ⟶ B[x],
squash: ↓T,
exists: ∃x:A. B[x],
nat: ℕ,
map: map(f;as),
upto: upto(n),
list: T List,
all: ∀x:A. B[x],
append: as @ bs,
cons: [a / b],
nil: [],
member: t ∈ T,
apply: f a,
axiom: Ax
Latex:
H \mvdash{} f [] \mmember{} X []
BY barInduction T R !parameter\{i:l\} a s x n t ()
H \mvdash{} T \mmember{} Type
H s:(T List) \mvdash{} (R s) \mvee{} (\mneg{}(R s))
H a:(\mBbbN{} {}\mrightarrow{} T) \mvdash{} \mdownarrow{}\mexists{}n:\mBbbN{}. (R map(a;upto(n)))
H s:(T List), x:R s \mvdash{} f s \mmember{} X s
H s:(T List), x:(\mforall{}t:T. (f (s @ [t]) \mmember{} X (s @ [t]))) \mvdash{} f s \mmember{} X s
Date html generated:
2019_06_20-PM-04_12_06
Last ObjectModification:
2015_11_25-PM-03_37_51
Theory : rules
Home
Index