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 ⊆B prop: implies:  Q pcw-pp-barred: Barred(pp) int_seg: {i..j-} lelt: i ≤ j < k decidable: Dec(P) or: P ∨ Q iff: ⇐⇒ Q not: ¬A rev_implies:  Q false: False uiff: uiff(P;Q) uimplies: supposing a subtract: 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 then else fi  bfalse: ff btrue: tt ext-eq: A ≡ B unit: Unit it: so_lambda: λ2y.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: 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)
Lemmas referenced :  W_wf W-elimination-facts int_seg_wf subtract_wf decidable__le false_wf not-le-2 less-iff-le condition-implies-le minus-one-mul zero-add minus-one-mul-top nat_wf minus-add minus-minus add-associates add-swap add-commutes add_functionality_wrt_le add-zero le-add-cancel decidable__lt not-lt-2 add-mul-special zero-mul le-add-cancel-alt lelt_wf top_wf less_than_wf true_wf equal_wf add-subtract-cancel W-ext param-co-W-ext unit_wf2 it_wf param-co-W_wf ext-eq_inversion subtype_rel_weakening assert_wf btrue_wf bfalse_wf pcw-steprel_wf subtype_rel_dep_function subtype_base_sq set_subtype_base le_wf int_subtype_base decidable__int_equal not-equal-2 minus-zero le-add-cancel2 int_seg_subtype sq_stable__le
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