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