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

comparison ordinal-definable.agda @ 58:323b561210b5

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, 28 May 2019 23:02:50 +0900
parents 419688a279e0
children d13d1351a1fa
comparison
equal deleted inserted replaced
57:419688a279e0 58:323b561210b5
337 minimul x not = ord→od ( mino (minord x not)) 337 minimul x not = ord→od ( mino (minord x not))
338 minimul<x : (x : OD {suc n} ) → (not : ¬ x == od∅ ) → x ∋ minimul x not 338 minimul<x : (x : OD {suc n} ) → (not : ¬ x == od∅ ) → x ∋ minimul x not
339 minimul<x x not = lemma0 (min<x (minord x not)) where 339 minimul<x x not = lemma0 (min<x (minord x not)) where
340 lemma0 : mino (minord x not) o< (od→ord x) → def x (od→ord (ord→od (mino (minord x not)))) 340 lemma0 : mino (minord x not) o< (od→ord x) → def x (od→ord (ord→od (mino (minord x not))))
341 lemma0 m<x = def-subst {suc n} {ord→od (od→ord x)} {od→ord (ord→od (mino (minord x not)))} (o<→c< m<x) oiso refl 341 lemma0 m<x = def-subst {suc n} {ord→od (od→ord x)} {od→ord (ord→od (mino (minord x not)))} (o<→c< m<x) oiso refl
342 regularity-ord : (x : Ordinal ) (not : o∅ o< x ) → 342 regularity-ord : (x : Ordinal ) (not : ¬ (ord→od x == od∅)) →
343 (ord→od x ∋ minimul (ord→od x) (∅0 not)) ∧ (Select (minimul (ord→od x) (∅0 not)) (λ x₁ → (minimul (ord→od x) (∅0 not) ∋ x₁) ∧ ((ord→od x) ∋ x₁)) == od∅) 343 (ord→od x ∋ minimul (ord→od x) not) ∧ (Select (minimul (ord→od x) not) (λ x₁ → (minimul (ord→od x) not ∋ x₁) ∧ ((ord→od x) ∋ x₁)) == od∅)
344 proj1 ( regularity-ord x non ) = minimul<x (ord→od x) (∅0 non) 344 proj1 ( regularity-ord x not ) = minimul<x (ord→od x) not
345 proj2 ( regularity-ord x non ) = reg1 where 345 proj2 ( regularity-ord x not ) = reg1 where
346 reg2 : {y : Ordinal} → ( def (minimul (ord→od x) (∅0 non)) y ∧ (minimul (ord→od x) (∅0 non) ∋ ord→od y) ∧ ((ord→od x) ∋ ord→od y) ) → ⊥ 346 reg2 : {y : Ordinal} → ( def (minimul (ord→od x) not) y ∧ (minimul (ord→od x) not ∋ ord→od y) ∧ ((ord→od x) ∋ ord→od y) ) → ⊥
347 reg2 {y} t with proj1 t | proj1 (proj2 t) | proj2 (proj2 t) 347 reg2 {y} t with proj1 t | proj1 (proj2 t) | proj2 (proj2 t)
348 ... | p1 | p2 | p3 with is-∋ (ord→od x) ( ord→od y) 348 ... | p1 | p2 | p3 with is-∋ (ord→od x) ( ord→od y)
349 reg2 {y} t | p1 | p2 | p3 | no ¬p = ⊥-elim (¬p p3 ) -- ¬ x ∋ ord→od y empty x case 349 reg2 {y} t | p1 | p2 | p3 | no ¬p = ⊥-elim (¬p p3 ) -- ¬ x ∋ ord→od y empty x case
350 reg2 {y} t | p1 | p2 | p3 | yes p with is-∋ (minimul (ord→od x) (∅0 non)) (ord→od y) 350 reg2 {y} t | p1 | p2 | p3 | yes p with is-∋ (minimul (ord→od x) not) (ord→od y)
351 reg2 {y} t | p1 | p2 | p3 | yes p | no ¬p = ⊥-elim (¬p p2 ) -- minimum contains nothing q.e.d. 351 reg2 {y} t | p1 | p2 | p3 | yes p | no ¬p = ⊥-elim (¬p p2 ) -- minimum contains nothing q.e.d.
352 reg2 {y} t | p1 | p2 | p3 | yes p | yes p₁ = {!!} 352 reg2 {y} t | p1 | p2 | p3 | yes p | yes p₁ = {!!}
353 reg0 : {y : Ordinal {suc n}} → Minimumo x → def (Select (minimul (ord→od x) (∅0 non)) (λ z → (minimul (ord→od x) (∅0 non) ∋ z) ∧ ((ord→od x) ∋ z))) y → def od∅ y 353 reg0 : {y : Ordinal {suc n}} → def (Select (minimul (ord→od x) not) (λ z → (minimul (ord→od x) not ∋ z) ∧ ((ord→od x) ∋ z))) y → def od∅ y
354 reg0 {y} m t with trio< y (mino (minord (ord→od x) (∅0 non))) 354 reg0 {y} t with trio< y (mino (minord (ord→od x) not))
355 reg0 {y} m t | tri< a ¬b ¬c with reg2 {y} t 355 reg0 {y} t | tri< a ¬b ¬c with reg2 {y} t
356 ... | () 356 ... | ()
357 reg0 {y} m t | tri≈ ¬a refl ¬c = lemma y ( mino (minord (ord→od x) (∅0 non)) ) refl 357 reg0 {y} t | tri≈ ¬a refl ¬c = lemma y ( mino (minord (ord→od x) not) ) refl
358 (def-subst {suc n} {ord→od y} {mino (minord (ord→od x) (∅0 non))} (proj1 t) refl (sym diso)) 358 (def-subst {suc n} {ord→od y} {mino (minord (ord→od x) not)} (proj1 t) refl (sym diso))
359 where 359 where
360 lemma : ( ox oy : Ordinal {suc n} ) → ox ≡ oy → ord→od ox c< ord→od oy → Lift (suc n) ⊥ 360 lemma : ( ox oy : Ordinal {suc n} ) → ox ≡ oy → ord→od ox c< ord→od oy → Lift (suc n) ⊥
361 lemma ox oy refl lt = lift ( o≡→¬c< {suc n} {ord→od oy} {ord→od oy} refl lt ) 361 lemma ox oy refl lt = lift ( o≡→¬c< {suc n} {ord→od oy} {ord→od oy} refl lt )
362 reg0 {y} m t | tri> ¬a ¬b c with o<> y (mino (minord (ord→od x) (∅0 non))) (lemma {!!}) c where 362 reg0 {y} t | tri> ¬a ¬b c with o<> y (mino (minord (ord→od x) not)) (lemma {!!}) c where
363 lemma : def (ord→od (mino (ominimal x (∅5 (λ eq → (∅0 non) (∅7 {!!})))))) y → y o< mino (minord (ord→od x) (∅0 non)) 363 lemma : def (ord→od (mino (minord (ord→od x) not))) y → y o< mino (minord (ord→od x) not)
364 lemma d with c<→o< {suc n} {ord→od y} {ord→od (mino (minord (ord→od x) (∅0 non)))} 364 lemma d with c<→o< {suc n} {ord→od y} {ord→od (mino (minord (ord→od x) not))}
365 (def-subst {suc n} {ord→od (mino (minord (ord→od x) (∅0 non)))} {y} {!!} refl (sym diso)) 365 (def-subst {suc n} {ord→od (mino (minord (ord→od x) not))} {y} {!!} refl (sym diso))
366 lemma d | clt = o<-subst clt ord-iso ord-iso 366 lemma d | clt = o<-subst clt ord-iso ord-iso
367 ... | () 367 ... | ()
368 reg1 : Select (minimul (ord→od x) (∅0 non)) (λ x₁ → (minimul (ord→od x) (∅0 non) ∋ x₁) ∧ ((ord→od x) ∋ x₁)) == od∅ 368 reg1 : Select (minimul (ord→od x) not) (λ x₁ → (minimul (ord→od x) not ∋ x₁) ∧ ((ord→od x) ∋ x₁)) == od∅
369 reg1 = record { eq→ = reg0 (ominimal x non) ; eq← = λ () } where 369 reg1 = record { eq→ = reg0 ; eq← = λ () } where
370 ∅-iso : {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) 370 ∅-iso : {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅)
371 ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq where 371 ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq where
372 regularity : (x : OD) (not : ¬ (x == od∅)) → 372 regularity : (x : OD) (not : ¬ (x == od∅)) →
373 (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅) 373 (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
374 regularity x not with regularity-ord ( od→ord x ) ( ∅9 not ) 374 proj1 (regularity x not ) = minimul<x x not
375 ... | t = ? 375 proj2 (regularity x not ) = record { eq→ = reg4 ; eq← = λ () } where
376 376 reg4 : {xd : Ordinal } → def (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁))) xd → def od∅ xd
377 377 reg4 {xd} = {!!} (eq→ (proj1 (regularity-ord {!!} {!!} )) )
378
379
380
381
382