Nuprl Lemma : test-model

[Dom:Type]. ∀[A,B:Dom ⟶ ℙ]. ∀[R:Dom ⟶ Dom ⟶ ℙ].
  ((∀x:Dom. ∃y:Dom. (R[x;y] ∧ (A[y] ∨ B[y])))
   (∀x,y,z:Dom.  ((R[x;y] ∧ R[x;z] ∧ A[y] ∧ A[z])  A[x]))
   (∀x,y,z:Dom.  ((R[x;y] ∧ R[x;z] ∧ B[y] ∧ B[z])  A[x]))
   (∀x:Dom. A[x]))


Proof




Definitions occuring in Statement :  uall: [x:A]. B[x] prop: so_apply: x[s1;s2] so_apply: x[s] all: x:A. B[x] exists: x:A. B[x] implies:  Q or: P ∨ Q and: P ∧ Q function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] implies:  Q all: x:A. B[x] member: t ∈ T exists: x:A. B[x] and: P ∧ Q or: P ∨ Q prop: so_lambda: λ2x.t[x] so_apply: x[s1;s2] so_apply: x[s]
Lemmas referenced :  all_wf and_wf exists_wf or_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation rename cut hypothesis sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality productElimination unionElimination because_Cache independent_functionElimination independent_pairFormation lemma_by_obid isectElimination sqequalRule lambdaEquality functionEquality applyEquality cumulativity universeEquality

Latex:
\mforall{}[Dom:Type].  \mforall{}[A,B:Dom  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[R:Dom  {}\mrightarrow{}  Dom  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}x:Dom.  \mexists{}y:Dom.  (R[x;y]  \mwedge{}  (A[y]  \mvee{}  B[y])))
    {}\mRightarrow{}  (\mforall{}x,y,z:Dom.    ((R[x;y]  \mwedge{}  R[x;z]  \mwedge{}  A[y]  \mwedge{}  A[z])  {}\mRightarrow{}  A[x]))
    {}\mRightarrow{}  (\mforall{}x,y,z:Dom.    ((R[x;y]  \mwedge{}  R[x;z]  \mwedge{}  B[y]  \mwedge{}  B[z])  {}\mRightarrow{}  A[x]))
    {}\mRightarrow{}  (\mforall{}x:Dom.  A[x]))



Date html generated: 2016_05_15-PM-03_19_25
Last ObjectModification: 2015_12_27-PM-01_03_52

Theory : general


Home Index