Nuprl Lemma : mFOLRule-definition

[A:Type]. ∀[R:A ─→ mFOLRule() ─→ ℙ].
  ({x:A| R[x;andI]} 
   {x:A| R[x;impI]} 
   (∀var:ℤ{x:A| R[x;allI with var]} )
   (∀var:ℤ{x:A| R[x;existsI with var]} )
   (∀left:𝔹{x:A| R[x;mRuleorI(left)]} )
   {x:A| R[x;hyp]} 
   (∀hypnum:ℕ{x:A| R[x;andE on hypnum]} )
   (∀hypnum:ℕ{x:A| R[x;orE on hypnum]} )
   (∀hypnum:ℕ{x:A| R[x;impE on hypnum]} )
   (∀hypnum:ℕ. ∀var:ℤ.  {x:A| R[x;allE on hypnum with var]} )
   (∀hypnum:ℕ. ∀var:ℤ.  {x:A| R[x;existsE on hypnum with var]} )
   {∀v:mFOLRule(). {x:A| R[x;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[s1;s2] all: x:A. B[x] implies:  Q set: {x:A| B[x]}  function: x:A ─→ B[x] int: universe: Type
Lemmas :  mFOLRule-induction set_wf mFOLRule_wf all_wf nat_wf mRuleexistsE_wf mRuleallE_wf mRuleimpE_wf mRuleorE_wf mRuleandE_wf mRulehyp_wf bool_wf mRuleorI_wf mRuleexistsI_wf mRuleallI_wf mRuleimpI_wf mRuleandI_wf
\mforall{}[A:Type].  \mforall{}[R:A  {}\mrightarrow{}  mFOLRule()  {}\mrightarrow{}  \mBbbP{}].
    (\{x:A|  R[x;andI]\} 
    {}\mRightarrow{}  \{x:A|  R[x;impI]\} 
    {}\mRightarrow{}  (\mforall{}var:\mBbbZ{}.  \{x:A|  R[x;allI  with  var]\}  )
    {}\mRightarrow{}  (\mforall{}var:\mBbbZ{}.  \{x:A|  R[x;existsI  with  var]\}  )
    {}\mRightarrow{}  (\mforall{}left:\mBbbB{}.  \{x:A|  R[x;mRuleorI(left)]\}  )
    {}\mRightarrow{}  \{x:A|  R[x;hyp]\} 
    {}\mRightarrow{}  (\mforall{}hypnum:\mBbbN{}.  \{x:A|  R[x;andE  on  hypnum]\}  )
    {}\mRightarrow{}  (\mforall{}hypnum:\mBbbN{}.  \{x:A|  R[x;orE  on  hypnum]\}  )
    {}\mRightarrow{}  (\mforall{}hypnum:\mBbbN{}.  \{x:A|  R[x;impE  on  hypnum]\}  )
    {}\mRightarrow{}  (\mforall{}hypnum:\mBbbN{}.  \mforall{}var:\mBbbZ{}.    \{x:A|  R[x;allE  on  hypnum  with  var]\}  )
    {}\mRightarrow{}  (\mforall{}hypnum:\mBbbN{}.  \mforall{}var:\mBbbZ{}.    \{x:A|  R[x;existsE  on  hypnum  with  var]\}  )
    {}\mRightarrow{}  \{\mforall{}v:mFOLRule().  \{x:A|  R[x;v]\}  \})



Date html generated: 2015_07_17-AM-07_56_15
Last ObjectModification: 2015_01_27-AM-10_05_29

Home Index