Nuprl Lemma : mFOL-sequent-evidence_transitivity1

From uniform evidence that hyps  and uniform evidence that  y
we construct uniform evidence that hyps  y.⋅

[hyps:mFOL() List]. ∀[x,y:mFOL()].
  ((∀[Dom:Type]. ∀[S:FOStruct(Dom)].
      ∀a:FOAssignment(Dom). (Dom,S,a |= mFOL-abstract(x)  Dom,S,a |= mFOL-abstract(y)))
   mFOL-sequent-evidence(<hyps, x>)
   mFOL-sequent-evidence(<hyps, y>))


Definitions occuring in Statement :  mFOL-sequent-evidence: mFOL-sequent-evidence(s) mFOL-abstract: mFOL-abstract(fmla) mFOL: mFOL() FOSatWith: Dom,S,a |= fmla FOStruct: FOStruct(Dom) FOAssignment: FOAssignment(Dom) list: List uall: [x:A]. B[x] all: x:A. B[x] implies:  Q pair: <a, b> universe: Type
Lemmas :  tuple-type_wf map_wf mFOL_wf FOSatWith_wf mFOL-abstract_wf FOAssignment_wf FOStruct_wf mFOL-sequent-evidence_wf list_wf uall_wf all_wf
\mforall{}[hyps:mFOL()  List].  \mforall{}[x,y:mFOL()].
    ((\mforall{}[Dom:Type].  \mforall{}[S:FOStruct(Dom)].
            \mforall{}a:FOAssignment(Dom).  (Dom,S,a  |=  mFOL-abstract(x)  {}\mRightarrow{}  Dom,S,a  |=  mFOL-abstract(y)))
    {}\mRightarrow{}  mFOL-sequent-evidence(<hyps,  x>)
    {}\mRightarrow{}  mFOL-sequent-evidence(<hyps,  y>))

Date html generated: 2015_07_17-AM-07_56_37
Last ObjectModification: 2015_01_27-AM-10_05_19

Home Index