Nuprl Lemma : hered-term-accum_wf2
∀[opr:Type]. ∀[P:term(opr) ⟶ ℙ]. ∀[Param:Type]. ∀[C:Param ⟶ hered-term(opr;t.P[t]) ⟶ Type].
∀[nextp:Param
        ⟶ (varname() List)
        ⟶ opr
        ⟶ very-dep-fun(Param;varname() List × hered-term(opr;t.P[t]);a,bt.C[a;snd(bt)])].
∀[m:a:Param
    ⟶ vs:(varname() List)
    ⟶ f:opr
    ⟶ L:{L:(a:Param × bt:varname() List × hered-term(opr;t.P[t]) × C[a;snd(bt)]) List| 
          vdf-eq(Param;nextp a vs f;L) ∧ hereditarily(opr;s.P[s];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())) ∧ P[varterm(v)]} 
                                                          ⟶ C[a;varterm(v)]]. ∀[p:Param]. ∀[t:hered-term(opr;t.P[t])].
  (hered-term-accum(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];
                    p;
                    <[], t>) ∈ C[p;t])
Proof
Definitions occuring in Statement : 
hered-term-accum: hered-term-accum, 
hered-term: hered-term(opr;t.P[t])
, 
hereditarily: hereditarily(opr;s.P[s];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)
, 
nil: []
, 
list: T List
, 
uall: ∀[x:A]. B[x]
, 
prop: ℙ
, 
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]
, 
so_apply: x[s]
, 
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]
, 
pair: <a, b>
, 
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 y.t[x; y]
, 
so_lambda: λ2x.t[x]
, 
so_apply: x[s]
, 
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]
, 
pi2: snd(t)
, 
subtype_rel: A ⊆r B
, 
hered-term: hered-term(opr;t.P[t])
, 
and: P ∧ Q
, 
uimplies: b supposing a
, 
not: ¬A
, 
implies: P 
⇒ Q
, 
false: False
, 
iff: P 
⇐⇒ Q
, 
rev_implies: P 
⇐ Q
, 
prop: ℙ
, 
guard: {T}
, 
all: ∀x:A. B[x]
, 
pi1: fst(t)
Lemmas referenced : 
hered-term-accum_wf, 
pi2_wf, 
list_wf, 
varname_wf, 
hered-term_wf, 
term_wf, 
nil_wf, 
subtype_rel_self, 
varterm_wf, 
hereditarily-varterm, 
nullvar_wf, 
istype-void, 
hereditarily_wf, 
vdf-eq_wf, 
mkterm_wf, 
map_wf, 
trivial-equal, 
very-dep-fun_wf, 
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, 
applyEquality, 
universeIsType, 
productIsType, 
independent_pairEquality, 
functionIsType, 
because_Cache, 
setElimination, 
rename, 
dependent_set_memberEquality_alt, 
productElimination, 
independent_isectElimination, 
equalityIstype, 
inhabitedIsType, 
independent_functionElimination, 
equalityTransitivity, 
equalitySymmetry, 
setIsType, 
productEquality, 
dependent_functionElimination, 
universeEquality, 
instantiate
Latex:
\mforall{}[opr:Type].  \mforall{}[P:term(opr)  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[Param:Type].  \mforall{}[C:Param  {}\mrightarrow{}  hered-term(opr;t.P[t])  {}\mrightarrow{}  Type].
\mforall{}[nextp:Param
                {}\mrightarrow{}  (varname()  List)
                {}\mrightarrow{}  opr
                {}\mrightarrow{}  very-dep-fun(Param;varname()  List  \mtimes{}  hered-term(opr;t.P[t]);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{}  hered-term(opr;t.P[t])  \mtimes{}  C[a;snd(bt)])  List| 
                    vdf-eq(Param;nextp  a  vs  f;L)
                    \mwedge{}  hereditarily(opr;s.P[s];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()))  \mwedge{}  P[varterm(v)]\} 
                                                                                                                    {}\mrightarrow{}  C[a;varterm(v)]].  \mforall{}[p:Param].
\mforall{}[t:hered-term(opr;t.P[t])].
    (hered-term-accum(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];
                                        p;
                                        <[],  t>)  \mmember{}  C[p;t])
Date html generated:
2020_05_19-PM-09_54_58
Last ObjectModification:
2020_03_10-PM-06_09_23
Theory : terms
Home
Index