### Nuprl Lemma : indexed-F-bisimulation_wf

`∀[I:Type]. ∀[F:Type ⟶ Type]. ∀[R:(I ⟶ corec(T.F[T])) ⟶ (I ⟶ corec(T.F[T])) ⟶ ℙ].`
`  x,y.R[x;y] is an T.F[T]-bisimulation (indexed I) ∈ ℙ' supposing ContinuousMonotone(T.F[T])`

Proof

Definitions occuring in Statement :  indexed-F-bisimulation: `x,y.R[x; y] is an T.F[T]-bisimulation (indexed I)` corec: `corec(T.F[T])` continuous-monotone: `ContinuousMonotone(T.F[T])` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` so_apply: `x[s]` member: `t ∈ T` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` so_lambda: `λ2x.t[x]` so_apply: `x[s]` indexed-F-bisimulation: `x,y.R[x; y] is an T.F[T]-bisimulation (indexed I)` implies: `P `` Q` prop: `ℙ` and: `P ∧ Q` subtype_rel: `A ⊆r B` so_apply: `x[s1;s2]` guard: `{T}` continuous-monotone: `ContinuousMonotone(T.F[T])` type-monotone: `Monotone(T.F[T])` type-continuous: `Continuous(T.F[T])`
Lemmas referenced :  corec-ext all_wf subtype_rel_wf corec_wf subtype_rel_self equal_wf subtype_rel_transitivity subtype_rel_weakening continuous-monotone_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin sqequalRule lambdaEquality applyEquality hypothesisEquality universeEquality independent_isectElimination hypothesis instantiate functionEquality productEquality functionExtensionality because_Cache cumulativity productElimination axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality

Latex:
\mforall{}[I:Type].  \mforall{}[F:Type  {}\mrightarrow{}  Type].  \mforall{}[R:(I  {}\mrightarrow{}  corec(T.F[T]))  {}\mrightarrow{}  (I  {}\mrightarrow{}  corec(T.F[T]))  {}\mrightarrow{}  \mBbbP{}].
x,y.R[x;y]  is  an  T.F[T]-bisimulation  (indexed  I)  \mmember{}  \mBbbP{}'  supposing  ContinuousMonotone(T.F[T])

Date html generated: 2019_06_20-PM-00_37_17
Last ObjectModification: 2018_08_01-AM-10_46_04

Theory : co-recursion

Home Index