Nuprl Lemma : pi-guarded-aux_wf

[compList:(pi_prefix() × pi_term()) List]. ∀[g:{Q:pi_term()| (∃C∈compList. pi-rank(Q) ≤ pi-rank(snd(C)))} 
                                                ─→ Id
                                                ─→ Name
                                                ─→ (Name List)
                                                ─→ pi-process()].
  (pi-guarded-aux(compList;g) ∈ Id ─→ Name ─→ (Name List) ─→ pi-process())


Proof




Definitions occuring in Statement :  pi-guarded-aux: pi-guarded-aux(compList;g) pi-process: pi-process() pi-rank: pi-rank(p) pi_term: pi_term() pi_prefix: pi_prefix() Id: Id name: Name l_exists: (∃x∈L. P[x]) list: List uall: [x:A]. B[x] pi2: snd(t) le: A ≤ B member: t ∈ T set: {x:A| B[x]}  function: x:A ─→ B[x] product: x:A × B[x]
Lemmas :  top_wf Id_wf pi_term_wf l_exists_wf pi_prefix_wf l_member_wf le_wf pi-rank_wf nat_wf name_wf list_wf pi-process_wf fix_wf_corec_3parameter piM_wf ldag_wf Com_wf continuous-constant pDVmsg?_wf bool_wf eqtt_to_assert pDVmsg-val_wf pDVmsg-index_wf lt_int_wf length_wf assert_of_lt_int select_wf pi-simple-subst_wf pircv-var_wf lelt_wf sq_stable__le make-lg_wf_dag cons_wf mk-tagged_wf_pCom_msg PiDataVal_wf subtype_rel_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot le_weakening and_wf pi2_wf less_than_wf nil_wf list-cases Process_wf product_subtype_list pi-rank-pi-simple-subst squash_wf true_wf

Latex:
\mforall{}[compList:(pi\_prefix()  \mtimes{}  pi\_term())  List].  \mforall{}[g:\{Q:pi\_term()| 
                                                                                                  (\mexists{}C\mmember{}compList.  pi-rank(Q)  \mleq{}  pi-rank(snd(C)))\} 
                                                                                                {}\mrightarrow{}  Id
                                                                                                {}\mrightarrow{}  Name
                                                                                                {}\mrightarrow{}  (Name  List)
                                                                                                {}\mrightarrow{}  pi-process()].
    (pi-guarded-aux(compList;g)  \mmember{}  Id  {}\mrightarrow{}  Name  {}\mrightarrow{}  (Name  List)  {}\mrightarrow{}  pi-process())



Date html generated: 2015_07_23-AM-11_59_23
Last ObjectModification: 2015_01_29-AM-07_49_33

Home Index