Nuprl Rule : StrongContinuity2

This rule proved as lemma rule_strong_continuity_true2_v3_2 in file continuity/stronger_continuity_rule4_v3.v
 at https://github.com/vrahli/NuprlInCoq  


   ⊢ <λn,f. ν(v.F x.if (x) < (0)  then ⊥  else if (x) < (n)  then x  else (exception(v; Ax)))?v:x.Ax), λf.<Ax, λn.Ax\000C>>
     ∈ ⇃(∃M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ ⋃ Unit)
          ∀f:ℕ ⟶ T
            ((↓∃n:ℕ((M f) (F f) ∈ ℕ))
            ∧ (∀n:ℕ(M f) (F f) ∈ ℕ supposing if is an integer then True else False)))

  BY StrongContinuity2 ()
  
  H  ⊢ F ∈ (ℕ ⟶ T) ⟶ ℕ
  H  ⊢ ↓T
  H  ⊢ T ⊆r ℕ



Definitions occuring in rule :  quotient: x,y:A//B[x; y] int_seg: {i..j-} b-union: A ⋃ B unit: Unit and: P ∧ Q exists: x:A. B[x] all: x:A. B[x] uimplies: supposing a isint: isint def false: False equal: t ∈ T true: True natural_number: $n bottom: less: if (a) < (b)  then c  else d apply: a pair: <a, b> lambda: λx.A[x] member: t ∈ T function: x:A ⟶ B[x] squash: T subtype_rel: A ⊆B nat: axiom: Ax

Latex:

      \mvdash{}  <\mlambda{}n,f.  \mnu{}(v.F  ...?v:x.Ax)
          ,  \mlambda{}f.<Ax,  \mlambda{}n.Ax>
          >  \mmember{}  \00D9(\mexists{}M:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  (\mBbbN{}  \mcup{}  Unit)
                        \mforall{}f:\mBbbN{}  {}\mrightarrow{}  T
                            ((\mdownarrow{}\mexists{}n:\mBbbN{}.  ((M  n  f)  =  (F  f)))
                            \mwedge{}  (\mforall{}n:\mBbbN{}.  (M  n  f)  =  (F  f)  supposing  if  M  n  f  is  an  integer  then  True  else  False)))

    BY  StrongContinuity2  ()
   
    H    \mvdash{}  F  \mmember{}  (\mBbbN{}  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbN{}
    H    \mvdash{}  \mdownarrow{}T
    H    \mvdash{}  T  \msubseteq{}r  \mBbbN{}



Date html generated: 2016_12_14-AM-08_53_50
Last ObjectModification: 2016_07_08-PM-03_49_09

Theory : rules


Home Index