2019-08-11 |
Shinji KONO |
...
|
2019-08-11 |
Shinji KONO |
try transfinite
|
2019-08-11 |
Shinji KONO |
...
|
2019-08-11 |
Shinji KONO |
set theortic function definition using sup
|
2019-08-10 |
Shinji KONO |
does not work
|
2019-08-10 |
Shinji KONO |
recover ε-induction
|
2019-08-09 |
Shinji KONO |
sepration of ordinal from OD
|
2019-08-09 |
Shinji KONO |
TransFinite induction fixed
|
2019-08-08 |
Shinji KONO |
fix Ordinals
|
2019-08-07 |
Shinji KONO |
try to separate Ordinals
|
2019-08-07 |
Shinji KONO |
separate cardinal
|
2019-08-06 |
Shinji KONO |
try func
|
2019-08-05 |
Shinji KONO |
cardinal continue
|
2019-08-04 |
Shinji KONO |
Cardinal start
|
2019-08-02 |
Shinji KONO |
Ord< : {n : Level} { x y : Ordinal {suc n}} → y o< x → Ord x ∋ Ord y is bad decision
|
2019-08-02 |
Shinji KONO |
both
|
2019-08-02 |
Shinji KONO |
separate logic and nat
|
2019-08-01 |
Shinji KONO |
Added tag current for changeset 2c7d45734e3b
|
2019-08-01 |
Shinji KONO |
Axiom of choice from exclude middle
release
|
2019-08-01 |
Shinji KONO |
axiom of choice from exclusive middle done
|
2019-08-01 |
Shinji KONO |
∀-imply-or
|
2019-07-31 |
Shinji KONO |
...
|
2019-07-31 |
Shinji KONO |
try again ..
|
2019-07-31 |
Shinji KONO |
...
|
2019-07-31 |
Shinji KONO |
...
|
2019-07-31 |
Shinji KONO |
Transfinite induction fixed
|
2019-07-31 |
Shinji KONO |
fixing transfinte induction...
|
2019-07-30 |
Shinji KONO |
ε-induction like loop again
|
2019-07-29 |
Shinji KONO |
...
|
2019-07-29 |
Shinji KONO |
ε-induction again
|
2019-07-29 |
Shinji KONO |
curry form
|
2019-07-29 |
Shinji KONO |
another approach
|
2019-07-29 |
Shinji KONO |
transfinite
|
2019-07-29 |
Shinji KONO |
...
|
2019-07-29 |
Shinji KONO |
...
|
2019-07-29 |
Shinji KONO |
emulate ε-induction proof
|
2019-07-28 |
Shinji KONO |
...
|
2019-07-28 |
Shinji KONO |
does not work
|
2019-07-28 |
Shinji KONO |
choice function cannot jump between ordinal level
|
2019-07-26 |
Shinji KONO |
add filter
|
2019-07-25 |
Shinji KONO |
Axiom of choies implies p ∨ ( ¬ p )
|
2019-07-25 |
Shinji KONO |
axiom of choice → p ∨ ¬ p
|
2019-07-23 |
Shinji KONO |
add Todo
|
2019-07-22 |
Shinji KONO |
fix extensionality
|
2019-07-22 |
Shinji KONO |
...
|
2019-07-22 |
Shinji KONO |
...
|
2019-07-21 |
Shinji KONO |
fix zf
|
2019-07-21 |
Shinji KONO |
remove ordinal-definable
|
2019-07-21 |
Shinji KONO |
...
|
2019-07-20 |
Shinji KONO |
new ordinal-definable
|
2019-07-19 |
Shinji KONO |
fix comments
|
2019-07-19 |
Shinji KONO |
ε-induction
release
|
2019-07-19 |
Shinji KONO |
Added tag current for changeset ecb329ba38ac
|
2019-07-19 |
Shinji KONO |
ε-induction done
|
2019-07-19 |
Shinji KONO |
...
|
2019-07-19 |
Shinji KONO |
...
|
2019-07-19 |
Shinji KONO |
...
|
2019-07-19 |
Shinji KONO |
non terminateing on ε-induction
|
2019-07-18 |
Shinji KONO |
...
|
2019-07-18 |
Shinji KONO |
...
|