Nuprl Rule : bar_Induction

H  ⊢ f 0 c ∈ X 0 c

  BY bar_Induction T B !parameter{i:l} a s x m n t ()
     
     n,s can not occur free in B
  H  ⊢ T ∈ Type
  H n:ℕ, s:(ℕn ⟶ T) ⊢ (B n s) ∨ (¬(B n s))
  H a:(ℕ ⟶ T) ⊢ ↓∃n:ℕ. (B n a)
  H n:ℕ, s:(ℕn ⟶ T), x:B n s ⊢ f n s ∈ X n s
  H n:ℕ, s:(ℕn ⟶ T), x:(∀t:T. (f (n + 1) (λm.if m=n then t else (s m)) ∈ X (n + 1) (λm.if m=n then t else (s m))))
     ⊢ f n s ∈ X n s


Definitions occuring in rule :  universe: Type,  or: P ∨ Q,  not: ¬A,  squash: ↓T,  exists: ∃x:A. B[x],  nat: ℕ,  function: x:A ⟶ B[x],  int_seg: {i..j-},  all: ∀x:A. B[x],  add: n + m,  natural_number: $n,  lambda: λx.A[x],  int_eq: if a=b then c else d,  member: t ∈ T,  apply: f a,  axiom: Ax
Latex:
H    \mvdash{}  f  0  c  \mmember{}  X  0  c

    BY  bar\_Induction  T  B  !parameter\{i:l\}  a  s  x  m  n  t  ()
         
          n,s  can  not  occur  free  in  B
    H    \mvdash{}  T  \mmember{}  Type
    H  n:\mBbbN{},  s:(\mBbbN{}n  {}\mrightarrow{}  T)  \mvdash{}  (B  n  s)  \mvee{}  (\mneg{}(B  n  s))
    H  a:(\mBbbN{}  {}\mrightarrow{}  T)  \mvdash{}  \mdownarrow{}\mexists{}n:\mBbbN{}.  (B  n  a)
    H  n:\mBbbN{},  s:(\mBbbN{}n  {}\mrightarrow{}  T),  x:B  n  s  \mvdash{}  f  n  s  \mmember{}  X  n  s
    H  n:\mBbbN{},  s:(\mBbbN{}n  {}\mrightarrow{}  T),  x:(\mforall{}t:T
                                                          (f  (n  +  1)  (\mlambda{}m.if  m=n  then  t  else  (s  m))  \mmember{}  X  (n  +  1) 
                                                                                                                                                (\mlambda{}m.if  m=n
                                                                                                                                                        then  t
                                                                                                                                                        else  (s  m))))
          \mvdash{}  f  n  s  \mmember{}  X  n  s


Date html generated: 2019_06_20-PM-04_12_20
Last ObjectModification: 2015_11_25-PM-03_37_51

Theory : rules


Home Index