2024-05-19
2024-05-18←前　次→2024-05-20
Natural number gameを解いているけれど、いよいよ本当に何をしたらよいかわからなくなってきた。
World: Power World Level 9 / 10 : add_sq、World: Advanced Addition World Level 5 / 6 : add_right_eq_zeroが本当にどうしたらいいかわからない
それぞれ以下で止まっている
code:World: Power World Level 9 / 10 : add_sq
induction b with d hd
rw add_zero, mul_zero, two_eq_succ_one, zero_pow_succ
rw add_zero, add_zero
rfl
rw add_succ, pow_two, pow_two, pow_two
rw succ_eq_add_one, succ_eq_add_one, two_mul
rw ← add_mul (d+1) (a+a) (d+1)
code:World: Advanced Addition World Level 5 / 6 : add_right_eq_zero
intro h
cases b with d
rw add_zero at h
exact h
rw add_succ at h
∞-グルーポイド、亜群(グルーポイド)がだいぶ分かってきた
ジャイナ教哲学にスィヤードヴァーダという論理学に関りがありそうなものがある
#日誌