---

Step * 1 1 1 1 of Lemma coinduction-principle


1. F : Type ⟶ Type
2. ContinuousMonotone(T.F[T])
3. R : corec(T.F[T]) ⟶ corec(T.F[T]) ⟶ ℙ
4. x,y.R[x;y] is an T.F[T]-bisimulation
5. n : ℤ
6. n ≠ 0
7. 0 < n
8. ∀[x,y:corec(T.F[T])].  x = y ∈ primrec(n - 1;Top;λ,T. F[T]) supposing R[x;y]
9. x : corec(T.F[T])
10. y : corec(T.F[T])
11. R[x;y]
⊢ x = y ∈ F[primrec(n - 1;Top;λ,T. F[T])]
BY
{ TACTIC:(UnfoldTopAb 4 THEN InstHyp [⌜primrec(n - 1;Top;λ,T. F[T])⌝] 4⋅ THEN Try (Complete (Auto))) }

1
.....antecedent..... 
1. F : Type ⟶ Type
2. ContinuousMonotone(T.F[T])
3. R : corec(T.F[T]) ⟶ corec(T.F[T]) ⟶ ℙ
4. ∀T:Type
     (((F[T] ⊆r T) ∧ (corec(T.F[T]) ⊆r T))
     ⇒ (∀x,y:corec(T.F[T]).  (R[x;y] ⇒ (x = y ∈ T)))
     ⇒ (∀x,y:corec(T.F[T]).  (R[x;y] ⇒ (x = y ∈ F[T]))))
5. n : ℤ
6. n ≠ 0
7. 0 < n
8. ∀[x,y:corec(T.F[T])].  x = y ∈ primrec(n - 1;Top;λ,T. F[T]) supposing R[x;y]
9. x : corec(T.F[T])
10. y : corec(T.F[T])
11. R[x;y]
⊢ (F[primrec(n - 1;Top;λ,T. F[T])] ⊆r primrec(n - 1;Top;λ,T. F[T])) ∧ (corec(T.F[T]) ⊆r primrec(n - 1;Top;λ,T. F[T]))

---

Latex:

---

Latex:

1.  F  :  Type  {}\mrightarrow{}  Type
2.  ContinuousMonotone(T.F[T])
3.  R  :  corec(T.F[T])  {}\mrightarrow{}  corec(T.F[T])  {}\mrightarrow{}  \mBbbP{}
4.  x,y.R[x;y]  is  an  T.F[T]-bisimulation
5.  n  :  \mBbbZ{}
6.  n  \mneq{}  0
7.  0  <  n
8.  \mforall{}[x,y:corec(T.F[T])].    x  =  y  supposing  R[x;y]
9.  x  :  corec(T.F[T])
10.  y  :  corec(T.F[T])
11.  R[x;y]
\mvdash{}  x  =  y


By

---

Latex:
TACTIC:(UnfoldTopAb  4  THEN  InstHyp  [\mkleeneopen{}primrec(n  -  1;Top;\mlambda{},T.  F[T])\mkleeneclose{}]  4\mcdot{}  THEN  Try  (Complete  (Auto)))

---

Home Index