Nuprl Lemma : add-sz_wf

[P:Type]. ∀[X:P ⟶ Type]. ∀[sz:i:P ⟶ (X i) ⟶ partial(ℕ)]. ∀[L:(P Type) List].
[x:tuple-type(map(λ of inl(y) => case of inl(p) => inr(p) => (X p) List inr(E) => E;L))].
  (add-sz(sz;L;x) ∈ partial(ℕ))


Definitions occuring in Statement :  add-sz: add-sz(sz;L;x) tuple-type: tuple-type(L) map: map(f;as) list: List partial: partial(T) nat: uall: [x:A]. B[x] member: t ∈ T apply: a lambda: λx.A[x] function: x:A ⟶ B[x] decide: case of inl(x) => s[x] inr(y) => t[y] union: left right universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T add-sz: add-sz(sz;L;x) all: x:A. B[x] implies:  Q nat: le: A ≤ B and: P ∧ Q less_than': less_than'(a;b) false: False not: ¬A
Lemmas referenced :  tuple-sum-wf-partial list_wf l_sum-wf-partial-nat map_wf partial_wf nat_wf nat-partial-nat istype-false istype-le tuple-type_wf istype-universe
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut thin instantiate extract_by_obid sqequalHypSubstitution isectElimination unionEquality cumulativity hypothesisEquality universeEquality Error :lambdaEquality_alt,  equalityTransitivity hypothesis equalitySymmetry Error :inhabitedIsType,  Error :lambdaFormation_alt,  unionElimination sqequalRule applyEquality Error :equalityIstype,  dependent_functionElimination independent_functionElimination Error :unionIsType,  Error :universeIsType,  functionExtensionality Error :dependent_set_memberEquality_alt,  natural_numberEquality independent_pairFormation because_Cache axiomEquality Error :isect_memberEquality_alt,  Error :isectIsTypeImplies,  Error :functionIsType

\mforall{}[P:Type].  \mforall{}[X:P  {}\mrightarrow{}  Type].  \mforall{}[sz:i:P  {}\mrightarrow{}  (X  i)  {}\mrightarrow{}  partial(\mBbbN{})].  \mforall{}[L:(P  +  P  +  Type)  List].
\mforall{}[x:tuple-type(map(\mlambda{}  x
                                              of  inl(y)  =>
                                              case  y  of  inl(p)  =>  X  p  |  inr(p)  =>  (X  p)  List
                                              |  inr(E)  =>
    (add-sz(sz;L;x)  \mmember{}  partial(\mBbbN{}))

Date html generated: 2019_06_20-PM-02_04_13
Last ObjectModification: 2019_02_22-AM-11_23_13

Theory : tuples

Home Index