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