Nuprl Lemma : modify-combinator2_wf

[n:ℕ]. ∀[A:ℕn ⟶ Type]. ∀[m:ℕ].
  ∀[B:ℕm ⟶ Type]. ∀[T:Type]. ∀[f:(i:ℕn ⟶ (A Top)) ⟶ (i:ℕm ⟶ (B Top)) ⟶ T].
    (modify-combinator2(f) ∈ (i:ℕn ⟶ (A Top))
     ⟶ (i:ℕ1 ⟶ if (i =z 0) then one_or_both(B 0;B 1) Top else (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 then else fi  eq_int: (i =z j) less_than: a < b uimplies: supposing a uall: [x:A]. B[x] top: Top member: t ∈ T apply: a function: x:A ⟶ B[x] union: left right subtract: m add: m natural_number: $n universe: Type one_or_both: one_or_both(A;B)
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a modify-combinator2: modify-combinator2(f) int_seg: {i..j-} all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  uiff: uiff(P;Q) and: P ∧ Q lelt: i ≤ j < k le: A ≤ B less_than': less_than'(a;b) false: False not: ¬A prop: guard: {T} nat: ge: i ≥  decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] top: Top bfalse: ff sq_type: SQType(T) bnot: ¬bb assert: b nequal: a ≠ b ∈  eq_int: (i =z j) subtype_rel: A ⊆B subtract: m

Latex:
\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: 2016_05_16-AM-10_10_54
Last ObjectModification: 2016_01_17-PM-01_23_20

Theory : new!event-ordering


Home Index