Nuprl Lemma : pi-par-decompose

[P:pi_term()]. pipar(pipar-left(P);pipar-right(P)) ∈ pi_term() supposing ↑pipar?(P)


Proof




Definitions occuring in Statement :  pipar-right: pipar-right(v) pipar-left: pipar-left(v) pipar?: pipar?(v) pipar: pipar(left;right) pi_term: pi_term() assert: b uimplies: supposing a uall: [x:A]. B[x] equal: t ∈ T
Lemmas :  nat_properties less_than_transitivity1 less_than_irreflexivity ge_wf less_than_wf assert_wf pipar?_wf le_wf pi_term_size_wf pi_term_wf int_seg_wf decidable__le subtract_wf false_wf not-ge-2 less-iff-le condition-implies-le minus-one-mul zero-add minus-add minus-minus add-associates add-swap add-commutes add_functionality_wrt_le add-zero le-add-cancel decidable__equal_int subtype_rel-int_seg le_weakening int_seg_properties pi_term-ext eq_atom_wf bool_wf eqtt_to_assert assert_of_eq_atom subtype_base_sq atom_subtype_base unit_wf2 unit_subtype_base it_wf assert_elim pizero_wf bfalse_wf btrue_neq_bfalse eqff_to_assert equal_wf bool_cases_sqequal bool_subtype_base assert-bnot neg_assert_of_eq_atom decidable__lt not-le-2 subtract-is-less lelt_wf picomm_wf nat_wf pioption_wf pipar_wf pirep_wf pinew_wf not-equal-2 le-add-cancel-alt sq_stable__le add-mul-special zero-mul

Latex:
\mforall{}[P:pi\_term()].  P  =  pipar(pipar-left(P);pipar-right(P))  supposing  \muparrow{}pipar?(P)



Date html generated: 2015_07_23-AM-11_32_56
Last ObjectModification: 2015_01_29-AM-00_55_57

Home Index