Nuprl Lemma : modify-combinator2_wf

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

Proof

Definitions occuring in Statement :  modify-combinator2: `modify-combinator2(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 less_than_wf nat_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-combinator2(f)  \mmember{}  (i:\mBbbN{}n  {}\mrightarrow{}  (A  i  +  Top))
{}\mrightarrow{}  (i:\mBbbN{}m  -  1  {}\mrightarrow{}  if  (i  =\msubz{}  0)  then  one\_or\_both(B  0;B  1)  +  Top  else  B  (i  +  1)  +  Top  fi  )
{}\mrightarrow{}  T)
supposing  1  <  m

Date html generated: 2015_07_17-AM-08_59_37
Last ObjectModification: 2015_01_27-PM-01_05_45

Home Index