---

Step * 1 1 of Lemma indexed-coinduction-principle

.....assertion..... 
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)
⊢ ∀n:ℕ. ∀[x,y:I ⟶ corec(T.F[T])].  x = y ∈ (I ⟶ primrec(n;Top;λ,T. F[T])) supposing R[x;y]
BY
{ (InductionOnNat
   THEN Reduce 0
   THEN Auto
   THEN Ext
   THEN Auto
   THEN RenameVar `i' (-1)
   THEN Try (((D 0 THEN Auto) THEN With ⌜n⌝ (D (-1))⋅ THEN Auto))) }

1
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 : ℤ
7. 0 < n
8. ∀[x,y:I ⟶ corec(T.F[T])].  x = y ∈ (I ⟶ primrec(n - 1;Top;λ,T. F[T])) supposing R[x;y]
9. x : I ⟶ corec(T.F[T])
10. y : I ⟶ corec(T.F[T])
11. R[x;y]
12. i : I
⊢ (x i) = (y i) ∈ primrec(n;Top;λ,T. F[T])

---

Latex:

---

Latex:
.....assertion..... 
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)
\mvdash{}  \mforall{}n:\mBbbN{}.  \mforall{}[x,y:I  {}\mrightarrow{}  corec(T.F[T])].    x  =  y  supposing  R[x;y]


By

---

Latex:
(InductionOnNat
  THEN  Reduce  0
  THEN  Auto
  THEN  Ext
  THEN  Auto
  THEN  RenameVar  `i'  (-1)
  THEN  Try  (((D  0  THEN  Auto)  THEN  With  \mkleeneopen{}n\mkleeneclose{}  (D  (-1))\mcdot{}  THEN  Auto)))

---

Home Index