Nuprl Lemma : mFO-dest-atomic_wf

[T:Type]. ∀[F:Atom ─→ (ℤ List) ─→ (T?)]. ∀[fmla:mFOL()].  (let nm,vars dest-atomic(fmla) inF[nm;vars] ∈ T?)


Proof




Definitions occuring in Statement :  mFO-dest-atomic: mFO-dest-atomic mFOL: mFOL() list: List uall: [x:A]. B[x] so_apply: x[s1;s2] unit: Unit member: t ∈ T function: x:A ─→ B[x] union: left right int: atom: Atom universe: Type
Lemmas :  mFOatomic?_wf bool_wf eqtt_to_assert mFOatomic-name_wf mFOatomic-vars_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot it_wf mFOL_wf list_wf unit_wf2
\mforall{}[T:Type].  \mforall{}[F:Atom  {}\mrightarrow{}  (\mBbbZ{}  List)  {}\mrightarrow{}  (T?)].  \mforall{}[fmla:mFOL()].
    (let  nm,vars  =  dest-atomic(fmla)  in
      F[nm;vars]  \mmember{}  T?)



Date html generated: 2015_07_17-AM-07_53_58
Last ObjectModification: 2015_01_27-AM-10_06_44

Home Index