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

changeset 64:87df00599a0e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
equal
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 29 May 2019 18:50:57 +0900
parents ba43f7ff60d4
children 164ad5a703d8
files ordinal-definable.agda
diffstat 1 files changed, 29 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/ordinal-definable.agda	Wed May 29 14:28:26 2019 +0900
+++ b/ordinal-definable.agda	Wed May 29 18:50:57 2019 +0900
@@ -353,19 +353,35 @@
          omin→cmin  {x} {not} 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
          minimul<x : (x : OD {suc n} ) →  (not :  ¬ x == od∅ ) → x ∋ minimul x not
          minimul<x x not =  omin→cmin {x} {not} (min<x (minord x not)) 
-         omin∅→min∅ : (ox : Ordinal {suc n}) { x : OD {suc n} } → ( x ≡ ord→od ox ) → {non : ¬ ( ord→od ox == od∅)} →  {not : ¬ (x == od∅)} 
-            → mino (ominimal ox (∅10 refl non)) ≡ o∅ → mino (ominimal (od→ord x) (∅9 not)) ≡ o∅
-         omin∅→min∅ ox {x} refl {non} {not} eq with ominimal ox (∅10 refl non)
-         omin∅→min∅ record { lv = Zero ; ord = (Φ .0) }  refl eq | record { mino = mino ; min<x = case1 () }
-         omin∅→min∅ record { lv = Zero ; ord = (Φ .0) }  refl eq | record { mino = mino ; min<x = case2 () }
-         omin∅→min∅ record { lv = Zero ; ord = (OSuc .0 ord₁) }  refl refl | record { mino = .o∅ ; min<x = case1 () }
-         omin∅→min∅ record { lv = Zero ; ord = (OSuc .0 ord₁) }  refl refl | record { mino = .o∅ ; min<x = case2 Φ< } = {!!}
-         omin∅→min∅ record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) }  refl refl | record { mino = .o∅ ; min<x = case1 (s≤s z≤n) } = {!!}
-         omin∅→min∅ record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) }  refl eq | record { mino = mino ; min<x = case2 () }
-         omin∅→min∅ record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) }  refl refl | record { mino = .o∅ ; min<x = case1 (s≤s z≤n) } = {!!}
-         omin∅→min∅ record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) }  refl refl | record { mino = .o∅ ; min<x = case2 () }
-         omin∅→min∅ record { lv = (Suc lv₁) ; ord = (ℵ .lv₁) }  refl refl | record { mino = .o∅ ; min<x = case1 (s≤s z≤n) } = {!!}
-         omin∅→min∅ record { lv = (Suc lv₁) ; ord = (ℵ .lv₁) }  refl refl | record { mino = .o∅ ; min<x = case2 () } 
+         omin∅≡min∅ : (ox : Ordinal {suc n}) → {not : ¬ ( ord→od ox == od∅)} 
+            → mino (ominimal ox (∅10 refl not)) ≡ mino (ominimal (od→ord (ord→od ox)) (∅9 not)) 
+         omin∅≡min∅ ox  {not} with ominimal ox (∅10 refl not)
+         omin∅≡min∅ record { lv = Zero ; ord = (Φ .0) }  | record { mino = mino ; min<x = case1 () }
+         omin∅≡min∅ record { lv = Zero ; ord = (Φ .0) }  | record { mino = mino ; min<x = case2 () }
+         omin∅≡min∅ record { lv = Zero ; ord = (OSuc .0 ord₁) }  | record { mino = _ ; min<x = case1 () }
+         omin∅≡min∅ record { lv = Zero ; ord = (OSuc .0 ord₁) }  | record { mino = record { lv = 0 ; ord = Φ 0 } ; min<x = case2 Φ< } =  {!!}
+         omin∅≡min∅ record { lv = Zero ; ord = (OSuc .0 ord₁) } {_} | record { mino = record { lv = .0 ; ord = .(OSuc 0 _) } ; min<x = case2 (s< x)}  = {!!}
+         omin∅≡min∅ record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) }  | record { mino = _ ; min<x = case1 (s≤s z≤n) } = {!!}
+         omin∅≡min∅ record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) }  | record { mino = mino ; min<x = case2 () }
+         omin∅≡min∅ record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) }  | record { mino = _ ; min<x = case1 (s≤s z≤n) } = {!!}
+         omin∅≡min∅ record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) }  | record { mino = _ ; min<x = case2 lt } = {!!}
+         omin∅≡min∅ record { lv = (Suc lv₁) ; ord = (ℵ .lv₁) }  | record { mino = _ ; min<x = case1 (s≤s z≤n) } = {!!}
+         omin∅≡min∅ record { lv = (Suc lv₁) ; ord = (ℵ .lv₁) }  | record { mino = _ ; min<x = case2 lt }  = {!!}
+         omin∅≡min∅ record { lv = (Suc lv₁) ; ord = ord } {not} | record { mino = mino ; min<x = min<x } = {!!}
+         omin∅→min∅ : (ox : Ordinal {suc n}) { x : OD {suc n} } →  {not : ¬ ( ord→od ox == od∅)} 
+            → mino (ominimal ox (∅10 refl not)) ≡ o∅ → mino (ominimal (od→ord (ord→od ox)) (∅9 not)) ≡ o∅
+         omin∅→min∅ ox {x} {not} eq with ominimal ox (∅10 refl not)
+         omin∅→min∅ record { lv = Zero ; ord = (Φ .0) }  eq | record { mino = mino ; min<x = case1 () }
+         omin∅→min∅ record { lv = Zero ; ord = (Φ .0) }  eq | record { mino = mino ; min<x = case2 () }
+         omin∅→min∅ record { lv = Zero ; ord = (OSuc .0 ord₁) }  refl | record { mino = .o∅ ; min<x = case1 () }
+         omin∅→min∅ record { lv = Zero ; ord = (OSuc .0 ord₁) }  refl | record { mino = .o∅ ; min<x = case2 Φ< } = 
+               subst (λ k → ?  ≡ k  ) ? (omin∅→min∅ o∅ {!!})
+         omin∅→min∅ record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) }  refl | record { mino = .o∅ ; min<x = case1 (s≤s z≤n) } = {!!}
+         omin∅→min∅ record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) }  eq | record { mino = mino ; min<x = case2 () }
+         omin∅→min∅ record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) }  refl | record { mino = .o∅ ; min<x = case1 (s≤s z≤n) } = {!!}
+         omin∅→min∅ record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) }  refl | record { mino = .o∅ ; min<x = case2 () }
+         omin∅→min∅ record { lv = (Suc lv₁) ; ord = (ℵ .lv₁) }  refl | record { mino = .o∅ ; min<x = case1 (s≤s z≤n) } = {!!}
+         omin∅→min∅ record { lv = (Suc lv₁) ; ord = (ℵ .lv₁) }  refl | record { mino = .o∅ ; min<x = case2 () } 
          regularity :  (x : OD) (not : ¬ (x == od∅)) →
             (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
          regularity x not = regularity-ord (od→ord x) {x} (sym oiso ) not where