Nuprl Lemma : term_accum_mkterm_lemma
∀p,bts,f,M,varcase,Q:Top.
(term-accum(mkterm(f;bts) with p)
a,b,c,d.Q[a;b;c;d]
varterm(x) with p ⇒ varcase[p;x]
mkterm(f,bts) with p ⇒ trs.M[p;f;bts;trs] ~ let trs = accumulate (with value d and list item bt):
let p' = Q[p;f;fst(bt);d] in
d
@ [<snd(bt)
, p'
, term-accum(snd(bt) with p')
a,b,c,d.Q[a;b;c;d]
varterm(x) with p ⇒ varcase[p;x]
mkterm(f,bts) with p ⇒ trs.M[p;f;bts;trs]>]
over list:
bts
with starting value:
[]) in
M[p;f;bts;trs])
Proof
Definitions occuring in Statement :
term-accum: term-accum,
mkterm: mkterm(opr;bts),
append: as @ bs,
list_accum: list_accum,
cons: [a / b],
nil: [],
let: let,
top: Top,
so_apply: x[s1;s2;s3;s4],
so_apply: x[s1;s2],
pi1: fst(t),
pi2: snd(t),
all: ∀x:A. B[x],
pair: <a, b>,
sqequal: s ~ t
Definitions unfolded in proof :
all: ∀x:A. B[x],
term-accum: term-accum,
term-accum1: term-accum1,
genrec-ap: genrec-ap,
mkterm: mkterm(opr;bts),
member: t ∈ T
Lemmas referenced :
istype-top
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
sqequalRule,
because_Cache,
inhabitedIsType,
hypothesisEquality,
cut,
introduction,
extract_by_obid,
hypothesis
Latex:
\mforall{}p,bts,f,M,varcase,Q:Top.
(term-accum(mkterm(f;bts) with p)
a,b,c,d.Q[a;b;c;d]
varterm(x) with p {}\mRightarrow{} varcase[p;x]
mkterm(f,bts) with p {}\mRightarrow{} trs.M[p;f;bts;trs]
\msim{} let trs = accumulate (with value d and list item bt):
let p' = Q[p;f;fst(bt);d] in
d
@ [<snd(bt)
, p'
, term-accum(snd(bt) with p')
a,b,c,d.Q[a;b;c;d]
varterm(x) with p {}\mRightarrow{} varcase[p;x]
mkterm(f,bts) with p {}\mRightarrow{} trs.M[p;f;bts;trs]>]
over list:
bts
with starting value:
[]) in
M[p;f;bts;trs])
Date html generated:
2020_05_19-PM-09_55_18
Last ObjectModification:
2020_03_09-PM-04_08_49
Theory : terms
Home
Index