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

comparison HOD.agda @ 157:afc030b7c8d0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
explict logical definition of Union failed
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 14 Jul 2019 08:04:16 +0900
parents 3e7475fb28db
children b97b4ee06f01
comparison
equal deleted inserted replaced
156:3e7475fb28db 157:afc030b7c8d0
337 -- lemma = def-subst {suc n} {_} {_} {Ord x} {_} UX∋z refl (sym diso) 337 -- lemma = def-subst {suc n} {_} {_} {Ord x} {_} UX∋z refl (sym diso)
338 338
339 union-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n} 339 union-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n}
340 union-u {X} {z} U>z = ord→od ( osuc ( od→ord z ) ) 340 union-u {X} {z} U>z = ord→od ( osuc ( od→ord z ) )
341 union→ : (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z 341 union→ : (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
342 union→ X z u xx = {!!} 342 union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx
343 343 ; proj2 = subst ( λ k → def k (od→ord z)) (sym oiso) (proj2 xx) } ))
344
345 union-u' : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n}
346 union-u' {X} {z} U>z = record { def = λ x → ¬ ( (u : Ordinal ) → ¬ (def X u) ∧ (ord→od u ∋ z ) ∧ ( u ≡ x ) ) }
347 union←' : (X z : OD) (X∋z : Union X ∋ z) → ¬ ( (u : OD ) → ¬ ((X ∋ u) ∧ (u ∋ z )))
348 union←' X z UX∋z = TransFiniteExists {suc (suc n)} {λ x → {!!} } {!!} {!!} where
344 union← : (X z : OD) (X∋z : Union X ∋ z) → (X ∋ union-u {X} {z} X∋z ) ∧ (union-u {X} {z} X∋z ∋ z ) 349 union← : (X z : OD) (X∋z : Union X ∋ z) → (X ∋ union-u {X} {z} X∋z ) ∧ (union-u {X} {z} X∋z ∋ z )
345 union← X z UX∋z = record { proj1 = lemma ; proj2 = lemma2 } where 350 union← X z UX∋z = record { proj1 = lemma ; proj2 = lemma2 } where
346 lemma : X ∋ union-u {X} {z} UX∋z 351 lemma : X ∋ union-u {X} {z} UX∋z
347 lemma = {!!} -- def-subst {suc n} {_} {_} {X} {od→ord (Ord (osuc ( od→ord z )))} UX∋z refl {!!} 352 lemma = {!!} -- def-subst {suc n} {_} {_} {X} {od→ord (Ord (osuc ( od→ord z )))} UX∋z refl {!!}
348 lemma2 : union-u {X} UX∋z ∋ z 353 lemma2 : union-u {X} UX∋z ∋ z