Mercurial > hg > Members > kono > Proof > ZF-in-agda
graph
-
fix pair2019-08-26, by Shinji KONO
-
...2019-08-25, by Shinji KONO
-
new assumption2019-08-25, by Shinji KONO
-
Product2019-08-25, by Shinji KONO
-
...2019-08-25, by Shinji KONO
-
...2019-08-25, by Shinji KONO
-
...2019-08-22, by Shinji KONO
-
fix2019-08-21, by Shinji KONO
-
...2019-08-20, by Shinji KONO
-
ZFProduct2019-08-19, by Shinji KONO
-
...2019-08-18, by Shinji KONO
-
...2019-08-16, by Shinji KONO
-
fix cardinal2019-08-14, by Shinji KONO
-
ac from LEM in abstract ordinal2019-08-13, by Shinji KONO
-
function continue2019-08-12, by Shinji KONO
-
Added tag current for changeset 1b1620e2053c2019-08-11, by Shinji KONO
-
we need ordered pair2019-08-11, by Shinji KONO
-
...2019-08-11, by Shinji KONO
-
try transfinite2019-08-11, by Shinji KONO
-
...2019-08-11, by Shinji KONO
-
set theortic function definition using sup2019-08-11, by Shinji KONO
-
does not work2019-08-10, by Shinji KONO
-
recover ε-induction2019-08-10, by Shinji KONO
-
sepration of ordinal from OD2019-08-09, by Shinji KONO
-
TransFinite induction fixed2019-08-09, by Shinji KONO
-
fix Ordinals2019-08-08, by Shinji KONO
-
try to separate Ordinals2019-08-07, by Shinji KONO
-
separate cardinal2019-08-07, by Shinji KONO
-
try func2019-08-06, by Shinji KONO
-
cardinal continue2019-08-05, by Shinji KONO
-
Cardinal start2019-08-04, by Shinji KONO
-
Ord< : {n : Level} { x y : Ordinal {suc n}} → y o< x → Ord x ∋ Ord y is bad decision2019-08-02, by Shinji KONO
-
both2019-08-02, by Shinji KONO
-
separate logic and nat2019-08-02, by Shinji KONO
-
Added tag current for changeset 2c7d45734e3b2019-08-01, by Shinji KONO
-
axiom of choice from exclusive middle done2019-08-01, by Shinji KONO
-
∀-imply-or2019-08-01, by Shinji KONO
-
...2019-07-31, by Shinji KONO
-
try again ..2019-07-31, by Shinji KONO
-
...2019-07-31, by Shinji KONO
-
...2019-07-31, by Shinji KONO
-
Transfinite induction fixed2019-07-31, by Shinji KONO
-
fixing transfinte induction...2019-07-31, by Shinji KONO
-
ε-induction like loop again2019-07-30, by Shinji KONO
-
...2019-07-29, by Shinji KONO
-
ε-induction again2019-07-29, by Shinji KONO
-
curry form2019-07-29, by Shinji KONO
-
another approach2019-07-29, by Shinji KONO
-
transfinite2019-07-29, by Shinji KONO
-
...2019-07-29, by Shinji KONO
-
...2019-07-29, by Shinji KONO
-
emulate ε-induction proof2019-07-29, by Shinji KONO
-
...2019-07-28, by Shinji KONO
-
does not work2019-07-28, by Shinji KONO
-
choice function cannot jump between ordinal level2019-07-28, by Shinji KONO
-
add filter2019-07-26, by Shinji KONO
-
Axiom of choies implies p ∨ ( ¬ p )2019-07-25, by Shinji KONO
-
axiom of choice → p ∨ ¬ p2019-07-25, by Shinji KONO