---

Step * 1 2 of Lemma indexed-coinduction-principle


1. I : Type
2. F : Type ⟶ Type
3. ContinuousMonotone(T.F[T])
4. R : (I ⟶ corec(T.F[T])) ⟶ (I ⟶ corec(T.F[T])) ⟶ ℙ
5. x,y.R[x;y] is an T.F[T]-bisimulation (indexed I)
6. ∀n:ℕ. ∀[x,y:I ⟶ corec(T.F[T])].  x = y ∈ (I ⟶ primrec(n;Top;λ,T. F[T])) supposing R[x;y]
⊢ ∀[x,y:I ⟶ corec(T.F[T])].  x = y ∈ (I ⟶ corec(T.F[T])) supposing R[x;y]
BY
{ (Auto
   THEN (Ext THEN Auto)
   THEN RenameVar `i' (-1)
   THEN Unfold `corec` 0
   THEN MemTypeCD
   THEN Auto
   THEN InstHyp [⌜n⌝;⌜x⌝;⌜y⌝] 6⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  Type
2.  F  :  Type  {}\mrightarrow{}  Type
3.  ContinuousMonotone(T.F[T])
4.  R  :  (I  {}\mrightarrow{}  corec(T.F[T]))  {}\mrightarrow{}  (I  {}\mrightarrow{}  corec(T.F[T]))  {}\mrightarrow{}  \mBbbP{}
5.  x,y.R[x;y]  is  an  T.F[T]-bisimulation  (indexed  I)
6.  \mforall{}n:\mBbbN{}.  \mforall{}[x,y:I  {}\mrightarrow{}  corec(T.F[T])].    x  =  y  supposing  R[x;y]
\mvdash{}  \mforall{}[x,y:I  {}\mrightarrow{}  corec(T.F[T])].    x  =  y  supposing  R[x;y]


By

---

Latex:
(Auto
  THEN  (Ext  THEN  Auto)
  THEN  RenameVar  `i'  (-1)
  THEN  Unfold  `corec`  0
  THEN  MemTypeCD
  THEN  Auto
  THEN  InstHyp  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]  6\mcdot{}
  THEN  Auto)

---

Home Index