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

comparison src/zorn.agda @ 557:f1e899cbe845

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 Fri, 29 Apr 2022 18:23:49 +0900
parents ba889c711524
children fed1c67b9a65
comparison
equal deleted inserted replaced
556:ba889c711524 557:f1e899cbe845
96 s≤fc {A} s {.(f x)} f mf (fsuc x fcy) with proj1 (mf x (A∋fc s f mf fcy ) ) 96 s≤fc {A} s {.(f x)} f mf (fsuc x fcy) with proj1 (mf x (A∋fc s f mf fcy ) )
97 ... | case1 x=fx = subst (λ k → * s ≤ * k ) (*≡*→≡ x=fx) ( s≤fc {A} s f mf fcy ) 97 ... | case1 x=fx = subst (λ k → * s ≤ * k ) (*≡*→≡ x=fx) ( s≤fc {A} s f mf fcy )
98 ... | case2 x<fx with s≤fc {A} s f mf fcy 98 ... | case2 x<fx with s≤fc {A} s f mf fcy
99 ... | case1 s≡x = case2 ( subst₂ (λ j k → j < k ) (sym s≡x) refl x<fx ) 99 ... | case1 s≡x = case2 ( subst₂ (λ j k → j < k ) (sym s≡x) refl x<fx )
100 ... | case2 s<x = case2 ( IsStrictPartialOrder.trans PO s<x x<fx ) 100 ... | case2 s<x = case2 ( IsStrictPartialOrder.trans PO s<x x<fx )
101
102 fcn : {A : HOD} (s : Ordinal) { x : Ordinal} {f : Ordinal → Ordinal} → (mf : ≤-monotonic-f A f) → FClosure A f s x → ℕ
103 fcn s mf (init as) = zero
104 fcn {A} s {x} {f} mf (fsuc y p) with mf y (A∋fc f mf p)
105 ... | ⟪ case1 eq , _ ⟫ = fcn s mf p
106 ... | ⟪ case2 y<fy , _ ⟫ = suc (fcn s mf p )
107
108 fcn-suc : {A : HOD} (s : Ordinal ) { x y : Ordinal} {f : Ordinal → Ordinal} → (mf : ≤-monotonic-f A f)
109 → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → suc (fcn s mf cx ) ≡ fcn s mf cy → * x < * y
110 fcn-suc = ?
111
112 fcn-< : {A : HOD} (s : Ordinal ) { x y : Ordinal} {f : Ordinal → Ordinal} → (mf : ≤-monotonic-f A f)
113 → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → fcn s mf cx Data.Nat.< fcn s mf cy → * x < * y
114 fcn-< = ?
115
116 fcn-fsuc : {A : HOD} (s : Ordinal ) { x y : Ordinal} {f : Ordinal → Ordinal} → (mf : ≤-monotonic-f A f)
117 → (cx : FClosure A f s x ) (cy : FClosure A f s (f x) ) → * x < * (f x) → suc (fcn s mf cx ) ≡ fcn s mf cy
118 fcn-fsuc = ?
101 119
102 fcn-cmp : {A : HOD} (s : Ordinal) { x y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f) (imm : immieate-f A f ) 120 fcn-cmp : {A : HOD} (s : Ordinal) { x y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f) (imm : immieate-f A f )
103 → (cx : FClosure A f s x) → (cy : FClosure A f s y ) → Tri (* x < * y) (* x ≡ * y) (* y < * x ) 121 → (cx : FClosure A f s x) → (cy : FClosure A f s y ) → Tri (* x < * y) (* x ≡ * y) (* y < * x )
104 fcn-cmp {A} s {.s} {.s} f mf imm (init x) (init x₁) = tri≈ (λ lt → <-irr (case1 refl) lt ) refl (λ lt → <-irr (case1 refl) lt ) 122 fcn-cmp {A} s {.s} {.s} f mf imm (init x) (init x₁) = tri≈ (λ lt → <-irr (case1 refl) lt ) refl (λ lt → <-irr (case1 refl) lt )
105 fcn-cmp {A} s f mf imm (init x) (fsuc y cy) with proj1 (mf y (A∋fc s f mf cy ) ) 123 fcn-cmp {A} s f mf imm (init x) (fsuc y cy) with proj1 (mf y (A∋fc s f mf cy ) )