Nuprl Lemma : W-rec_wf

`∀[T,A:Type]. ∀[B:A ⟶ Type]. ∀[F:a:A ⟶ (B[a] ⟶ W(A;a.B[a])) ⟶ (B[a] ⟶ T) ⟶ T]. ∀[w:W(A;a.B[a])].`
`  (W-rec(a,f,r.F[a;f;r];w) ∈ T)`

Proof

Definitions occuring in Statement :  W-rec: `W-rec(a,f,r.F[a; f; r];w)` W: `W(A;a.B[a])` uall: `∀[x:A]. B[x]` so_apply: `x[s1;s2;s3]` so_apply: `x[s]` member: `t ∈ T` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` so_apply: `x[s]` all: `∀x:A. B[x]` and: `P ∧ Q` nat: `ℕ` subtype_rel: `A ⊆r B` prop: `ℙ` implies: `P `` Q` pcw-pp-barred: `Barred(pp)` int_seg: `{i..j-}` lelt: `i ≤ j < k` decidable: `Dec(P)` or: `P ∨ Q` iff: `P `⇐⇒` Q` not: `¬A` rev_implies: `P `` Q` false: `False` uiff: `uiff(P;Q)` uimplies: `b supposing a` subtract: `n - m` top: `Top` le: `A ≤ B` less_than': `less_than'(a;b)` true: `True` cw-step: `cw-step(A;a.B[a])` pcw-step: `pcw-step(P;p.A[p];p,a.B[p; a];p,a,b.C[p; a; b])` spreadn: spread3 less_than: `a < b` squash: `↓T` isr: `isr(x)` assert: `↑b` ifthenelse: `if b then t else f fi ` bfalse: `ff` btrue: `tt` ext-eq: `A ≡ B` unit: `Unit` it: `⋅` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` so_lambda: `so_lambda(x,y,z.t[x; y; z])` so_apply: `x[s1;s2;s3]` ext-family: `F ≡ G` pi1: `fst(t)` nat_plus: `ℕ+` guard: `{T}` W-rel: `W-rel(A;a.B[a];w)` param-W-rel: `param-W-rel(P;p.A[p];p,a.B[p; a];p,a,b.C[p; a; b];par;w)` pcw-steprel: `StepRel(s1;s2)` pi2: `snd(t)` isl: `isl(x)` pcw-step-agree: `StepAgree(s;p1;w)` cand: `A c∧ B` Wsup: `Wsup(a;b)` sq_type: `SQType(T)` sq_stable: `SqStable(P)` W-rec: `W-rec(a,f,r.F[a; f; r];w)`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution hypothesis sqequalRule axiomEquality equalityTransitivity equalitySymmetry extract_by_obid isectElimination thin cumulativity hypothesisEquality lambdaEquality applyEquality functionExtensionality isect_memberEquality because_Cache functionEquality universeEquality dependent_functionElimination productElimination strong_bar_Induction natural_numberEquality setElimination rename independent_functionElimination dependent_set_memberEquality independent_pairFormation unionElimination lambdaFormation voidElimination independent_isectElimination addEquality voidEquality minusEquality intEquality lessCases sqequalAxiom imageMemberEquality baseClosed imageElimination int_eqReduceTrueSq promote_hyp hypothesis_subsumption equalityElimination dependent_pairEquality productEquality inlEquality unionEquality hyp_replacement applyLambdaEquality instantiate

Latex:
\mforall{}[T,A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[F:a:A  {}\mrightarrow{}  (B[a]  {}\mrightarrow{}  W(A;a.B[a]))  {}\mrightarrow{}  (B[a]  {}\mrightarrow{}  T)  {}\mrightarrow{}  T].
\mforall{}[w:W(A;a.B[a])].
(W-rec(a,f,r.F[a;f;r];w)  \mmember{}  T)

Date html generated: 2017_04_14-AM-07_43_46
Last ObjectModification: 2017_02_27-PM-03_14_48

Theory : co-recursion

Home Index