Nuprl Lemma : modify-combinator1_wf

∀[n:ℕ]
  ∀[A:ℕn ─→ Type]. ∀[m:ℕ]. ∀[B:ℕm ─→ Type]. ∀[T:Type]. ∀[f:(i:ℕn ─→ (A i + Top)) ─→ (i:ℕm ─→ (B i + Top)) ─→ T].
    (modify-combinator1(f) ∈ (i:ℕn - 1 ─→ if (i =z 0) then one_or_both(A 0;A 1) + Top else A (i + 1) + Top fi )
     ─→ (i:ℕm ─→ (B i + Top))
     ─→ T) 
  supposing 1 < n


Proof



Definitions occuring in Statement :  modify-combinator1: modify-combinator1(f),  int_seg: {i..j-},  nat: ℕ,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  less_than: a < b,  uimplies: b supposing a,  uall: ∀[x:A]. B[x],  top: Top,  member: t ∈ T,  apply: f a,  function: x:A ─→ B[x],  union: left + right,  subtract: n - m,  add: n + m,  natural_number: $n,  universe: Type,  one_or_both: one_or_both(A;B)
Lemmas :  eq_int_wf,  bool_wf,  eqtt_to_assert,  assert_of_eq_int,  false_wf,  decidable__lt,  subtract_wf,  less-iff-le,  condition-implies-le,  minus-add,  minus-minus,  minus-one-mul,  zero-add,  add-commutes,  add_functionality_wrt_le,  add-associates,  add-swap,  le-add-cancel,  lelt_wf,  one_or_both_wf,  top_wf,  eqff_to_assert,  equal_wf,  bool_cases_sqequal,  subtype_base_sq,  bool_subtype_base,  assert-bnot,  neg_assert_of_eq_int,  oob-hasleft_wf,  oob-getleft_wf,  int_subtype_base,  subtype_rel_self,  assert_wf,  not-equal-2,  oob-hasright_wf,  oob-getright_wf,  decidable__le,  not-le-2,  sq_stable__le,  add-zero,  minus-zero,  le-add-cancel-alt,  subtype_rel-equal,  le_antisymmetry_iff,  le-add-cancel2,  int_seg_wf,  nat_wf,  less_than_wf
\mforall{}[n:\mBbbN{}]
    \mforall{}[A:\mBbbN{}n  {}\mrightarrow{}  Type].  \mforall{}[m:\mBbbN{}].  \mforall{}[B:\mBbbN{}m  {}\mrightarrow{}  Type].  \mforall{}[T:Type].  \mforall{}[f:(i:\mBbbN{}n  {}\mrightarrow{}  (A  i  +  Top))
                                                                                                                      {}\mrightarrow{}  (i:\mBbbN{}m  {}\mrightarrow{}  (B  i  +  Top))
                                                                                                                      {}\mrightarrow{}  T].
        (modify-combinator1(f)  \mmember{}  (i:\mBbbN{}n  -  1  {}\mrightarrow{}  if  (i  =\msubz{}  0)
                                                                                    then  one\_or\_both(A  0;A  1)  +  Top
                                                                                    else  A  (i  +  1)  +  Top
                                                                                    fi  )
          {}\mrightarrow{}  (i:\mBbbN{}m  {}\mrightarrow{}  (B  i  +  Top))
          {}\mrightarrow{}  T) 
    supposing  1  <  n


Date html generated: 2015_07_17-AM-08_59_30
Last ObjectModification: 2015_01_27-PM-01_05_39

Home Index