Nuprl Lemma : rec-combined-loc-class_wf

∀[Info:Type]. ∀[n:ℕ]. ∀[A:ℕn ⟶ Type]. ∀[X:i:ℕn ⟶ EClass(A i)]. ∀[T:Type]. ∀[f:Id
                                                                                ⟶ (i:ℕn ⟶ bag(A i))
                                                                                ⟶ bag(T)
                                                                                ⟶ bag(T)].
  (f|Loc, X, Prior(self)| ∈ EClass(T))


Proof



Definitions occuring in Statement :  rec-combined-loc-class: f|Loc, X, Prior(self)|,  eclass: EClass(A[eo; e]),  Id: Id,  int_seg: {i..j-},  nat: ℕ,  uall: ∀[x:A]. B[x],  member: t ∈ T,  apply: f a,  function: x:A ⟶ B[x],  natural_number: $n,  universe: Type,  bag: bag(T)
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  member: t ∈ T,  eclass: EClass(A[eo; e]),  top: Top,  all: ∀x:A. B[x],  subtype_rel: A ⊆r B,  strongwellfounded: SWellFounded(R[x; y]),  exists: ∃x:A. B[x],  nat: ℕ,  implies: P ⇒ Q,  false: False,  ge: i ≥ j ,  uimplies: b supposing a,  satisfiable_int_formula: satisfiable_int_formula(fmla),  not: ¬A,  and: P ∧ Q,  prop: ℙ,  guard: {T},  int_seg: {i..j-},  lelt: i ≤ j < k,  le: A ≤ B,  less_than': less_than'(a;b),  decidable: Dec(P),  or: P ∨ Q,  less_than: a < b,  squash: ↓T,  rec-combined-loc-class: f|Loc, X, Prior(self)|,  primed-class: Prior(X),  so_lambda: λ2x y.t[x; y],  so_apply: x[s1;s2],  sq_exists: ∃x:{A| B[x]},  so_lambda: λ2x.t[x],  so_apply: x[s]
Latex:
\mforall{}[Info:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[A:\mBbbN{}n  {}\mrightarrow{}  Type].  \mforall{}[X:i:\mBbbN{}n  {}\mrightarrow{}  EClass(A  i)].  \mforall{}[T:Type].  \mforall{}[f:Id
                                                                                                                                                                {}\mrightarrow{}  (i:\mBbbN{}n
                                                                                                                                                                      {}\mrightarrow{}  bag(A  i))
                                                                                                                                                                {}\mrightarrow{}  bag(T)
                                                                                                                                                                {}\mrightarrow{}  bag(T)].
    (f|Loc,  X,  Prior(self)|  \mmember{}  EClass(T))


Date html generated: 2016_05_17-AM-00_01_54
Last ObjectModification: 2016_01_17-PM-06_59_18

Theory : event-ordering


Home Index