Mercurial > hg > Members > kono > Proof > ZF-in-agda
graph
-
...2022-12-16, by Shinji KONO
-
order done2022-12-16, by Shinji KONO
-
...2022-12-16, by Shinji KONO
-
...2022-12-16, by Shinji KONO
-
is-minsup done2022-12-16, by Shinji KONO
-
...2022-12-15, by Shinji KONO
-
...2022-12-14, by Shinji KONO
-
...2022-12-14, by Shinji KONO
-
supf-mono done2022-12-14, by Shinji KONO
-
...2022-12-13, by Shinji KONO
-
...2022-12-13, by Shinji KONO
-
...2022-12-13, by Shinji KONO
-
add 0<supfz2022-12-12, by Shinji KONO
-
ic case2022-12-12, by Shinji KONO
-
...2022-12-12, by Shinji KONO
-
equal case2022-12-12, by Shinji KONO
-
...2022-12-12, by Shinji KONO
-
...2022-12-11, by Shinji KONO
-
...2022-12-11, by Shinji KONO
-
another IChain2022-12-11, by Shinji KONO
-
IChain?2022-12-10, by Shinji KONO
-
...2022-12-10, by Shinji KONO
-
...2022-12-10, by Shinji KONO
-
lim2022-12-09, by Shinji KONO
-
sup=u ONDE2022-12-09, by Shinji KONO
-
order (px case) done2022-12-09, by Shinji KONO
-
...2022-12-09, by Shinji KONO
-
order connected2022-12-09, by Shinji KONO
-
...2022-12-09, by Shinji KONO
-
... bad2022-12-09, by Shinji KONO
-
...2022-12-07, by Shinji KONO
-
...2022-12-07, by Shinji KONO
-
...2022-12-07, by Shinji KONO
-
...2022-12-07, by Shinji KONO
-
...2022-12-05, by Shinji KONO
-
is-minsup in px case done2022-12-04, by Shinji KONO
-
...2022-12-04, by Shinji KONO
-
...2022-12-04, by Shinji KONO
-
pxhainx conditon is requied?2022-12-04, by Shinji KONO
-
...2022-12-03, by Shinji KONO
-
...2022-12-03, by Shinji KONO
-
...2022-12-03, by Shinji KONO
-
mf< everywhere2022-12-02, by Shinji KONO
-
...2022-12-02, by Shinji KONO
-
...2022-12-02, by Shinji KONO
-
...2022-12-02, by Shinji KONO
-
...2022-12-01, by Shinji KONO
-
ch-init again, because ch-is-sup require u<x which is not valid supf o∅2022-12-01, by Shinji KONO
-
minsup is not obvious in ZChain2022-11-30, by Shinji KONO
-
...2022-11-30, by Shinji KONO
-
...2022-11-28, by Shinji KONO
-
ChainP removal2022-11-27, by Shinji KONO
-
...2022-11-27, by Shinji KONO
-
...2022-11-26, by Shinji KONO
-
...2022-11-25, by Shinji KONO
-
...2022-11-25, by Shinji KONO
-
supf-< and ZChain1.order is removed2022-11-25, by Shinji KONO
-
...2022-11-25, by Shinji KONO
-
...2022-11-25, by Shinji KONO
-
...2022-11-25, by Shinji KONO
-
...2022-11-24, by Shinji KONO
-
...2022-11-24, by Shinji KONO
-
sa<b2022-11-24, by Shinji KONO
-
trying cscf as odef (UnionCF A f mf ay supf z) w2022-11-24, by Shinji KONO
-
...2022-11-23, by Shinji KONO
-
...2022-11-23, by Shinji KONO
-
...2022-11-23, by Shinji KONO
-
fc-inject is no good2022-11-23, by Shinji KONO
-
maxα2022-11-23, by Shinji KONO
-
IChain recursive record avoided2022-11-20, by Shinji KONO
-
Recursive record IChain2022-11-20, by Shinji KONO
-
...2022-11-20, by Shinji KONO
-
...2022-11-20, by Shinji KONO
-
...2022-11-19, by Shinji KONO
-
...2022-11-18, by Shinji KONO
-
...2022-11-18, by Shinji KONO
-
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