Nuprl Rule : strong_bar_Induction

H  ⊢ f 0 c ∈ X 0 c

  BY strong_bar_Induction T R B !parameter{i:l} a s con x m n t ()
  
  H  ⊢ T ∈ Type
  H n:ℕ, s:(ℕn ⟶ T), t:T ⊢ R n s t ∈ Type
  H n:ℕ, s:(ℕn ⟶ T), con:(∀x:ℕn. (R x s (s x))) ⊢ (B n s) ∨ (¬(B n s))
  H a:(ℕ ⟶ T), con:(∀n:ℕ. (R n a (a n))) ⊢ ↓∃n:ℕ. (B n a)
  H n:ℕ, s:(ℕn ⟶ T), con:(∀x:ℕn. (R x s (s x))), m:B n s ⊢ f n s ∈ X n s
  H n:ℕ, s:(ℕn ⟶ T), con:(∀x:ℕn. (R x s (s x))), x:(∀t:{t:T| R n s 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 :  lambda: λx.A[x],  natural_number: $n,  add: n + m,  apply: f a,  int_eq: if a=b then c else d,  member: t ∈ T,  set: {x:A| B[x]} ,  all: ∀x:A. B[x],  int_seg: {i..j-},  function: x:A ⟶ B[x],  nat: ℕ,  axiom: Ax,  exists: ∃x:A. B[x],  squash: ↓T,  not: ¬A,  or: P ∨ Q,  universe: Type
Latex:
H    \mvdash{}  f  0  c  \mmember{}  X  0  c

    BY  strong\_bar\_Induction  T  R  B  !parameter\{i:l\}  a  s  con  x  m  n  t  ()
   
    H    \mvdash{}  T  \mmember{}  Type
    H  n:\mBbbN{},  s:(\mBbbN{}n  {}\mrightarrow{}  T),  t:T  \mvdash{}  R  n  s  t  \mmember{}  Type
    H  n:\mBbbN{},  s:(\mBbbN{}n  {}\mrightarrow{}  T),  con:(\mforall{}x:\mBbbN{}n.  (R  x  s  (s  x)))  \mvdash{}  (B  n  s)  \mvee{}  (\mneg{}(B  n  s))
    H  a:(\mBbbN{}  {}\mrightarrow{}  T),  con:(\mforall{}n:\mBbbN{}.  (R  n  a  (a  n)))  \mvdash{}  \mdownarrow{}\mexists{}n:\mBbbN{}.  (B  n  a)
    H  n:\mBbbN{},  s:(\mBbbN{}n  {}\mrightarrow{}  T),  con:(\mforall{}x:\mBbbN{}n.  (R  x  s  (s  x))),  m:B  n  s  \mvdash{}  f  n  s  \mmember{}  X  n  s
    H  n:\mBbbN{},  s:(\mBbbN{}n  {}\mrightarrow{}  T),  con:(\mforall{}x:\mBbbN{}n.  (R  x  s  (s  x))),  x:(\mforall{}t:\{t:T|  R  n  s  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_03
Last ObjectModification: 2015_11_25-PM-03_37_51

Theory : rules


Home Index