Mercurial > hg > Members > kono > Proof > ZF-in-agda
graph
-
first cfcs done2022-11-18, by Shinji KONO
-
...2022-11-18, by Shinji KONO
-
...2022-11-18, by Shinji KONO
-
...2022-11-18, by Shinji KONO
-
...2022-11-18, by Shinji KONO
-
fcs<sup requires <-monotonicity2022-11-18, by Shinji KONO
-
...2022-11-17, by Shinji KONO
-
...2022-11-17, by Shinji KONO
-
...2022-11-17, by Shinji KONO
-
UChain is now u o< x2022-11-16, by Shinji KONO
-
u ≤ x again?2022-11-16, by Shinji KONO
-
SZ1 done2022-11-16, by Shinji KONO
-
... x < & A ?2022-11-16, by Shinji KONO
-
f (supf x) = supf x2022-11-16, by Shinji KONO
-
...2022-11-16, by Shinji KONO
-
...2022-11-16, by Shinji KONO
-
is-max and supf b = supf x2022-11-13, by Shinji KONO
-
is-max?2022-11-13, by Shinji KONO
-
..2022-11-12, by Shinji KONO
-
zc10 : supf c ≡ supf (& A) → {x : Ordinal } → odef A x → ¬ ( c << x ) ?2022-11-11, by Shinji KONO
-
order s o< t is bad2022-11-11, by Shinji KONO
-
...2022-11-11, by Shinji KONO
-
... order supf o< supf is bad?2022-11-11, by Shinji KONO
-
...2022-11-10, by Shinji KONO
-
...2022-11-09, by Shinji KONO
-
chain is now u≤x again2022-11-08, by Shinji KONO
-
... csupf is bad2022-11-08, by Shinji KONO
-
is-max on supf b o< supf x and csupf on supf x o< z is better?2022-11-08, by Shinji KONO
-
is-max condition have to be b o< x2022-11-08, by Shinji KONO
-
...2022-11-08, by Shinji KONO
-
csupf removal?2022-11-07, by Shinji KONO
-
...2022-11-07, by Shinji KONO
-
...2022-11-07, by Shinji KONO
-
...2022-11-07, by Shinji KONO
-
...2022-11-06, by Shinji KONO
-
...2022-11-06, by Shinji KONO
-
...2022-11-06, by Shinji KONO
-
...2022-11-05, by Shinji KONO
-
...2022-11-05, by Shinji KONO
-
removing ch-init is no good because of initialization2022-11-05, by Shinji KONO
-
...2022-11-04, by Shinji KONO
-
...2022-11-04, by Shinji KONO
-
...2022-11-04, by Shinji KONO
-
supf sp = sp ?2022-11-04, by Shinji KONO
-
IsMinSUP< is wrong2022-11-04, by Shinji KONO
-
...2022-11-03, by Shinji KONO
-
IsMinSup contains not HasPrev2022-11-03, by Shinji KONO
-
MinSup onlu2022-11-03, by Shinji KONO
-
...2022-11-03, by Shinji KONO
-
...2022-11-03, by Shinji KONO
-
IsSUP is now min sup2022-11-02, by Shinji KONO
-
...2022-11-01, by Shinji KONO
-
z04 done2022-11-01, by Shinji KONO
-
supf mc = mc2022-11-01, by Shinji KONO
-
...2022-11-01, by Shinji KONO
-
...2022-10-31, by Shinji KONO
-
...2022-10-31, by Shinji KONO
-
avoid memory exhaust2022-10-31, by Shinji KONO
-
...2022-10-31, by Shinji KONO
-
memory exhaust work around2022-10-30, by Shinji KONO
-
bad with trio< o2022-10-30, by Shinji KONO
-
...2022-10-30, by Shinji KONO
-
...2022-10-29, by Shinji KONO
-
avoided2022-10-29, by Shinji KONO
-
not-hasprev z29 and z31 cause memory exhaust2022-10-29, by Shinji KONO
-
...2022-10-28, by Shinji KONO
-
...2022-10-28, by Shinji KONO
-
...2022-10-24, by Shinji KONO
-
...2022-10-24, by Shinji KONO
-
mem exhaust fix on fixpoint2022-10-24, by Shinji KONO
-
resync zorn.agda2022-10-24, by Shinji KONO
-
...2022-10-24, by Shinji KONO
-
memory exhaust work around2022-10-23, by Shinji KONO
-
...2022-10-23, by Shinji KONO
-
...2022-10-23, by Shinji KONO
-
...2022-10-22, by Shinji KONO
-
...2022-10-22, by Shinji KONO
-
...2022-10-20, by Shinji KONO
-
...2022-10-20, by Shinji KONO
-
...2022-10-19, by Shinji KONO
-
supf usp0 instead of supf (& A) ?2022-10-19, by Shinji KONO
-
use supf of zchain for (nmx : ¬ Maximal A ) → ⊥2022-10-18, by Shinji KONO
-
...2022-10-17, by Shinji KONO
-
UnionZF2022-10-17, by Shinji KONO
-
fixpoint?2022-10-16, by Shinji KONO
-
supf u o< supf x2022-10-16, by Shinji KONO
-
supf px o< px is in csupf2022-10-15, by Shinji KONO
-
roll back2022-10-15, by Shinji KONO
-
...2022-10-13, by Shinji KONO
-
...2022-10-12, by Shinji KONO
-
this csupf is bad2022-10-12, by Shinji KONO
-
...2022-10-12, by Shinji KONO
-
...2022-10-12, by Shinji KONO
-
...2022-10-12, by Shinji KONO
-
...2022-10-12, by Shinji KONO
-
...2022-10-11, by Shinji KONO
-
supf (supf x) ≡ supf x is bad2022-10-11, by Shinji KONO
-
...2022-10-11, by Shinji KONO
-
...2022-10-10, by Shinji KONO
-
union equal passed2022-10-10, by Shinji KONO
-
...2022-10-10, by Shinji KONO
-
...2022-10-09, by Shinji KONO
-
...2022-10-09, by Shinji KONO
-
...2022-10-09, by Shinji KONO
-
roll back to u<x2022-10-07, by Shinji KONO
-
UChain u<x to u≤x again2022-10-06, by Shinji KONO
-
...2022-10-06, by Shinji KONO
-
...2022-10-06, by Shinji KONO
-
fixing u<x is no good2022-10-06, by Shinji KONO
-
sp1 = supf (& A)2022-10-06, by Shinji KONO
-
...2022-10-06, by Shinji KONO
-
...2022-10-05, by Shinji KONO
-
x ≤ supf x is no good2022-10-05, by Shinji KONO
-
u < supf z2022-10-05, by Shinji KONO
-
...2022-10-04, by Shinji KONO
-
x≤supfx1 is no good2022-10-03, by Shinji KONO
-
csupf2022-10-03, by Shinji KONO
-
...2022-10-02, by Shinji KONO
-
...2022-10-02, by Shinji KONO
-
...2022-10-02, by Shinji KONO