Nuprl Lemma : mFOLco-ext

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


Proof



Definitions occuring in Statement :  mFOLco: mFOLco(),  list: T List,  ifthenelse: if b then t else f fi ,  eq_atom: x =a y,  bool: 𝔹,  ext-eq: A ≡ B,  product: x:A × B[x],  int: ℤ,  token: "$token",  atom: Atom,  void: Void
Definitions unfolded in proof :  mFOLco: mFOLco(),  uall: ∀[x:A]. B[x],  so_lambda: λ2x.t[x],  member: t ∈ T,  so_apply: x[s],  uimplies: b supposing a,  continuous-monotone: ContinuousMonotone(T.F[T]),  and: P ∧ Q,  type-monotone: Monotone(T.F[T]),  subtype_rel: A ⊆r B,  all: ∀x:A. B[x],  implies: P ⇒ Q,  bool: 𝔹,  unit: Unit,  it: ⋅,  btrue: tt,  uiff: uiff(P;Q),  ifthenelse: if b then t else f fi ,  bfalse: ff,  exists: ∃x:A. B[x],  prop: ℙ,  or: P ∨ Q,  sq_type: SQType(T),  guard: {T},  bnot: ¬bb,  assert: ↑b,  false: False,  so_lambda: λ2x y.t[x; y],  so_apply: x[s1;s2],  strong-type-continuous: Continuous+(T.F[T]),  type-continuous: Continuous(T.F[T])
Lemmas referenced :  corec-ext,  ifthenelse_wf,  eq_atom_wf,  list_wf,  bool_wf,  subtype_rel_product,  eqtt_to_assert,  assert_of_eq_atom,  subtype_rel_self,  eqff_to_assert,  equal_wf,  bool_cases_sqequal,  subtype_base_sq,  bool_subtype_base,  assert-bnot,  neg_assert_of_eq_atom,  subtype_rel_wf,  strong-continuous-depproduct,  continuous-constant,  strong-continuous-product,  continuous-id,  subtype_rel_weakening,  nat_wf
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  cut,  introduction,  extract_by_obid,  sqequalHypSubstitution,  isectElimination,  thin,  sqequalRule,  lambdaEquality,  productEquality,  atomEquality,  instantiate,  hypothesisEquality,  tokenEquality,  hypothesis,  universeEquality,  intEquality,  cumulativity,  voidEquality,  independent_isectElimination,  independent_pairFormation,  isect_memberFormation,  because_Cache,  lambdaFormation,  unionElimination,  equalityElimination,  productElimination,  dependent_pairFormation,  equalityTransitivity,  equalitySymmetry,  promote_hyp,  dependent_functionElimination,  independent_functionElimination,  voidElimination,  axiomEquality,  isect_memberEquality,  isectEquality,  applyEquality,  functionExtensionality,  functionEquality
Latex:
mFOLco()  \mequiv{}  lbl:Atom  \mtimes{}  if  lbl  =a  "atomic"  then  name:Atom  \mtimes{}  (\mBbbZ{}  List)
                                            if  lbl  =a  "connect"  then  knd:Atom  \mtimes{}  left:mFOLco()  \mtimes{}  mFOLco()
                                            if  lbl  =a  "quant"  then  isall:\mBbbB{}  \mtimes{}  var:\mBbbZ{}  \mtimes{}  mFOLco()
                                            else  Void
                                            fi 


Date html generated: 2018_05_21-PM-10_20_44
Last ObjectModification: 2017_07_26-PM-06_37_35

Theory : minimal-first-order-logic


Home Index