### Nuprl Lemma : mFOL-sequent-evidence_transitivity1

`From uniform evidence that hyps `` x and uniform evidence that x `` 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>))`

Proof

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: `T List` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` 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