Nuprl Lemma : wfterm-accum_wf
∀[opr:Type]. ∀[sort:term(opr) ⟶ ℕ]. ∀[arity:opr ⟶ ((ℕ × ℕ) List)]. ∀[Param:Type]. ∀[C:Param
⟶ wfterm(opr;sort;arity)
⟶ Type].
∀[nextp:Param
⟶ (varname() List)
⟶ opr
⟶ very-dep-fun(Param;varname() List × wfterm(opr;sort;arity);a,bt.C[a;snd(bt)])].
∀[m:a:Param
⟶ vs:(varname() List)
⟶ f:opr
⟶ L:{L:(a:Param × bt:varname() List × wfterm(opr;sort;arity) × C[a;snd(bt)]) List|
vdf-eq(Param;nextp a vs f;L) ∧ (↑wf-term(arity;sort;mkterm(f;map(λx.(fst(snd(x)));L))))}
⟶ C[a;mkterm(f;map(λx.(fst(snd(x)));L))]]. ∀[varcase:a:Param
⟶ vs:(varname() List)
⟶ v:{v:varname()| ¬(v = nullvar() ∈ varname())}
⟶ C[a;varterm(v)]]. ∀[p:Param]. ∀[t:wfterm(opr;sort;arity)].
(wfterm-accum(p;t)
p,vs,v.varcase[p;vs;v]
prm,vs,f,L.m[prm;vs;f;L]
p0,ws,op,sofar,bt.nextp[p0;ws;op;sofar;bt] ∈ C[p;t])
Proof
Definitions occuring in Statement :
wfterm-accum: wfterm-accum,
wfterm: wfterm(opr;sort;arity),
wf-term: wf-term(arity;sort;t),
mkterm: mkterm(opr;bts),
varterm: varterm(v),
term: term(opr),
nullvar: nullvar(),
varname: varname(),
very-dep-fun: very-dep-fun(A;B;a,b.C[a; b]),
vdf-eq: vdf-eq(A;f;L),
map: map(f;as),
list: T List,
nat: ℕ,
assert: ↑b,
uall: ∀[x:A]. B[x],
so_apply: x[s1;s2;s3;s4;s5],
so_apply: x[s1;s2;s3;s4],
so_apply: x[s1;s2;s3],
so_apply: x[s1;s2],
pi1: fst(t),
pi2: snd(t),
not: ¬A,
and: P ∧ Q,
member: t ∈ T,
set: {x:A| B[x]} ,
apply: f a,
lambda: λx.A[x],
function: x:A ⟶ B[x],
product: x:A × B[x],
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
so_lambda: λ2x.t[x],
so_apply: x[s],
subtype_rel: A ⊆r B,
uimplies: b supposing a,
guard: {T},
all: ∀x:A. B[x],
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
wfterm-accum: wfterm-accum,
so_lambda: so_lambda4,
and: P ∧ Q,
pi2: snd(t),
istype: istype(T),
prop: ℙ,
pi1: fst(t),
hered-term: hered-term(opr;t.P[t]),
so_apply: x[s1;s2;s3;s4],
cand: A c∧ B,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
implies: P ⇒ Q,
wfterm: wfterm(opr;sort;arity),
so_lambda: so_lambda3,
so_apply: x[s1;s2;s3],
not: ¬A,
false: False,
assert: ↑b,
ifthenelse: if b then t else f fi ,
wf-term: wf-term(arity;sort;t),
varterm: varterm(v),
btrue: tt,
true: True,
sq_type: SQType(T)
Lemmas referenced :
wfterm-hered-correct-sort-arity,
hered-term-accum_wf2,
correct-sort-arity_wf,
term_wf,
subtype_rel_dep_function,
wfterm_wf,
hered-term_wf,
ext-eq_inversion,
subtype_rel_weakening,
list_wf,
varname_wf,
very-dep-fun_wf,
pi2_wf,
very-dep-fun-subtype-domain,
subtype_rel_product,
vdf-eq_wf,
subtype_rel_list,
hereditarily_wf,
mkterm_wf,
map_wf,
wf-term-hereditarily-correct-sort-arity,
istype-assert,
wf-term_wf,
nullvar_wf,
istype-void,
varterm_wf,
assert_elim,
subtype_base_sq,
bool_wf,
bool_subtype_base,
nat_wf,
istype-nat,
istype-universe
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
hypothesis,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
sqequalRule,
lambdaEquality_alt,
universeIsType,
functionExtensionality,
applyEquality,
instantiate,
cumulativity,
universeEquality,
because_Cache,
independent_isectElimination,
lambdaFormation_alt,
inhabitedIsType,
functionEquality,
productEquality,
productIsType,
productElimination,
dependent_functionElimination,
independent_pairEquality,
setElimination,
rename,
dependent_set_memberEquality_alt,
independent_pairFormation,
independent_functionElimination,
setIsType,
functionIsType,
equalityIstype,
natural_numberEquality,
voidElimination,
equalityTransitivity,
equalitySymmetry
Latex:
\mforall{}[opr:Type]. \mforall{}[sort:term(opr) {}\mrightarrow{} \mBbbN{}]. \mforall{}[arity:opr {}\mrightarrow{} ((\mBbbN{} \mtimes{} \mBbbN{}) List)]. \mforall{}[Param:Type].
\mforall{}[C:Param {}\mrightarrow{} wfterm(opr;sort;arity) {}\mrightarrow{} Type]. \mforall{}[nextp:Param
{}\mrightarrow{} (varname() List)
{}\mrightarrow{} opr
{}\mrightarrow{} very-dep-fun(Param;varname() List
\mtimes{} wfterm(opr;sort;arity);a,bt.C[a;
snd(bt)])].
\mforall{}[m:a:Param
{}\mrightarrow{} vs:(varname() List)
{}\mrightarrow{} f:opr
{}\mrightarrow{} L:\{L:(a:Param \mtimes{} bt:varname() List \mtimes{} wfterm(opr;sort;arity) \mtimes{} C[a;snd(bt)]) List|
vdf-eq(Param;nextp a vs f;L) \mwedge{} (\muparrow{}wf-term(arity;sort;mkterm(f;map(\mlambda{}x.(fst(snd(x)));L))))\}
{}\mrightarrow{} C[a;mkterm(f;map(\mlambda{}x.(fst(snd(x)));L))]]. \mforall{}[varcase:a:Param
{}\mrightarrow{} vs:(varname() List)
{}\mrightarrow{} v:\{v:varname()| \mneg{}(v = nullvar())\}
{}\mrightarrow{} C[a;varterm(v)]]. \mforall{}[p:Param].
\mforall{}[t:wfterm(opr;sort;arity)].
(wfterm-accum(p;t)
p,vs,v.varcase[p;vs;v]
prm,vs,f,L.m[prm;vs;f;L]
p0,ws,op,sofar,bt.nextp[p0;ws;op;sofar;bt] \mmember{} C[p;t])
Date html generated:
2020_05_19-PM-09_58_48
Last ObjectModification:
2020_03_12-PM-01_19_00
Theory : terms
Home
Index