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

changeset 22:3da2c00bd24d

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 Thu, 16 May 2019 17:20:45 +0900
parents 6d9fdd1dfa79
children 7293a151d949
files constructible-set.agda
diffstat 1 files changed, 21 insertions(+), 21 deletions(-) [+]
line wrap: on
line diff
--- a/constructible-set.agda	Thu May 16 16:47:27 2019 +0900
+++ b/constructible-set.agda	Thu May 16 17:20:45 2019 +0900
@@ -38,27 +38,6 @@
 o∅ : Ordinal
 o∅  = record { lv = Zero ; ord = Φ }
 
-TransFinite : ( ψ : Ordinal  → Set n ) 
-  → ( ∀ (lx : Nat ) → ψ ( record { lv = Suc lx ; ord = ℵ lx } )) 
-  → ( ∀ (lx : Nat ) → ψ ( record { lv = lx ; ord = Φ } ) )
-  → ( ∀ (lx : Nat ) → (x : OrdinalD lx )  → ψ ( record { lv = lx ; ord = x } ) → ψ ( record { lv = lx ; ord = OSuc x } ) )
-  →  ∀ (x : Ordinal)  → ψ x
-TransFinite ψ caseℵ caseΦ caseOSuc record { lv = lv ; ord = Φ } = caseΦ lv
-TransFinite ψ caseℵ caseΦ caseOSuc record { lv = lv ; ord = OSuc ord₁ } = caseOSuc lv ord₁
-    ( TransFinite ψ caseℵ caseΦ caseOSuc (record { lv = lv ; ord = ord₁ } ))
-TransFinite ψ caseℵ caseΦ caseOSuc record { lv = Suc lv₁ ; ord = ℵ lv₁ } = caseℵ lv₁
-
-record SupR (ψ : Ordinal → Ordinal ) : Set n where
-  field
-    sup : Ordinal
-    smax : { x : Ordinal } → ψ x o< sup
-
-open SupR
-
-Sup : (ψ : Ordinal → Ordinal )  → SupR ψ
-sup (Sup ψ) = {!!}
-smax (Sup ψ) = {!!}
-     
 
 ≡→¬d< : {lv : Nat} → {x  : OrdinalD  lv }  → x d< x → ⊥
 ≡→¬d<  {lx} {OSuc y} (s< t) = ≡→¬d< t
@@ -145,6 +124,27 @@
      }
  }
 
+TransFinite : ( ψ : Ordinal  → Set n ) 
+  → ( ∀ (lx : Nat ) → ψ ( record { lv = Suc lx ; ord = ℵ lx } )) 
+  → ( ∀ (lx : Nat ) → ψ ( record { lv = lx ; ord = Φ } ) )
+  → ( ∀ (lx : Nat ) → (x : OrdinalD lx )  → ψ ( record { lv = lx ; ord = x } ) → ψ ( record { lv = lx ; ord = OSuc x } ) )
+  →  ∀ (x : Ordinal)  → ψ x
+TransFinite ψ caseℵ caseΦ caseOSuc record { lv = lv ; ord = Φ } = caseΦ lv
+TransFinite ψ caseℵ caseΦ caseOSuc record { lv = lv ; ord = OSuc ord₁ } = caseOSuc lv ord₁
+    ( TransFinite ψ caseℵ caseΦ caseOSuc (record { lv = lv ; ord = ord₁ } ))
+TransFinite ψ caseℵ caseΦ caseOSuc record { lv = Suc lv₁ ; ord = ℵ lv₁ } = caseℵ lv₁
+
+record SupR (ψ : Ordinal → Ordinal ) : Set n where
+  field
+    sup : Ordinal
+    smax : { x : Ordinal } → ψ x o< sup
+
+open SupR
+
+Sup : (ψ : Ordinal → Ordinal )  → SupR ψ
+sup (Sup ψ) = {!!}
+smax (Sup ψ) = {!!}
+     
 -- X' = { x ∈ X |  ψ  x } ∪ X , Mα = ( ∪ (β < α) Mβ ) '
 
 record ConstructibleSet  : Set (suc (suc n)) where