Nuprl Lemma : term-accum1_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)].
(term-accum1(t)
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] ∈ p:P ⟶ R[p;t])
Proof
Definitions occuring in Statement :
term-accum1: term-accum1,
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,
term-accum-induction-ext,
so_apply: x[s1;s2;s3;s4],
so_apply: x[s1;s2],
all: ∀x:A. B[x],
implies: P ⇒ Q,
subtype_rel: A ⊆r B,
prop: ℙ,
not: ¬A,
false: False,
uimplies: b supposing a,
and: P ∧ Q,
nat: ℕ,
so_lambda: λ2x.t[x],
so_apply: x[s],
int_seg: {i..j-},
lelt: i ≤ j < k,
le: A ≤ B,
decidable: Dec(P),
or: P ∨ Q,
satisfiable_int_formula: satisfiable_int_formula(fmla),
exists: ∃x:A. B[x],
pi1: fst(t),
bound-term: bound-term(opr),
pi2: snd(t),
guard: {T}
Lemmas referenced :
term-accum-induction-ext,
term_wf,
list_wf,
varname_wf,
nullvar_wf,
istype-void,
varterm_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,
subtype_rel_self,
istype-universe
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
cut,
sqequalRule,
lambdaEquality_alt,
isectElimination,
hypothesisEquality,
equalityTransitivity,
equalitySymmetry,
hypothesis,
inhabitedIsType,
lambdaFormation_alt,
thin,
equalityIstype,
sqequalHypSubstitution,
dependent_functionElimination,
independent_functionElimination,
isectIsType,
because_Cache,
functionIsType,
universeIsType,
introduction,
extract_by_obid,
universeEquality,
productEquality,
applyEquality,
setIsType,
setElimination,
rename,
independent_isectElimination,
voidElimination,
productIsType,
intEquality,
natural_numberEquality,
sqequalBase,
productElimination,
unionElimination,
approximateComputation,
dependent_pairFormation_alt,
int_eqEquality,
Error :memTop,
independent_pairFormation,
functionEquality,
instantiate
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:\mforall{}p:P. \mforall{}v:\{v:varname()|
\mneg{}(v = nullvar())\} .
R[p;varterm(v)]].
\mforall{}[mktermcase:\mforall{}p:P. \mforall{}f:opr. \mforall{}bts:bound-term(opr) List. \mforall{}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)]))\} .
R[p;mkterm(f;bts)]]. \mforall{}[t:term(opr)].
(term-accum1(t)
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{} p:P {}\mrightarrow{} R[p;t])
Date html generated:
2020_05_19-PM-09_55_10
Last ObjectModification:
2020_03_09-PM-04_08_43
Theory : terms
Home
Index