Nuprl Lemma : mFOLRule-induction
∀[P:mFOLRule() ─→ ℙ]
  (P[andI]
  
⇒ P[impI]
  
⇒ (∀var:ℤ. P[allI with var])
  
⇒ (∀var:ℤ. P[existsI with var])
  
⇒ (∀left:𝔹. P[mRuleorI(left)])
  
⇒ P[hyp]
  
⇒ (∀hypnum:ℕ. P[andE on hypnum])
  
⇒ (∀hypnum:ℕ. P[orE on hypnum])
  
⇒ (∀hypnum:ℕ. P[impE on hypnum])
  
⇒ (∀hypnum:ℕ. ∀var:ℤ.  P[allE on hypnum with var])
  
⇒ (∀hypnum:ℕ. ∀var:ℤ.  P[existsE on hypnum with var])
  
⇒ {∀v:mFOLRule(). P[v]})
Proof
Definitions occuring in Statement : 
mRuleexistsE: existsE on hypnum with var
, 
mRuleallE: allE on hypnum with var
, 
mRuleimpE: impE on hypnum
, 
mRuleorE: orE on hypnum
, 
mRuleandE: andE on hypnum
, 
mRulehyp: hyp
, 
mRuleorI: mRuleorI(left)
, 
mRuleexistsI: existsI with var
, 
mRuleallI: allI with var
, 
mRuleimpI: impI
, 
mRuleandI: andI
, 
mFOLRule: mFOLRule()
, 
nat: ℕ
, 
bool: 𝔹
, 
uall: ∀[x:A]. B[x]
, 
prop: ℙ
, 
guard: {T}
, 
so_apply: x[s]
, 
all: ∀x:A. B[x]
, 
implies: P 
⇒ Q
, 
function: x:A ─→ B[x]
, 
int: ℤ
Lemmas : 
mFOLRule-ext, 
eq_atom_wf, 
bool_wf, 
eqtt_to_assert, 
assert_of_eq_atom, 
subtype_base_sq, 
atom_subtype_base, 
unit_wf2, 
unit_subtype_base, 
it_wf, 
eqff_to_assert, 
equal_wf, 
bool_cases_sqequal, 
bool_subtype_base, 
assert-bnot, 
neg_assert_of_eq_atom, 
mFOLRule_wf
\mforall{}[P:mFOLRule()  {}\mrightarrow{}  \mBbbP{}]
    (P[andI]
    {}\mRightarrow{}  P[impI]
    {}\mRightarrow{}  (\mforall{}var:\mBbbZ{}.  P[allI  with  var])
    {}\mRightarrow{}  (\mforall{}var:\mBbbZ{}.  P[existsI  with  var])
    {}\mRightarrow{}  (\mforall{}left:\mBbbB{}.  P[mRuleorI(left)])
    {}\mRightarrow{}  P[hyp]
    {}\mRightarrow{}  (\mforall{}hypnum:\mBbbN{}.  P[andE  on  hypnum])
    {}\mRightarrow{}  (\mforall{}hypnum:\mBbbN{}.  P[orE  on  hypnum])
    {}\mRightarrow{}  (\mforall{}hypnum:\mBbbN{}.  P[impE  on  hypnum])
    {}\mRightarrow{}  (\mforall{}hypnum:\mBbbN{}.  \mforall{}var:\mBbbZ{}.    P[allE  on  hypnum  with  var])
    {}\mRightarrow{}  (\mforall{}hypnum:\mBbbN{}.  \mforall{}var:\mBbbZ{}.    P[existsE  on  hypnum  with  var])
    {}\mRightarrow{}  \{\mforall{}v:mFOLRule().  P[v]\})
Date html generated:
2015_07_17-AM-07_56_13
Last ObjectModification:
2015_01_27-AM-10_05_58
Home
Index