Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 1331:97ea311161ba

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 13 Jun 2023 12:04:49 +0900
parents 27ce91231127
children 87df366f85f3
files src/bijection.agda
diffstat 1 files changed, 11 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/src/bijection.agda	Tue Jun 13 11:47:55 2023 +0900
+++ b/src/bijection.agda	Tue Jun 13 12:04:49 2023 +0900
@@ -792,8 +792,18 @@
          n<ca (cons (ca<n j fi<fm) fl fr) (suc i) i<fl = cl03 where
              cl02 : i + count-A (c fl 0 ?) ≤ count-A (c fl i ? )
              cl02 = n<ca fl i ?
+             cl05 : count-A (c fl 0 ?) ≡  count-A (c (cons (ca<n j fi<fm) fl fr) 0 ? ) 
+             cl05 = ?
+             cl06 : count-A (c fl i ?) ≡  count-A (c (cons (ca<n j fi<fm) fl fr) (suc i) ? ) 
+             cl06 = ?
              cl03 : (suc i) + count-A (c (cons (ca<n j fi<fm) fl fr) 0 ?) ≤ count-A (c (cons (ca<n j fi<fm) fl fr) (suc i) ? )
-             cl03 = ?
+             cl03 = begin
+                 (suc i) + count-A (c (cons (ca<n j fi<fm) fl fr) 0 ?) ≡⟨ ? ⟩
+                 (suc i) + count-A (c fl 0 ?) ≤⟨ ? ⟩
+                 suc (i + count-A (c fl 0 ?)) ≤⟨ ? ⟩
+                 suc (count-A (c fl i ?)) ≤⟨ ? ⟩
+                 count-A (c (cons (ca<n j fi<fm) fl fr) (suc i) ? ) ∎ where
+                    open ≤-Reasoning
 
 
     record CountB (n : ℕ) : Set where