### Nuprl Lemma : formula-definition

`∀[A:Type]. ∀[R:A ⟶ formula() ⟶ ℙ].`
`  ((∀name:Atom. {x:A| R[x;pvar(name)]} )`
`  `` (∀sub:formula(). ({x:A| R[x;sub]}  `` {x:A| R[x;pnot(sub)]} ))`
`  `` (∀left,right:formula().  ({x:A| R[x;left]}  `` {x:A| R[x;right]}  `` {x:A| R[x;pand(left;right)]} ))`
`  `` (∀left,right:formula().  ({x:A| R[x;left]}  `` {x:A| R[x;right]}  `` {x:A| R[x;por(left;right)]} ))`
`  `` (∀left,right:formula().  ({x:A| R[x;left]}  `` {x:A| R[x;right]}  `` {x:A| R[x;pimp(left;right)]} ))`
`  `` {∀v:formula(). {x:A| R[x;v]} })`

Proof

Definitions occuring in Statement :  pimp: `pimp(left;right)` por: `por(left;right)` pand: `pand(left;right)` pnot: `pnot(sub)` pvar: `pvar(name)` formula: `formula()` uall: `∀[x:A]. B[x]` prop: `ℙ` guard: `{T}` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` implies: `P `` Q` set: `{x:A| B[x]} ` function: `x:A ⟶ B[x]` atom: `Atom` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` guard: `{T}` so_lambda: `λ2x.t[x]` member: `t ∈ T` so_apply: `x[s1;s2]` subtype_rel: `A ⊆r B` so_apply: `x[s]` prop: `ℙ`
Lemmas referenced :  formula-induction set_wf formula_wf all_wf pimp_wf por_wf pand_wf pnot_wf pvar_wf
Rules used in proof :  cut lemma_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation hypothesis sqequalHypSubstitution isectElimination thin sqequalRule lambdaEquality hypothesisEquality applyEquality because_Cache independent_functionElimination functionEquality universeEquality atomEquality cumulativity

Latex:
\mforall{}[A:Type].  \mforall{}[R:A  {}\mrightarrow{}  formula()  {}\mrightarrow{}  \mBbbP{}].
((\mforall{}name:Atom.  \{x:A|  R[x;pvar(name)]\}  )
{}\mRightarrow{}  (\mforall{}sub:formula().  (\{x:A|  R[x;sub]\}    {}\mRightarrow{}  \{x:A|  R[x;pnot(sub)]\}  ))
{}\mRightarrow{}  (\mforall{}left,right:formula().
(\{x:A|  R[x;left]\}    {}\mRightarrow{}  \{x:A|  R[x;right]\}    {}\mRightarrow{}  \{x:A|  R[x;pand(left;right)]\}  ))
{}\mRightarrow{}  (\mforall{}left,right:formula().
(\{x:A|  R[x;left]\}    {}\mRightarrow{}  \{x:A|  R[x;right]\}    {}\mRightarrow{}  \{x:A|  R[x;por(left;right)]\}  ))
{}\mRightarrow{}  (\mforall{}left,right:formula().
(\{x:A|  R[x;left]\}    {}\mRightarrow{}  \{x:A|  R[x;right]\}    {}\mRightarrow{}  \{x:A|  R[x;pimp(left;right)]\}  ))
{}\mRightarrow{}  \{\mforall{}v:formula().  \{x:A|  R[x;v]\}  \})

Date html generated: 2016_05_15-PM-07_11_39
Last ObjectModification: 2015_12_27-AM-11_32_34

Theory : general

Home Index