Mercurial > hg > Members > kono > Proof > ZF-in-agda
graph
-
...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