### Nuprl Lemma : tcWO_wf

[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (tcWO(T;x,y.R[x;y]) ∈ ℙ)

Proof

Definitions occuring in Statement :  tcWO: tcWO(T;x,y.>[x; y]) uall: [x:A]. B[x] prop: so_apply: x[s1;s2] member: t ∈ T function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T tcWO: tcWO(T;x,y.>[x; y]) prop: and: P ∧ Q so_lambda: λ2x.t[x] implies:  Q so_apply: x[s1;s2] subtype_rel: A ⊆B so_apply: x[s] all: x:A. B[x] nat: exists: x:A. B[x]
Lemmas referenced :  all_wf nat_wf squash_wf exists_wf less_than_wf not_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule productEquality lemma_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality lambdaEquality because_Cache functionEquality applyEquality hypothesis universeEquality setElimination rename axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    (tcWO(T;x,y.R[x;y])  \mmember{}  \mBbbP{})

Date html generated: 2016_05_13-PM-03_51_50
Last ObjectModification: 2015_12_26-AM-10_17_22

Theory : bar-induction

Home Index