Nuprl Lemma : mFOL-ext

mFOL() ≡ lbl:Atom × if lbl =a "atomic" then name:Atom × (ℤ List)
                    if lbl =a "connect" then knd:Atom × left:mFOL() × mFOL()
                    if lbl =a "quant" then isall:𝔹 × var:ℤ × mFOL()
                    else Void
                    fi 


Proof




Definitions occuring in Statement :  mFOL: mFOL() list: List ifthenelse: if then else fi  eq_atom: =a y bool: 𝔹 ext-eq: A ≡ B product: x:A × B[x] int: token: "$token" atom: Atom void: Void
Lemmas :  mFOLco-ext eq_atom_wf bool_wf eqtt_to_assert assert_of_eq_atom subtype_base_sq atom_subtype_base list_wf eqff_to_assert equal_wf bool_cases_sqequal bool_subtype_base assert-bnot neg_assert_of_eq_atom value-type-has-value int-value-type has-value_wf-partial nat_wf set-value-type le_wf mFOLco_size_wf mFOL_wf mFOLco_wf add-nat false_wf mFOL_size_wf nat_properties
mFOL()  \mequiv{}  lbl:Atom  \mtimes{}  if  lbl  =a  "atomic"  then  name:Atom  \mtimes{}  (\mBbbZ{}  List)
                                        if  lbl  =a  "connect"  then  knd:Atom  \mtimes{}  left:mFOL()  \mtimes{}  mFOL()
                                        if  lbl  =a  "quant"  then  isall:\mBbbB{}  \mtimes{}  var:\mBbbZ{}  \mtimes{}  mFOL()
                                        else  Void
                                        fi 



Date html generated: 2015_07_17-AM-07_53_24
Last ObjectModification: 2015_01_29-PM-04_40_43

Home Index