Nuprl Lemma : get-triples

Nuprl Lemma : get-triples_wf

[preList:pi_prefix() List].

[st:x:Id fp-> pi_prefix() List]. (get-triples(preList;st)

(

Id

Name) List)

Proof not projected

Definitions occuring in Statement : get-triples: get-triples(preList;st), pi_prefix: pi_prefix(), fpf: a:A fp-> B[a], Id: Id, name: Name, nat:

, uall:

[x:A]. B[x], member: t

T, product: x:A

B[x], list: type List
Definitions : so_lambda:

x.t[x], subtype: S

T, all:

x:A. B[x], top: Top, let: let, get-triples: get-triples(preList;st), member: t

T, uall:

[x:A]. B[x], so_apply: x[s]
Lemmas : Id_wf, fpf_wf, accum-matching-tagged-indices_wf, pi_prefix_wf, map-index_wf, pi2_wf, pi1_wf_top, interleave2_wf, map_wf, name_wf, nat_wf, concat_wf

\mforall{}[preList:pi\_prefix() List]. \mforall{}[st:x:Id fp-> pi\_prefix() List]. (get-triples(preList;st) \mmember{} (\mBbbN{} \mtimes{} Id \mtimes{} \mBbbN{} \mtimes{} Name) List) Date html generated: 2012_01_23-PM-01_33_53 Last ObjectModification: 2011_12_11-PM-12_21_08 Home Index