Nuprl Lemma : pi-bar-trans_wf

[l_loc:Id]. ∀[P,Q:pi_term()]. ∀[g:{R:pi_term()| pi-rank(R) < pi-rank(pipar(P;Q))} 
                                   ─→ Id
                                   ─→ Name
                                   ─→ (Name List)
                                   ─→ pi-process()].
  (pi-bar-trans(l_loc;P;Q;g) ∈ Id ─→ Name ─→ (Name List) ─→ pi-process())


Proof




Definitions occuring in Statement :  pi-bar-trans: pi-bar-trans(l_loc;P;Q;g) pi-process: pi-process() pi-rank: pi-rank(p) pipar: pipar(left;right) pi_term: pi_term() Id: Id name: Name list: List less_than: a < b uall: [x:A]. B[x] member: t ∈ T set: {x:A| B[x]}  function: x:A ─→ B[x]
Lemmas :  list_wf name_wf Id_wf rec-process_wf_pi_simple_state int_seg_wf false_wf lelt_wf decidable__equal_int subtype_base_sq int_subtype_base pDVfire?_wf bool_wf eqtt_to_assert make-lg_wf_dag Com_wf piM_wf cons_wf mk-tagged_wf_pCom_msg PiDataVal_wf subtype_rel_wf Process_wf subtype_rel_transitivity pDVloc_wf subtype_rel_self pi_prefix_wf nat_wf unit_wf2 nil_wf eqff_to_assert equal_wf bool_cases_sqequal bool_subtype_base assert-bnot pDVloc_tag?_wf lg-add_wf_dag pDVloc_tag-id_wf mk-tagged_wf_pCom_create pDVloc_tag-name_wf pDVfire_wf map_cons_lemma map_nil_lemma length_of_cons_lemma length_of_nil_lemma lg-size_wf tag-case_wf make-lg_wf mk-tagged_wf_unequal iff_transitivity not_wf equal-wf-base assert_wf eq_atom_wf bnot_wf assert_of_eq_atom iff_weakening_uiff assert_of_bnot mk-tagged_wf pi-process_wf less_than_wf pi-rank_wf pipar_wf squash_wf true_wf rank-par iff_weakening_equal

Latex:
\mforall{}[l$_{loc}$:Id].  \mforall{}[P,Q:pi\_term()].  \mforall{}[g:\{R:pi\_term()|  pi-rank(R)  <  pi-rank(pipar(\000CP;Q))\} 
                                                                    {}\mrightarrow{}  Id
                                                                    {}\mrightarrow{}  Name
                                                                    {}\mrightarrow{}  (Name  List)
                                                                    {}\mrightarrow{}  pi-process()].
    (pi-bar-trans(l$_{loc}$;P;Q;g)  \mmember{}  Id  {}\mrightarrow{}  Name  {}\mrightarrow{}  (Name  List)  {}\mrightarrow{}  pi-process())



Date html generated: 2015_07_23-AM-11_59_05
Last ObjectModification: 2015_02_04-PM-03_43_21

Home Index