### Nuprl Lemma : RankEx1-induction

`∀[T:Type]. ∀[P:RankEx1(T) ─→ ℙ].`
`  ((∀leaf:T. P[RankEx1_Leaf(leaf)])`
`  `` (∀prod:RankEx1(T) × RankEx1(T). (let u,u1 = prod in P[u] ∧ P[u1] `` P[RankEx1_Prod(prod)]))`
`  `` (∀prodl:T × RankEx1(T). (let u,u1 = prodl in P[u1] `` P[RankEx1_ProdL(prodl)]))`
`  `` (∀prodr:RankEx1(T) × T. (let u,u1 = prodr in P[u] `` P[RankEx1_ProdR(prodr)]))`
`  `` (∀list:RankEx1(T) List. ((∀u∈list.P[u]) `` P[RankEx1_List(list)]))`
`  `` {∀v:RankEx1(T). P[v]})`

Proof

Definitions occuring in Statement :  RankEx1_List: `RankEx1_List(list)` RankEx1_ProdR: `RankEx1_ProdR(prodr)` RankEx1_ProdL: `RankEx1_ProdL(prodl)` RankEx1_Prod: `RankEx1_Prod(prod)` RankEx1_Leaf: `RankEx1_Leaf(leaf)` RankEx1: `RankEx1(T)` l_all: `(∀x∈L.P[x])` list: `T List` uall: `∀[x:A]. B[x]` prop: `ℙ` guard: `{T}` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` function: `x:A ─→ B[x]` spread: spread def product: `x:A × B[x]` universe: `Type`
Lemmas :  uniform-comp-nat-induction all_wf isect_wf le_wf RankEx1_size_wf nat_wf less_than_wf RankEx1-ext eq_atom_wf bool_wf eqtt_to_assert assert_of_eq_atom subtype_base_sq atom_subtype_base eqff_to_assert equal_wf bool_cases_sqequal bool_subtype_base assert-bnot neg_assert_of_eq_atom subtract_wf decidable__le false_wf not-le-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 subtract-is-less lelt_wf decidable__lt sum-nat length_wf_nat select_wf sq_stable__le int_seg_wf length_wf sum_wf RankEx1_wf sum-nat-less uall_wf le_weakening list_wf l_all_wf2 l_member_wf RankEx1_List_wf RankEx1_ProdR_wf RankEx1_ProdL_wf RankEx1_Prod_wf RankEx1_Leaf_wf
\mforall{}[T:Type].  \mforall{}[P:RankEx1(T)  {}\mrightarrow{}  \mBbbP{}].
((\mforall{}leaf:T.  P[RankEx1\_Leaf(leaf)])
{}\mRightarrow{}  (\mforall{}prod:RankEx1(T)  \mtimes{}  RankEx1(T).  (let  u,u1  =  prod  in  P[u]  \mwedge{}  P[u1]  {}\mRightarrow{}  P[RankEx1\_Prod(prod)]))
{}\mRightarrow{}  (\mforall{}prodl:T  \mtimes{}  RankEx1(T).  (let  u,u1  =  prodl  in  P[u1]  {}\mRightarrow{}  P[RankEx1\_ProdL(prodl)]))
{}\mRightarrow{}  (\mforall{}prodr:RankEx1(T)  \mtimes{}  T.  (let  u,u1  =  prodr  in  P[u]  {}\mRightarrow{}  P[RankEx1\_ProdR(prodr)]))
{}\mRightarrow{}  (\mforall{}list:RankEx1(T)  List.  ((\mforall{}u\mmember{}list.P[u])  {}\mRightarrow{}  P[RankEx1\_List(list)]))
{}\mRightarrow{}  \{\mforall{}v:RankEx1(T).  P[v]\})

Date html generated: 2015_07_17-AM-07_48_32
Last ObjectModification: 2015_01_27-AM-09_38_57

Home Index