Nuprl Lemma : mFOL_case_wf

∀[T:Type]. ∀[v:mFOL()]. ∀[atomic:name:Atom ⟶ vars:(ℤ List) ⟶ T]. ∀[connect:knd:Atom
                                                                             ⟶ left:mFOL()
                                                                             ⟶ right:mFOL()
                                                                             ⟶ T]. ∀[quant:isall:𝔹
                                                                                            ⟶ var:ℤ
                                                                                            ⟶ body:mFOL()
                                                                                            ⟶ T].
  (case(v)
   name(vars) => atomic[name;vars];
   left knd right => connect[knd;left;right];
   isall var.body => quant[isall;var;body] ∈ T)


Proof



Definitions occuring in Statement :  mFOL_case: mFOL_case,  mFOL: mFOL(),  list: T List,  bool: 𝔹,  uall: ∀[x:A]. B[x],  so_apply: x[s1;s2;s3],  so_apply: x[s1;s2],  member: t ∈ T,  function: x:A ⟶ B[x],  int: ℤ,  atom: Atom,  universe: Type
Definitions unfolded in proof :  ext-eq: A ≡ B,  and: P ∧ Q,  member: t ∈ T,  subtype_rel: A ⊆r B,  uall: ∀[x:A]. B[x],  all: ∀x:A. B[x],  implies: P ⇒ Q,  bool: 𝔹,  unit: Unit,  it: ⋅,  btrue: tt,  uiff: uiff(P;Q),  uimplies: b supposing a,  sq_type: SQType(T),  guard: {T},  eq_atom: x =a y,  ifthenelse: if b then t else f fi ,  mFOatomic: name(vars),  mFOconnect?: mFOconnect?(v),  pi1: fst(t),  assert: ↑b,  bfalse: ff,  mFOatomic?: mFOatomic?(v),  mFOquant?: mFOquant?(v),  not: ¬A,  true: True,  false: False,  exists: ∃x:A. B[x],  or: P ∨ Q,  bnot: ¬bb,  mFOconnect: mFOconnect(knd;left;right),  mFOquant: mFOquant(isall;var;body),  mFOL_case: mFOL_case,  so_apply: x[s1;s2],  so_apply: x[s1;s2;s3]
Lemmas referenced :  mFOL-ext,  eq_atom_wf,  eqtt_to_assert,  assert_of_eq_atom,  subtype_base_sq,  atom_subtype_base,  eqff_to_assert,  bool_cases_sqequal,  bool_wf,  bool_subtype_base,  assert-bnot,  neg_assert_of_eq_atom,  mFOatomic?_wf,  mFOatomic-name_wf,  mFOatomic-vars_wf,  uiff_transitivity,  equal-wf-T-base,  assert_wf,  bnot_wf,  not_wf,  assert_of_bnot,  mFOconnect?_wf,  mFOconnect-knd_wf,  mFOconnect-left_wf,  mFOconnect-right_wf,  mFOquant-isall_wf,  mFOquant-var_wf,  mFOquant-body_wf,  istype-int,  istype-atom,  list_wf,  mFOL_wf,  istype-universe
Rules used in proof :  cut,  introduction,  extract_by_obid,  promote_hyp,  sqequalHypSubstitution,  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  productElimination,  thin,  hypothesis_subsumption,  hypothesis,  hypothesisEquality,  applyEquality,  sqequalRule,  isectElimination,  tokenEquality,  inhabitedIsType,  lambdaFormation_alt,  unionElimination,  equalityElimination,  equalityTransitivity,  equalitySymmetry,  independent_isectElimination,  instantiate,  cumulativity,  atomEquality,  dependent_functionElimination,  independent_functionElimination,  because_Cache,  natural_numberEquality,  voidElimination,  dependent_pairFormation_alt,  equalityIstype,  isect_memberFormation_alt,  baseClosed,  axiomEquality,  functionIsType,  universeIsType,  isect_memberEquality_alt,  isectIsTypeImplies,  intEquality,  universeEquality
Latex:
\mforall{}[T:Type].  \mforall{}[v:mFOL()].  \mforall{}[atomic:name:Atom  {}\mrightarrow{}  vars:(\mBbbZ{}  List)  {}\mrightarrow{}  T].  \mforall{}[connect:knd:Atom
                                                                                                                                                          {}\mrightarrow{}  left:mFOL()
                                                                                                                                                          {}\mrightarrow{}  right:mFOL()
                                                                                                                                                          {}\mrightarrow{}  T].
\mforall{}[quant:isall:\mBbbB{}  {}\mrightarrow{}  var:\mBbbZ{}  {}\mrightarrow{}  body:mFOL()  {}\mrightarrow{}  T].
    (case(v)
      name(vars)  =>  atomic[name;vars];
      left  knd  right  =>  connect[knd;left;right];
      isall  var.body  =>  quant[isall;var;body]  \mmember{}  T)


Date html generated: 2019_10_16-AM-11_38_59
Last ObjectModification: 2018_11_26-PM-03_09_48

Theory : minimal-first-order-logic


Home Index