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

changeset 195:0cefb1e4d2cc

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 Mon, 29 Jul 2019 11:49:58 +0900
parents 2a5844398f1c
children a3211dcb4d83
files OD.agda
diffstat 1 files changed, 4 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/OD.agda	Mon Jul 29 11:27:33 2019 +0900
+++ b/OD.agda	Mon Jul 29 11:49:58 2019 +0900
@@ -565,12 +565,9 @@
                 → (ly < lx) ∨ (oy d< ox  ) → OD {suc n}
             lemma-ord Zero (Φ 0) (case1 ())
             lemma-ord Zero (Φ 0) (case2 ())
-            lemma-ord Zero (OSuc 0 ox) lt with ∋-p X (ord→od record { lv = Zero ; ord = OSuc 0 ox })
-            lemma-ord Zero (OSuc Zero ox) lt | yes p = ord→od record { lv = Zero ; ord = OSuc 0 ox }
-            lemma-ord Zero (OSuc Zero ox) {ly} {oy} lt | no ¬p = lemma-ord Zero ox {!!}
-            lemma-ord (Suc lx) (OSuc (Suc lx) ox) lt with ∋-p X (ord→od record { lv = (Suc lx)  ; ord = ox } )
-            lemma-ord (Suc lx) (OSuc (Suc lx) ox) lt | yes p = ord→od record { lv = (Suc lx)  ; ord = ox } 
-            lemma-ord (Suc lx) (OSuc (Suc lx) ox) {ly} {oy} lt | no ¬p = lemma-ord (Suc lx) ox {!!}
+            lemma-ord lx (OSuc lx ox) lt with ∋-p X (ord→od record { lv = lx ; ord = OSuc lx ox })
+            lemma-ord lx (OSuc lx ox) lt | yes p = ord→od record { lv = lx ; ord = OSuc lx ox }
+            lemma-ord lx (OSuc lx ox) {ly} {oy} lt | no ¬p = lemma-ord lx ox {ly} {oy} {!!}
             lemma-ord (Suc lx) (Φ (Suc lx)) lt with ∋-p X (ord→od record { lv = Suc lx ; ord = Φ (Suc lx)})
             lemma-ord (Suc lx) (Φ (Suc lx)) lt | yes p = ord→od record { lv = Suc lx ; ord = Φ (Suc lx)}
-            lemma-ord (Suc lx) (Φ (Suc lx)) {ly} {oy} lt | no ¬p = {!!}
+            lemma-ord (Suc lx) (Φ .(Suc lx)) {ly} {oy} (case1 lt ) | no ¬p = {!!}