Nuprl Rule : choiceSequenceRec

H  ⊢ ↓∃f:ℕ ⟶ ℕ. ∀n:ℕ(↓f)

  BY choiceSequenceRec !parameter{i:l} ()
     
     n ≠ 
     f ≠ 
     m ≠ 
     x ≠ 
     x ≠ 
     x ≠ 
     can not occur free in P
  H  ⊢ s
  n:ℕf:(ℕn ⟶ ℕ), z:P f ⊢ ↓∃m:ℕ(P (n 1) x.if x=n  then m  else (f x)))
  n:ℕf:(ℕn ⟶ ℕ) ⊢ f ∈ Type



Definitions occuring in rule :  all: x:A. B[x] squash: T exists: x:A. B[x] add: m lambda: λx.A[x] int_eq: if a=b  then c  else d function: x:A ⟶ B[x] int_seg: {i..j-} natural_number: $n nat: member: t ∈ T universe: Type apply: a axiom: Ax

Latex:
H    \mvdash{}  \mdownarrow{}\mexists{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mforall{}n:\mBbbN{}.  (\mdownarrow{}P  n  f)

    BY  choiceSequenceRec  !parameter\{i:l\}  m  x  z  s  ()
         
          n  \mneq{}  m 
          f  \mneq{}  n 
          m  \mneq{}  f 
          x  \mneq{}  f 
          x  \mneq{}  m 
          x  \mneq{}  n 
          m  can  not  occur  free  in  P
    H    \mvdash{}  P  0  s
    H  n:\mBbbN{},  f:(\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}),  z:P  n  f  \mvdash{}  \mdownarrow{}\mexists{}m:\mBbbN{}.  (P  (n  +  1)  (\mlambda{}x.if  x=n    then  m    else  (f  x)))
    H  n:\mBbbN{},  f:(\mBbbN{}n  {}\mrightarrow{}  \mBbbN{})  \mvdash{}  P  n  f  \mmember{}  Type



Date html generated: 2017_09_29-PM-05_45_01
Last ObjectModification: 2016_06_07-PM-05_35_52

Theory : rules


Home Index