Nuprl Lemma : mFOLRule-induction

[P:mFOLRule() ─→ ℙ]
   (∀var:ℤP[allI with var])
   (∀var:ℤP[existsI with var])
   (∀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]})


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:  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{}]
    {}\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