Mercurial > hg > Members > kono > Proof > ZF-in-agda
graph
-
otrans in repl2019-07-06, by Shinji KONO
-
replacement in HOD2019-07-06, by Shinji KONO
-
replacement in ordinal-definable2019-07-06, by Shinji KONO
-
use OD for replace condition2019-07-06, by Shinji KONO
-
...2019-07-02, by Shinji KONO
-
new replacement axiom2019-07-02, by Shinji KONO
-
ord power set2019-07-02, by Shinji KONO
-
... dead end?2019-07-01, by Shinji KONO
-
...2019-07-01, by Shinji KONO
-
power set2019-06-30, by Shinji KONO
-
...2019-06-30, by Shinji KONO
-
record L2019-06-30, by Shinji KONO
-
...2019-06-30, by Shinji KONO
-
...2019-06-30, by Shinji KONO
-
...2019-06-27, by Shinji KONO
-
inifinite done2019-06-26, by Shinji KONO
-
infinite2019-06-26, by Shinji KONO
-
Union done2019-06-26, by Shinji KONO
-
minimum assuption2019-06-25, by Shinji KONO
-
axiom of selection2019-06-25, by Shinji KONO
-
Select declaration2019-06-25, by Shinji KONO
-
f x d2019-06-25, by Shinji KONO
-
...2019-06-25, by Shinji KONO
-
HOD2019-06-24, by Shinji KONO
-
...2019-06-20, by Shinji KONO
-
dead end2019-06-18, by Shinji KONO
-
remove o<→c< and add otrans in OD2019-06-18, by Shinji KONO
-
dead end?2019-06-18, by Shinji KONO
-
add assumption2019-06-16, by Shinji KONO
-
add Ord Ordinal order preserving map2019-06-16, by Shinji KONO
-
power set2019-06-16, by Shinji KONO
-
...2019-06-15, by Shinji KONO
-
starting over HOD2019-06-12, by Shinji KONO
-
Added tag current for changeset a402881cc3412019-06-10, by Shinji KONO
-
add comment2019-06-10, by Shinji KONO
-
Power Set done with min-sup assumption2019-06-10, by Shinji KONO
-
...2019-06-09, by Shinji KONO
-
power set using sup on Def2019-06-09, by Shinji KONO
-
Power Set and L2019-06-08, by Shinji KONO
-
clean up2019-06-08, by Shinji KONO
-
...2019-06-08, by Shinji KONO
-
replacement2019-06-06, by Shinji KONO
-
Added tag current for changeset b4742cf4ef972019-06-05, by Shinji KONO
-
infinity axiom done2019-06-05, by Shinji KONO
-
def ord conversion2019-06-05, by Shinji KONO
-
...2019-06-05, by Shinji KONO
-
osuc work around done2019-06-05, by Shinji KONO
-
split omax?2019-06-04, by Shinji KONO
-
internal error2019-06-04, by Shinji KONO
-
omax-induction does not work2019-06-04, by Shinji KONO
-
omax ..2019-06-04, by Shinji KONO
-
...2019-06-04, by Shinji KONO
-
Union (x , y) == (x , y ) only true on infinite case2019-06-04, by Shinji KONO
-
simpler ordinal2019-06-03, by Shinji KONO
-
remove ∅-base-def2019-06-03, by Shinji KONO
-
add some lemma2019-06-03, by Shinji KONO
-
infinite and replacement begin2019-06-03, by Shinji KONO
-
Power Set on going ...2019-06-02, by Shinji KONO
-
extensionality done2019-06-02, by Shinji KONO
-
Union done2019-06-02, by Shinji KONO
-
ordinal atomical successor?2019-06-01, by Shinji KONO
-
fix ordinal2019-06-01, by Shinji KONO
-
...2019-06-01, by Shinji KONO
-
add osuc ( next larger element of Ordinal )2019-06-01, by Shinji KONO
-
Union needs +1 space2019-06-01, by Shinji KONO
-
union continue2019-05-31, by Shinji KONO
-
Union2019-05-29, by Shinji KONO
-
Added tag current for changeset 92a11dc6425c2019-05-29, by Shinji KONO
-
regularity done2019-05-29, by Shinji KONO
-
¬∅=→∅∈ : {n : Level} → { x : OD {suc n} } → ¬ ( x == od∅ {suc n} ) → x ∋ od∅ {suc n}2019-05-29, by Shinji KONO
-
equal2019-05-29, by Shinji KONO
-
omin2019-05-29, by Shinji KONO
-
...2019-05-29, by Shinji KONO
-
fix2019-05-29, by Shinji KONO
-
dead end2019-05-29, by Shinji KONO
-
lemma = cong₂ (λ x not → minimul x not ) oiso { }62019-05-28, by Shinji KONO
-
...2019-05-28, by Shinji KONO
-
...2019-05-28, by Shinji KONO
-
almost ...2019-05-27, by Shinji KONO
-
regurality elimination case2019-05-27, by Shinji KONO
-
fix selection axiom2019-05-27, by Shinji KONO
-
...2019-05-27, by Shinji KONO
-
tri-c<2019-05-27, by Shinji KONO
-
...2019-05-27, by Shinji KONO
-
...2019-05-25, by Shinji KONO
-
fix Select2019-05-25, by Shinji KONO
-
Added tag current for changeset 264784731a672019-05-25, by Shinji KONO
-
clean up2019-05-25, by Shinji KONO
-
== and ∅72019-05-25, by Shinji KONO
-
od∅' {n} = ord→od (o∅ {n})2019-05-24, by Shinji KONO
-
od→lv : {n : Level} → OD {n} → Nat2019-05-24, by Shinji KONO
-
equalitu and internal parametorisity2019-05-24, by Shinji KONO
-
regurality2019-05-24, by Shinji KONO
-
mnimul2019-05-23, by Shinji KONO
-
...2019-05-23, by Shinji KONO
-
...2019-05-23, by Shinji KONO
-
...2019-05-23, by Shinji KONO
-
¬ ( y c< x ) → x ≡ od∅2019-05-23, by Shinji KONO
-
transitive2019-05-22, by Shinji KONO
-
ordinal fixed2019-05-22, by Shinji KONO
-
fix oridinal2019-05-22, by Shinji KONO
-
fix2019-05-21, by Shinji KONO
-
oridnal dead end2019-05-21, by Shinji KONO
-
fix ordinal2019-05-21, by Shinji KONO
-
problem on Ordinal ( OSuc ℵ )2019-05-20, by Shinji KONO
-
posturate OD is isomorphic to Ordinal2019-05-20, by Shinji KONO
-
OD continue2019-05-19, by Shinji KONO
-
OD, HOD, TC2019-05-19, by Shinji KONO
-
dom-ψ2019-05-18, by Shinji KONO
-
...2019-05-18, by Shinji KONO
-
separte level2019-05-18, by Shinji KONO
-
Sup2019-05-17, by Shinji KONO
-
..2019-05-16, by Shinji KONO
-
add transfinite2019-05-16, by Shinji KONO
-
...2019-05-16, by Shinji KONO
-
...2019-05-16, by Shinji KONO
-
fix2019-05-16, by Shinji KONO
-
clean up2019-05-14, by Shinji KONO
-
...2019-05-14, by Shinji KONO