Nuprl Lemma : mFOL_ind_wf_simple

[A:Type]. ∀[v:mFOL()]. ∀[atomic:name:Atom ─→ vars:(ℤ List) ─→ A]. ∀[connect:knd:Atom
                                                                             ─→ left:mFOL()
                                                                             ─→ right:mFOL()
                                                                             ─→ A
                                                                             ─→ A
                                                                             ─→ A]. ∀[quant:isall:𝔹
                                                                                            ─→ var:ℤ
                                                                                            ─→ body:mFOL()
                                                                                            ─→ A
                                                                                            ─→ A].
  (mFOL_ind(v;
            mFOatomic(name,vars) atomic[name;vars];
            mFOconnect(knd,left,right) rec1,rec2.connect[knd;left;right;rec1;rec2];
            mFOquant(isall,var,body) rec3.quant[isall;var;body;rec3])  ∈ A)


Proof




Definitions occuring in Statement :  mFOL_ind: mFOL_ind mFOL: mFOL() list: List bool: 𝔹 uall: [x:A]. B[x] so_apply: x[s1;s2;s3;s4;s5] so_apply: x[s1;s2;s3;s4] so_apply: x[s1;s2] member: t ∈ T function: x:A ─→ B[x] int: atom: Atom universe: Type
Lemmas :  mFOL_ind_wf true_wf mFOL_wf subtype_rel_dep_function list_wf set_wf bool_wf
\mforall{}[A:Type].  \mforall{}[v:mFOL()].  \mforall{}[atomic:name:Atom  {}\mrightarrow{}  vars:(\mBbbZ{}  List)  {}\mrightarrow{}  A].  \mforall{}[connect:knd:Atom
                                                                                                                                                          {}\mrightarrow{}  left:mFOL()
                                                                                                                                                          {}\mrightarrow{}  right:mFOL()
                                                                                                                                                          {}\mrightarrow{}  A
                                                                                                                                                          {}\mrightarrow{}  A
                                                                                                                                                          {}\mrightarrow{}  A].
\mforall{}[quant:isall:\mBbbB{}  {}\mrightarrow{}  var:\mBbbZ{}  {}\mrightarrow{}  body:mFOL()  {}\mrightarrow{}  A  {}\mrightarrow{}  A].
    (mFOL\_ind(v;
                        mFOatomic(name,vars){}\mRightarrow{}  atomic[name;vars];
                        mFOconnect(knd,left,right){}\mRightarrow{}  rec1,rec2.connect[knd;left;right;rec1;rec2];
                        mFOquant(isall,var,body){}\mRightarrow{}  rec3.quant[isall;var;body;rec3])    \mmember{}  A)



Date html generated: 2015_07_17-AM-07_53_52
Last ObjectModification: 2015_01_27-AM-10_06_48

Home Index