Nuprl Lemma : term-accum_wf
∀[opr,P:Type]. ∀[R:P ⟶ term(opr) ⟶ ℙ]. ∀[Q:P ⟶ opr ⟶ (varname() List) ⟶ ((t:term(opr) × p:P × R[p;t]) List) ⟶ P].
∀[varcase:p:P ⟶ v:{v:varname()| ¬(v = nullvar() ∈ varname())}  ⟶ R[p;varterm(v)]].
∀[mktermcase:p:P
             ⟶ f:opr
             ⟶ bts:(bound-term(opr) List)
             ⟶ L:{L:(t:term(opr) × p:P × R[p;t]) List| 
                   (||L|| = ||bts|| ∈ ℤ)
                   ∧ (∀i:ℕ||L||. ((fst(L[i])) = (snd(bts[i])) ∈ term(opr)))
                   ∧ (∀i:ℕ||L||. ((fst(snd(L[i]))) = Q[p;f;fst(bts[i]);firstn(i;L)] ∈ P))} 
             ⟶ R[p;mkterm(f;bts)]]. ∀[t:term(opr)]. ∀[p:P].
  (term-accum(t with p)
   p,f,vs,tr.Q[p;f;vs;tr]
   varterm(x) with p 
⇒ varcase[p;x]
   mkterm(f,bts) with p 
⇒ trs.mktermcase[p;f;bts;trs] ∈ R[p;t])
Proof
Definitions occuring in Statement : 
term-accum: term-accum, 
bound-term: bound-term(opr)
, 
mkterm: mkterm(opr;bts)
, 
varterm: varterm(v)
, 
term: term(opr)
, 
nullvar: nullvar()
, 
varname: varname()
, 
firstn: firstn(n;as)
, 
select: L[n]
, 
length: ||as||
, 
list: T List
, 
int_seg: {i..j-}
, 
uall: ∀[x:A]. B[x]
, 
prop: ℙ
, 
so_apply: x[s1;s2;s3;s4]
, 
so_apply: x[s1;s2]
, 
pi1: fst(t)
, 
pi2: snd(t)
, 
all: ∀x:A. B[x]
, 
not: ¬A
, 
and: P ∧ Q
, 
member: t ∈ T
, 
set: {x:A| B[x]} 
, 
function: x:A ⟶ B[x]
, 
product: x:A × B[x]
, 
natural_number: $n
, 
int: ℤ
, 
universe: Type
, 
equal: s = t ∈ T
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
so_apply: x[s1;s2]
, 
all: ∀x:A. B[x]
, 
so_apply: x[s1;s2;s3;s4]
, 
and: P ∧ Q
, 
term-accum: term-accum, 
subtype_rel: A ⊆r B
, 
nat: ℕ
, 
so_lambda: λ2x.t[x]
, 
so_apply: x[s]
, 
uimplies: b supposing a
, 
int_seg: {i..j-}
, 
lelt: i ≤ j < k
, 
le: A ≤ B
, 
decidable: Dec(P)
, 
or: P ∨ Q
, 
not: ¬A
, 
implies: P 
⇒ Q
, 
satisfiable_int_formula: satisfiable_int_formula(fmla)
, 
exists: ∃x:A. B[x]
, 
false: False
, 
prop: ℙ
, 
pi1: fst(t)
, 
bound-term: bound-term(opr)
, 
pi2: snd(t)
Lemmas referenced : 
term-accum1_wf, 
term_wf, 
list_wf, 
bound-term_wf, 
istype-int, 
length_wf_nat, 
set_subtype_base, 
le_wf, 
int_subtype_base, 
int_seg_wf, 
length_wf, 
select_wf, 
int_seg_properties, 
decidable__le, 
full-omega-unsat, 
intformand_wf, 
intformnot_wf, 
intformle_wf, 
itermConstant_wf, 
itermVar_wf, 
int_formula_prop_and_lemma, 
int_formula_prop_not_lemma, 
int_formula_prop_le_lemma, 
int_term_value_constant_lemma, 
int_term_value_var_lemma, 
int_formula_prop_wf, 
decidable__lt, 
intformless_wf, 
int_formula_prop_less_lemma, 
intformeq_wf, 
int_formula_prop_eq_lemma, 
pi1_wf, 
firstn_wf, 
mkterm_wf, 
varname_wf, 
nullvar_wf, 
istype-void, 
varterm_wf, 
subtype_rel_self, 
istype-universe
Rules used in proof : 
cut, 
introduction, 
extract_by_obid, 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
isect_memberFormation_alt, 
hypothesis, 
sqequalHypSubstitution, 
isectElimination, 
thin, 
hypothesisEquality, 
sqequalRule, 
applyEquality, 
axiomEquality, 
equalityTransitivity, 
equalitySymmetry, 
universeIsType, 
functionIsType, 
setIsType, 
productEquality, 
because_Cache, 
productIsType, 
equalityIstype, 
intEquality, 
lambdaEquality_alt, 
natural_numberEquality, 
independent_isectElimination, 
sqequalBase, 
setElimination, 
rename, 
productElimination, 
dependent_functionElimination, 
unionElimination, 
approximateComputation, 
independent_functionElimination, 
dependent_pairFormation_alt, 
int_eqEquality, 
Error :memTop, 
independent_pairFormation, 
voidElimination, 
inhabitedIsType, 
lambdaFormation_alt, 
instantiate, 
universeEquality
Latex:
\mforall{}[opr,P:Type].  \mforall{}[R:P  {}\mrightarrow{}  term(opr)  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[Q:P
                                                                                          {}\mrightarrow{}  opr
                                                                                          {}\mrightarrow{}  (varname()  List)
                                                                                          {}\mrightarrow{}  ((t:term(opr)  \mtimes{}  p:P  \mtimes{}  R[p;t])  List)
                                                                                          {}\mrightarrow{}  P].  \mforall{}[varcase:p:P
                                                                                                                            {}\mrightarrow{}  v:\{v:varname()|  \mneg{}(v  =  nullvar())\} 
                                                                                                                            {}\mrightarrow{}  R[p;varterm(v)]].
\mforall{}[mktermcase:p:P
                          {}\mrightarrow{}  f:opr
                          {}\mrightarrow{}  bts:(bound-term(opr)  List)
                          {}\mrightarrow{}  L:\{L:(t:term(opr)  \mtimes{}  p:P  \mtimes{}  R[p;t])  List| 
                                      (||L||  =  ||bts||)
                                      \mwedge{}  (\mforall{}i:\mBbbN{}||L||.  ((fst(L[i]))  =  (snd(bts[i]))))
                                      \mwedge{}  (\mforall{}i:\mBbbN{}||L||.  ((fst(snd(L[i])))  =  Q[p;f;fst(bts[i]);firstn(i;L)]))\} 
                          {}\mrightarrow{}  R[p;mkterm(f;bts)]].  \mforall{}[t:term(opr)].  \mforall{}[p:P].
    (term-accum(t  with  p)
      p,f,vs,tr.Q[p;f;vs;tr]
      varterm(x)  with  p  {}\mRightarrow{}  varcase[p;x]
      mkterm(f,bts)  with  p  {}\mRightarrow{}  trs.mktermcase[p;f;bts;trs]  \mmember{}  R[p;t])
Date html generated:
2020_05_19-PM-09_55_14
Last ObjectModification:
2020_03_09-PM-04_08_45
Theory : terms
Home
Index