Nuprl Rule : SquashedBarInductionSqBase

H  ⊢ ↓seq-normalize(0;t)

  BY SquashedBarInductionSqBase !parameter{i:l} ()
     
     n,s can not occur free in B
  n:ℕs:(ℕn ⟶ ℕ) ⊢ s ∈ Type
  s:(ℕ ⟶ ℕ) ⊢ ↓∃n:ℕ(B seq-normalize(n;s))
  n:ℕs:(ℕn ⟶ ℕ), w:(↓s) ⊢ s
  n:ℕs:(ℕn ⟶ ℕ), w:(∀m:ℕ(P (n 1) x.if x=n  then m  else (s x)))) ⊢ s



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

Latex:
H    \mvdash{}  \mdownarrow{}P  0  seq-normalize(0;t)

    BY  SquashedBarInductionSqBase  !parameter\{i:l\}  B  n  s  m  x  w  ()
         
          n,s  can  not  occur  free  in  B
    H  n:\mBbbN{},  s:(\mBbbN{}n  {}\mrightarrow{}  \mBbbN{})  \mvdash{}  B  n  s  \mmember{}  Type
    H  s:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  \mvdash{}  \mdownarrow{}\mexists{}n:\mBbbN{}.  (B  n  seq-normalize(n;s))
    H  n:\mBbbN{},  s:(\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}),  w:(\mdownarrow{}B  n  s)  \mvdash{}  P  n  s
    H  n:\mBbbN{},  s:(\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}),  w:(\mforall{}m:\mBbbN{}.  (P  (n  +  1)  (\mlambda{}x.if  x=n    then  m    else  (s  x))))  \mvdash{}  P  n  s



Date html generated: 2017_09_29-PM-05_45_01
Last ObjectModification: 2016_05_16-AM-06_45_22

Theory : rules


Home Index