---

Step * 1 1 1 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 : ℤ
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])
BY
{ ((RWO "primrec-unroll" 0 THENA Auto) THEN AutoSplit)⋅ }

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

---

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.  n  :  \mBbbZ{}
7.  0  <  n
8.  \mforall{}[x,y:I  {}\mrightarrow{}  corec(T.F[T])].    x  =  y  supposing  R[x;y]
9.  x  :  I  {}\mrightarrow{}  corec(T.F[T])
10.  y  :  I  {}\mrightarrow{}  corec(T.F[T])
11.  R[x;y]
12.  i  :  I
\mvdash{}  (x  i)  =  (y  i)


By

---

Latex:
((RWO  "primrec-unroll"  0  THENA  Auto)  THEN  AutoSplit)\mcdot{}

---

Home Index