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

changeset 1332:87df366f85f3

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:28:04 +0900
parents 97ea311161ba
children 069966121911
files src/bijection.agda
diffstat 1 files changed, 2 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/src/bijection.agda	Tue Jun 13 12:04:49 2023 +0900
+++ b/src/bijection.agda	Tue Jun 13 12:28:04 2023 +0900
@@ -794,12 +794,12 @@
              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 : suc (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 = 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 (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