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

comparison ordinal-definable.agda @ 55:9c0a5e28a572

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
regurality elimination case
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 27 May 2019 23:45:56 +0900
parents 33fb8228ace9
children aad8cdce8845
comparison
equal deleted inserted replaced
54:33fb8228ace9 55:9c0a5e28a572
295 ; extentionality = {!!} 295 ; extentionality = {!!}
296 ; minimul = minimul 296 ; minimul = minimul
297 ; regularity = regularity 297 ; regularity = regularity
298 ; infinity∅ = {!!} 298 ; infinity∅ = {!!}
299 ; infinity = {!!} 299 ; infinity = {!!}
300 ; selection = selection 300 ; selection = λ {ψ} {X} {y} → selection {ψ} {X} {y}
301 ; replacement = {!!} 301 ; replacement = {!!}
302 } where 302 } where
303 open _∧_ 303 open _∧_
304 open Minimumo 304 open Minimumo
305 pair : (A B : OD {suc n} ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B) 305 pair : (A B : OD {suc n} ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B)
330 (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅) 330 (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
331 proj1 ( regularity x non ) = minimul<x x non 331 proj1 ( regularity x non ) = minimul<x x non
332 proj2 ( regularity x non ) = reg1 where 332 proj2 ( regularity x non ) = reg1 where
333 reg2 : {y : Ordinal} → ( def (minimul x non) y ∧ (minimul x non ∋ ord→od y) ∧ (x ∋ ord→od y) ) → ⊥ 333 reg2 : {y : Ordinal} → ( def (minimul x non) y ∧ (minimul x non ∋ ord→od y) ∧ (x ∋ ord→od y) ) → ⊥
334 reg2 {y} t with proj1 t | proj1 (proj2 t) | proj2 (proj2 t) 334 reg2 {y} t with proj1 t | proj1 (proj2 t) | proj2 (proj2 t)
335 ... | p1 | p2 | p3 = ? 335 ... | p1 | p2 | p3 = {!!}
336 reg0 : {y : Ordinal {suc n}} → Minimumo (od→ord x) → def (Select (minimul x non) (λ z → (minimul x non ∋ z) ∧ (x ∋ z))) y → def od∅ y 336 reg0 : {y : Ordinal {suc n}} → Minimumo (od→ord x) → def (Select (minimul x non) (λ z → (minimul x non ∋ z) ∧ (x ∋ z))) y → def od∅ y
337 reg0 {y} m t with trio< y (mino (minord x non)) 337 reg0 {y} m t with trio< y (mino (minord x non))
338 reg0 {y} m t | tri< a ¬b ¬c with reg2 {y} ( record { 338 reg0 {y} m t | tri< a ¬b ¬c with reg2 {y} ( record {
339 proj1 = (def-subst {suc n} {minimul x non} (o<→c< a) refl diso ) 339 proj1 = (def-subst {suc n} {minimul x non} (o<→c< a) refl diso )
340 ; proj2 = record { proj1 = {!!} 340 ; proj2 = record { proj1 = proj1 (proj2 t )
341 ; proj2 = {!!} 341 ; proj2 = proj2 (proj2 t )
342 }} ) 342 }} )
343 ... | () 343 ... | ()
344 reg0 {y} m t | tri≈ ¬a refl ¬c = lemma y ( mino (minord x non) ) {!!} where 344 reg0 {y} m t | tri≈ ¬a refl ¬c = lemma y ( mino (minord x non) ) refl
345 lemma : ( ox oy : Ordinal {suc n} ) → ord→od ox c< ord→od oy → Lift (suc n) ⊥ 345 (def-subst {suc n} {ord→od y} {mino (minord x non)} (proj1 t) refl (sym diso))
346 lemma ox oy lt = lift ( o≡→¬c< {suc n} refl lt ) 346 where
347 -- o≡→¬c< {suc n} refl ( c<→o< {suc n} {ord→od y} {ord→od (od→ord (minimul x non))} (proj1 t) ) 347 lemma : ( ox oy : Ordinal {suc n} ) → ox ≡ oy → ord→od ox c< ord→od oy → Lift (suc n) ⊥
348 reg0 {y} m t | tri> ¬a ¬b c = lemma y ( mino (minord x non) ) {!!} {!!} where 348 lemma ox oy refl lt = lift ( o≡→¬c< {suc n} {ord→od oy} {ord→od oy} refl lt )
349 lemma : ( ox oy : Ordinal {suc n} ) → ox o< oy → ord→od oy c< ord→od ox → Lift (suc n) ⊥ 349 reg0 {y} m t | tri> ¬a ¬b c with o<> y (mino (minord x non)) (lemma (proj1 t)) c where
350 lemma ox oy (case1 x) yc<x = {!!} 350 lemma : def (ord→od (mino (ominimal (od→ord x) (∅5 (od→ord x) (λ eq → non (∅7 eq)))))) y → y o< mino (minord x non)
351 lemma ox oy (case2 lt) yc<x with d<→lv lt 351 lemma d with c<→o< {suc n} {ord→od y} {ord→od (mino (minord x non))}
352 ... | refl = lift ( o<→¬c> {suc n} (case2 {!!}) yc<x ) 352 (def-subst {suc n} {ord→od (mino (minord x non))} {y} d refl (sym diso))
353 lemma d | clt = o<-subst clt ord-iso ord-iso
354 ... | ()
353 reg1 : Select (minimul x non) (λ x₁ → (minimul x non ∋ x₁) ∧ (x ∋ x₁)) == od∅ 355 reg1 : Select (minimul x non) (λ x₁ → (minimul x non ∋ x₁) ∧ (x ∋ x₁)) == od∅
354 reg1 = record { eq→ = reg0 (minord x non) ; eq← = λ () } 356 reg1 = record { eq→ = reg0 (minord x non) ; eq← = λ () }
355 357
358
359 -- (o<-subst {suc n} {y} (c<→o< {suc n} (def-subst {suc n} (proj1 t ) {!!} {!!} )) {!!} {!!} )
360 -- c<> {n} (o<→c< {suc n} {mino (minord x non)} {y} (case2 lto))
361 -- (def-subst {suc n} {ord→od (mino (minord x non))} {y} lt refl refl ) -- lemma y ( mino (minord x non) )
362 -- (def-subst {suc n} {ord→od y} {mino (minord x non)} (proj1 t) refl (sym diso))
363 -- {!!} where