### Nuprl Lemma : add-sz_wf

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

Proof

Definitions occuring in Statement :  add-sz: `add-sz(sz;L;x)` tuple-type: `tuple-type(L)` map: `map(f;as)` list: `T List` partial: `partial(T)` nat: `ℕ` uall: `∀[x:A]. B[x]` member: `t ∈ T` apply: `f a` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` decide: `case b 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: `P `` 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

Latex:
\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.case  x
of  inl(y)  =>
case  y  of  inl(p)  =>  X  p  |  inr(p)  =>  (X  p)  List
|  inr(E)  =>
E;L))].
(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