Nuprl Lemma : mFOLRule_ind_wf

∀[A:Type]. ∀[R:A ─→ mFOLRule() ─→ ℙ]. ∀[v:mFOLRule()]. ∀[andI:{x:A| R[x;andI]} ]. ∀[impI:{x:A| R[x;impI]} ].
∀[allI:var:ℤ ─→ {x:A| R[x;allI with var]} ]. ∀[existsI:var:ℤ ─→ {x:A| R[x;existsI with var]} ].
∀[orI:left:𝔹 ─→ {x:A| R[x;mRuleorI(left)]} ]. ∀[hyp:{x:A| R[x;hyp]} ]. ∀[andE:hypnum:ℕ ─→ {x:A| R[x;andE on hypnum]} ].
∀[orE:hypnum:ℕ ─→ {x:A| R[x;orE on hypnum]} ]. ∀[impE:hypnum:ℕ ─→ {x:A| R[x;impE on hypnum]} ].
∀[allE:hypnum:ℕ ─→ var:ℤ ─→ {x:A| R[x;allE on hypnum with var]} ]. ∀[existsE:hypnum:ℕ
                                                                            ─→ var:ℤ
                                                                            ─→ {x:A| R[x;existsE on hypnum with var]} ].
  (mFOLRule_ind(v;
   andI;
   impI;
   var.allI[var];
   var.existsI[var];
   left.orI[left];
   hyp;hypnum.andE[hypnum];
   hypnum.orE[hypnum];
   hypnum.impE[hypnum];
   hypnum,var.allE[hypnum;var];
   hypnum,var.existsE[hypnum;var]) ∈ {x:A| R[x;v]} )


Proof



Definitions occuring in Statement :  mFOLRule_ind: mFOLRule_ind,  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: ℙ,  so_apply: x[s1;s2],  so_apply: x[s],  member: t ∈ T,  set: {x:A| B[x]} ,  function: x:A ─→ B[x],  int: ℤ,  universe: Type
Lemmas :  top_wf,  has-value_wf_base,  lifting-strict-atom_eq,  base_wf,  mRuleandI_wf,  mRuleimpI_wf,  mRuleallI_wf,  mRuleexistsI_wf,  bool_wf,  mRuleorI_wf,  mRulehyp_wf,  nat_wf,  mRuleandE_wf,  mRuleorE_wf,  mRuleimpE_wf,  mRuleallE_wf,  mRuleexistsE_wf,  mFOLRule_wf,  all_wf,  set_wf,  subtype_rel-equal
\mforall{}[A:Type].  \mforall{}[R:A  {}\mrightarrow{}  mFOLRule()  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[v:mFOLRule()].  \mforall{}[andI:\{x:A|  R[x;andI]\}  ].  \mforall{}[impI:\{x:A| 
                                                                                                                                                                                  R
                                                                                                                                                                                  [x;impI]\}  ]\000C.
\mforall{}[allI:var:\mBbbZ{}  {}\mrightarrow{}  \{x:A|  R[x;allI  with  var]\}  ].  \mforall{}[existsI:var:\mBbbZ{}  {}\mrightarrow{}  \{x:A|  R[x;existsI  with  var]\}  ].
\mforall{}[orI:left:\mBbbB{}  {}\mrightarrow{}  \{x:A|  R[x;mRuleorI(left)]\}  ].  \mforall{}[hyp:\{x:A|  R[x;hyp]\}  ].
\mforall{}[andE:hypnum:\mBbbN{}  {}\mrightarrow{}  \{x:A|  R[x;andE  on  hypnum]\}  ].  \mforall{}[orE:hypnum:\mBbbN{}  {}\mrightarrow{}  \{x:A|  R[x;orE  on  hypnum]\}  ].
\mforall{}[impE:hypnum:\mBbbN{}  {}\mrightarrow{}  \{x:A|  R[x;impE  on  hypnum]\}  ].  \mforall{}[allE:hypnum:\mBbbN{}
                                                                                                              {}\mrightarrow{}  var:\mBbbZ{}
                                                                                                              {}\mrightarrow{}  \{x:A|  R[x;allE  on  hypnum  with  var]\}  ].
\mforall{}[existsE:hypnum:\mBbbN{}  {}\mrightarrow{}  var:\mBbbZ{}  {}\mrightarrow{}  \{x:A|  R[x;existsE  on  hypnum  with  var]\}  ].
    (mFOLRule\_ind(v;
      andI;
      impI;
      var.allI[var];
      var.existsI[var];
      left.orI[left];
      hyp;hypnum.andE[hypnum];
      hypnum.orE[hypnum];
      hypnum.impE[hypnum];
      hypnum,var.allE[hypnum;var];
      hypnum,var.existsE[hypnum;var])  \mmember{}  \{x:A|  R[x;v]\}  )


Date html generated: 2015_07_17-AM-07_56_19
Last ObjectModification: 2015_01_29-PM-04_41_11

Home Index