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

comparison OD.agda @ 196:a3211dcb4d83

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:58:10 +0900
parents 0cefb1e4d2cc
children b114cf5b9130
comparison
equal deleted inserted replaced
195:0cefb1e4d2cc 196:a3211dcb4d83
556 lemma5 ox lt = subst (λ k → ψ k ) oiso (ε-induction-ord lx ox lt ) 556 lemma5 ox lt = subst (λ k → ψ k ) oiso (ε-induction-ord lx ox lt )
557 lemma6 : { ly : Nat } { ox : OrdinalD {suc n} lx } { oy : OrdinalD {suc n} ly } → 557 lemma6 : { ly : Nat } { ox : OrdinalD {suc n} lx } { oy : OrdinalD {suc n} ly } →
558 lx ≡ ly → ly ≡ lv (od→ord z) → ψ z 558 lx ≡ ly → ly ≡ lv (od→ord z) → ψ z
559 lemma6 {ly} {ox} {oy} refl refl = lemma5 (OSuc lx (ord (od→ord z)) ) (case2 s<refl) 559 lemma6 {ly} {ox} {oy} refl refl = lemma5 (OSuc lx (ord (od→ord z)) ) (case2 s<refl)
560 560
561 choice-func' : (X : OD {suc n} ) → (∋-p : (A x : OD {suc n} ) → Dec ( A ∋ x ) ) → ¬ ( X == od∅ ) → OD {suc n} 561 record choiced {n : Level} ( X : OD {suc n}) : Set (suc (suc n)) where
562 field
563 a-choice : OD {suc n}
564 is-in : X ∋ a-choice
565 choice-func' : (X : OD {suc n} ) → (∋-p : (A x : OD {suc n} ) → Dec ( A ∋ x ) ) → ¬ ( X == od∅ ) → choiced X
562 choice-func' X ∋-p not = lemma-ord (lv (osuc (od→ord X))) (ord (osuc (od→ord X))) <-osuc 566 choice-func' X ∋-p not = lemma-ord (lv (osuc (od→ord X))) (ord (osuc (od→ord X))) <-osuc
563 where 567 where
564 lemma-ord : (lx : Nat) ( ox : OrdinalD {suc n} lx ) {ly : Nat} {oy : OrdinalD {suc n} ly } 568 lemma-ord : (lx : Nat) ( ox : OrdinalD {suc n} lx ) {ly : Nat} {oy : OrdinalD {suc n} ly }
565 → (ly < lx) ∨ (oy d< ox ) → OD {suc n} 569 → (ly < lx) ∨ (oy d< ox ) → choiced X
566 lemma-ord Zero (Φ 0) (case1 ()) 570 lemma-ord Zero (Φ 0) (case1 ())
567 lemma-ord Zero (Φ 0) (case2 ()) 571 lemma-ord Zero (Φ 0) (case2 ())
568 lemma-ord lx (OSuc lx ox) lt with ∋-p X (ord→od record { lv = lx ; ord = OSuc lx ox }) 572 lemma-ord lx (OSuc lx ox) lt with ∋-p X (ord→od record { lv = lx ; ord = OSuc lx ox })
569 lemma-ord lx (OSuc lx ox) lt | yes p = ord→od record { lv = lx ; ord = OSuc lx ox } 573 lemma-ord lx (OSuc lx ox) lt | yes p = record { a-choice = ord→od record { lv = lx ; ord = OSuc lx ox } ; is-in = p }
570 lemma-ord lx (OSuc lx ox) {ly} {oy} lt | no ¬p = lemma-ord lx ox {ly} {oy} {!!} 574 lemma-ord lx (OSuc lx ox) {ly} {oy} lt | no ¬p = lemma-ord lx ox {ly} {oy} {!!}
571 lemma-ord (Suc lx) (Φ (Suc lx)) lt with ∋-p X (ord→od record { lv = Suc lx ; ord = Φ (Suc lx)}) 575 lemma-ord (Suc lx) (Φ (Suc lx)) lt with ∋-p X (ord→od record { lv = Suc lx ; ord = Φ (Suc lx)})
572 lemma-ord (Suc lx) (Φ (Suc lx)) lt | yes p = ord→od record { lv = Suc lx ; ord = Φ (Suc lx)} 576 lemma-ord (Suc lx) (Φ (Suc lx)) lt | yes p = record { a-choice = ord→od record { lv = Suc lx ; ord = Φ (Suc lx)} ; is-in = p }
573 lemma-ord (Suc lx) (Φ .(Suc lx)) {ly} {oy} (case1 lt ) | no ¬p = {!!} 577 lemma-ord (Suc lx) (Φ .(Suc lx)) {ly} {oy} (case1 lt ) | no ¬p = {!!}