Mercurial > hg > Members > kono > Proof > category

changeset 886:1c659deb22f8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
loop
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 12 Apr 2020 03:34:50 +0900
parents a502754b890a
children 9c41a7851817
files CCCGraph1.agda
diffstat 1 files changed, 6 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph1.agda	Sun Apr 12 03:26:35 2020 +0900
+++ b/CCCGraph1.agda	Sun Apr 12 03:34:50 2020 +0900
@@ -295,6 +295,12 @@
                   cong₂ (λ j k → < j , k > ) ( d-eval f g ) ( d-eval f₁ g ))
               d-eval (iv x (iv f f₁)) g = begin
                     eval (iv x (iv f f₁) ・ g)
+                ≡⟨⟩
+                    eval (iv x (iv f f₁ ・ g))
+                ≡⟨ {!!} ⟩
+                    eval (iv x (eval (iv f f₁ ・ g)))
+                ≡⟨ {!!} ⟩
+                    eval (iv x (eval (iv f f₁) ・ eval g))
                 ≡⟨ {!!} ⟩
                     eval (eval (iv x (iv f f₁)) ・ eval g)
                 ∎  where open ≡-Reasoning