Step
*
1
of Lemma
equiv-on-corec
1. F : Type ⟶ Type
2. ContinuousMonotone(T.F[T])
3. G : ⋂T:Type. ((T ⟶ T ⟶ ℙ) ⟶ F[T] ⟶ F[T] ⟶ ℙ)
4. ∀T:Type. ∀E:T ⟶ T ⟶ ℙ. (EquivRel(T;x,y.E x y)
⇒ EquivRel(F[T];x,y.G E x y))
5. ∀n:ℕ. (G^n (λx,y. True) ∈ primrec(n;Top;λ,T. F[T]) ⟶ primrec(n;Top;λ,T. F[T]) ⟶ ℙ)
6. ∀n:ℕ. EquivRel(primrec(n;Top;λ,T. F[T]);x,y.G^n (λx,y. True) x y)
⊢ EquivRel(corec(T.F[T]);x,y.corec-rel(G) x y)
BY
{ (RepeatFor 2 ((D 0 THEN Auto))
THEN All (RepUR ``corec-rel``)
THEN D 0
THEN Auto
THEN (Assert EquivRel(primrec(n;Top;λ,T. F[T]);x,y.G^n (λx,y. True) x y) BY
Auto)) }
1
1. F : Type ⟶ Type
2. ContinuousMonotone(T.F[T])
3. G : ⋂T:Type. ((T ⟶ T ⟶ ℙ) ⟶ F[T] ⟶ F[T] ⟶ ℙ)
4. ∀T:Type. ∀E:T ⟶ T ⟶ ℙ. (EquivRel(T;x,y.E x y)
⇒ EquivRel(F[T];x,y.G E x y))
5. ∀n:ℕ. (G^n (λx,y. True) ∈ primrec(n;Top;λ,T. F[T]) ⟶ primrec(n;Top;λ,T. F[T]) ⟶ ℙ)
6. ∀n:ℕ. EquivRel(primrec(n;Top;λ,T. F[T]);x,y.G^n (λx,y. True) x y)
7. Sym(corec(T.F[T]);x,y.∀n:ℕ. (G^n (λx,y. True) x y))
8. a : corec(T.F[T])
9. b : corec(T.F[T])
10. c : corec(T.F[T])
11. ∀n:ℕ. (G^n (λx,y. True) a b)
12. ∀n:ℕ. (G^n (λx,y. True) b c)
13. n : ℕ
14. EquivRel(primrec(n;Top;λ,T. F[T]);x,y.G^n (λx,y. True) x y)
⊢ G^n (λx,y. True) a c
Latex:
Latex:
1. F : Type {}\mrightarrow{} Type
2. ContinuousMonotone(T.F[T])
3. G : \mcap{}T:Type. ((T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}) {}\mrightarrow{} F[T] {}\mrightarrow{} F[T] {}\mrightarrow{} \mBbbP{})
4. \mforall{}T:Type. \mforall{}E:T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}. (EquivRel(T;x,y.E x y) {}\mRightarrow{} EquivRel(F[T];x,y.G E x y))
5. \mforall{}n:\mBbbN{}. (G\^{}n (\mlambda{}x,y. True) \mmember{} primrec(n;Top;\mlambda{},T. F[T]) {}\mrightarrow{} primrec(n;Top;\mlambda{},T. F[T]) {}\mrightarrow{} \mBbbP{})
6. \mforall{}n:\mBbbN{}. EquivRel(primrec(n;Top;\mlambda{},T. F[T]);x,y.G\^{}n (\mlambda{}x,y. True) x y)
\mvdash{} EquivRel(corec(T.F[T]);x,y.corec-rel(G) x y)
By
Latex:
(RepeatFor 2 ((D 0 THEN Auto))
THEN All (RepUR ``corec-rel``)
THEN D 0
THEN Auto
THEN (Assert EquivRel(primrec(n;Top;\mlambda{},T. F[T]);x,y.G\^{}n (\mlambda{}x,y. True) x y) BY
Auto))
Home
Index