| Name | Category | Theorems |
|---|
PGame 📖 | CompData | 391 mathmath: PGame.nim_add_equiv_zero_iff, PGame.lt_or_equiv_or_gt, PGame.Identical.neg, PGame.grundyValue_eq_sInf_moveLeft, PGame.one_leftMoves, PGame.not_lf, PGame.star_lf_zero, PGame.zero_le_of_isEmpty_rightMoves, PGame.Impartial.fuzzy_zero_iff_gf, PGame.zero_rightMoves, Surreal.Multiplication.P2_neg_left, PGame.exists_leftMoves_neg, PGame.one_rightMoves, PGame.Impartial.le_zero_iff, Surreal.Multiplication.ih4_neg, Surreal.Multiplication.P24_neg_right, PGame.quot_neg_mul, PGame.sub_self_equiv, PGame.birthday_add, PGame.neg_lf_neg_iff, PGame.rightMoves_add, PGame.powHalf_succ_lt_one, PGame.isOption_neg, PGame.Impartial.mk'_add_self, PGame.neg_le_neg_iff, PGame.right_distrib_equiv, PGame.lt_iff_le_and_lf, PGame.ofLists_moveLeft, PGame.quot_one, PGame.grundyValue_eq_iff_equiv_nim, PGame.lt_or_fuzzy_of_lf, PGame.mk_mul_moveRight_inl, PGame.one_mul_equiv, PGame.birthday_one, Surreal.Multiplication.numeric_mul_option, PGame.addLeftMono, PGame.lt_iff_exists_le, PGame.grundyValue_nim_add_nim, Surreal.zero_def, PGame.Impartial.equiv_zero_iff_le, PGame.add_moveLeft_inl, PGame.powHalf_succ_lt_powHalf, Surreal.Multiplication.mulOption_lt_mul_iff_P3, PGame.equiv_iff_game_eq, PGame.isEmpty_leftMoves_mul, PGame.quot_right_distrib_sub, PGame.le_birthday, PGame.fuzzy_iff_game_fuzzy, PGame.lf_iff_exists_le, PGame.Impartial.add_self, PGame.neg_mk_mul_moveRight_inl, PGame.invVal_isEmpty, PGame.le_of_forall_lf, PGame.grundyValue_eq_iff_equiv, PGame.Numeric.sub, PGame.mk_add_moveRight_inl, PGame.neg_lt_zero_iff, PGame.leftMoves_add, Ordinal.toPGame_zero, PGame.neg_lt_neg_iff, PGame.isOption_neg_neg, PGame.quot_natCast, PGame.quot_mul_neg, PGame.lt_or_equiv_or_gf, PGame.add_moveRight_inr, PGame.mul_moveRight_inl, PGame.mulOption_neg_neg, Ordinal.toPGame_nmul, PGame.lt_iff_game_lt, PGame.neg_star, PGame.inv_one_equiv, PGame.rightMoves_mul_iff, PGame.lf_zero_le, PGame.mul_moveRight_inr, PGame.neg_add, PGame.star_moveRight, Game.zero_def, PGame.quot_mul_one, PGame.nim_one_equiv, Surreal.mk_eq_mk, PGame.Identical.sub, PGame.mul_moveLeft_inl, Surreal.Multiplication.numeric_of_ih, PGame.instIsEquivEquiv, Surreal.Multiplication.ih1_neg_left, PGame.birthday_sub, PGame.star_fuzzy_zero, PGame.neg_mk_mul_moveLeft_inr, PGame.powHalf_le_one, PGame.ofLists_moveRight, PGame.quot_left_distrib_sub, PGame.addRightMono, PGame.equiv_comm, PGame.Numeric.mul, PGame.Impartial.nonneg, PGame.equiv_refl, Game.birthday_eq_pGameBirthday, PGame.le_iff_forall_lt, PGame.one_moveLeft, PGame.instIsTransIdentical, PGame.mk_add_moveLeft, PGame.addRightStrictMono, PGame.Identical.add, PGame.le_def, PGame.mk_lf_mk, PGame.mul_one_equiv, PGame.nat_succ, PGame.lt_neg_iff, PGame.equiv_def, PGame.instReflIdentical, PGame.LF.not_equiv', PGame.lt_iff_sub_pos, PGame.LF.not_ge, PGame.grundyValue_zero, PGame.Fuzzy.not_equiv, PGame.lf_iff_sub_zero_lf, Ordinal.toPGame_one, PGame.mul_moveLeft_inr, PGame.lf_or_equiv_or_gf, Surreal.Multiplication.numeric_option_mul_option, PGame.neg_equiv_iff, PGame.ofLists_moveRight', PGame.sub_zero, PGame.Fuzzy.not_equiv', PGame.Equiv.isEmpty, PGame.Relabelling.le, PGame.neg_ofLists, PGame.sub_zero_eq_add_zero, PGame.add_eq_zero, PGame.lt_or_equiv_or_gt_or_fuzzy, PGame.mul_zero_equiv, PGame.add_comm_le, PGame.neg_fuzzy_zero_iff, PGame.grundyValue_eq_sInf_moveRight, PGame.mk_add_moveLeft_inr, PGame.Identical.add_left, PGame.neg_insertRight_neg, PGame.add_lf_add_right, PGame.nim_fuzzy_zero_of_ne_zero, PGame.Impartial.exists_left_move_equiv_iff_fuzzy_zero, PGame.zero_leftMoves, PGame.quot_left_distrib, PGame.zero_lf_one, PGame.Impartial.equiv_zero_iff_ge, PGame.zero_add_equiv, PGame.left_distrib_equiv, PGame.Numeric.left_lt_right, PGame.not_le, PGame.neg_fuzzy_neg_iff, Surreal.Multiplication.mulOption_lt, Surreal.Multiplication.P24_neg_left, PGame.zero_mul, PGame.equiv_congr_right, Surreal.zero_lt_mk, PGame.mulOption_symm, PGame.Identical.ge, PGame.mul_assoc_equiv, PGame.quot_one_mul, PGame.instSymmIdentical, PGame.Identical.le, PGame.equiv_congr_left, PGame.neg_equiv_zero_iff, Surreal.Multiplication.P4_neg_left, PGame.le_zero, PGame.mk_le_mk, PGame.wf_subsequent, PGame.lf_zero, PGame.isEmpty_zero_rightMoves, PGame.birthday_zero, PGame.inv'_one_equiv, PGame.add_comm_equiv, PGame.Impartial.mk'_neg_equiv_self, PGame.Impartial.equiv_iff_add_equiv_zero, PGame.zero_lt_one, PGame.lf_neg_iff, PGame.rightMoves_ofLists, PGame.zero_add, PGame.zero_le, PGame.Impartial.not_fuzzy_zero_iff, PGame.Impartial.lf_zero_iff, Surreal.Multiplication.P3_of_ih, PGame.le_neg_iff, PGame.equiv_nim_grundyValue, PGame.isEmpty_one_rightMoves, PGame.leftMoves_mul_iff, PGame.le_zero_of_isEmpty_leftMoves, PGame.moveRight_neg, PGame.zero_lf_star, PGame.bddAbove_of_small, PGame.LF.lt, Ordinal.toPGame_nonneg, PGame.insertLeft_equiv_of_lf, PGame.grundyValue_neg, PGame.add_lf_add_left, PGame.neg_fuzzy_iff, PGame.forall_rightMoves_neg, PGame.forall_leftMoves_neg, PGame.bddBelow_of_small, Ordinal.mk_toPGame, PGame.neg_lt_iff, PGame.add_assoc_equiv, PGame.nim_add_fuzzy_zero_iff, PGame.Impartial.not_equiv_zero_iff, PGame.powHalf_succ_le_powHalf, PGame.neg_sub', PGame.Numeric.neg, PGame.zero_lf_le, PGame.le_zero_lf, PGame.add_assoc, PGame.Impartial.nonpos, PGame.up_neg, PGame.Numeric.add, PGame.identical_zero_iff, PGame.lt_def, PGame.identical_zero, PGame.neg_add_cancel_equiv, PGame.Impartial.fuzzy_zero_iff_lf, PGame.neg_equiv_neg_iff, PGame.Impartial.equiv_or_fuzzy_zero, PGame.mul_comm_equiv, PGame.add_zero_equiv, PGame.impartial_def, Ordinal.toPGame_le, PGame.nim_zero_equiv, PGame.zero_lt_neg_iff, Ordinal.toPGame_natCast, PGame.neg_add_rev, PGame.quot_mul_comm, Surreal.Multiplication.mulOption_lt_iff_P1, PGame.rightMoves_mul, PGame.zero_lf_inv', PGame.memᵣ_neg_iff, PGame.moveLeft_neg_toLeftMovesNeg, PGame.equiv_rfl, PGame.add_neg_cancel_equiv, PGame.Impartial.impartial_neg, Ordinal.toGame_nmul, PGame.quot_mul_zero, PGame.up_moveLeft, PGame.instIrreflFuzzy, Surreal.Multiplication.numeric_option_mul, PGame.memₗ_add_iff, PGame.instZeroLEOneClass, PGame.not_lt, PGame.mk_add_moveRight, PGame.LF.not_equiv, Surreal.Multiplication.P1_of_ih, PGame.zero_le_add_neg_cancel, PGame.powHalf_moveLeft, PGame.powHalf_pos, PGame.add_moveRight_inl, PGame.add_moveLeft_inr, Ordinal.toPGame_lt_iff, PGame.zero_le_neg_add_cancel, PGame.zero_mul_equiv, PGame.le_iff_game_le, PGame.inv'_one, PGame.neg_lf_zero_iff, PGame.add_powHalf_succ_self_eq_powHalf, PGame.zero_le_powHalf, PGame.bddBelow_range_of_small, PGame.neg_add_le, PGame.Identical.equiv, PGame.birthday_neg, PGame.Numeric.lt_moveRight, PGame.moveRight_neg_toRightMovesNeg, PGame.nim_equiv_iff_eq, PGame.Impartial.forall_rightMoves_fuzzy_iff_equiv_zero, PGame.le_or_gf, PGame.isEmpty_zero_leftMoves, PGame.exists_rightMoves_neg, PGame.wf_isOption, PGame.leftMoves_neg, PGame.inv_zero, PGame.equiv_of_eq, PGame.LF.le, PGame.le_iff_sub_nonneg, Game.birthday_star, PGame.instSymmFuzzy, PGame.quot_mul_assoc, PGame.leftMoves_mul, PGame.leftMoves_ofLists, PGame.mk_add_moveRight_inr, PGame.isEmpty_leftMoves_add, PGame.one_mul, PGame.mk_mul_moveLeft_inl, PGame.numeric_one, PGame.Relabelling.equiv, PGame.neg_up, PGame.down_moveRight, Surreal.zero_le_mk, PGame.quot_neg, PGame.zero_le_neg_iff, PGame.neg_lf_iff, PGame.mk_mul_moveRight_inr, PGame.down_neg, PGame.quot_right_distrib, PGame.instIsEquivIdentical, PGame.birthday_natCast, PGame.isEmpty_rightMoves_mul, PGame.bddAbove_range_of_small, Surreal.mk_eq_zero, PGame.numeric_zero, PGame.Impartial.impartial_add, PGame.memₗ_neg_iff, PGame.insertRight_equiv_of_lf, PGame.neg_le_iff, PGame.quot_zero_mul, Ordinal.toPGame_nadd, PGame.instIsTransSubsequent, PGame.Impartial.equiv_iff_add_equiv_zero', PGame.Impartial.forall_leftMoves_fuzzy_iff_equiv_zero, PGame.Numeric.moveLeft_le, PGame.mk_add_moveLeft_inl, PGame.zero_lf, PGame.LF.not_gt, PGame.neg_mk_mul_moveLeft_inl, Surreal.mk_sub, Surreal.Multiplication.P2_neg_right, PGame.numeric_def, PGame.mk_mul_moveLeft_inr, PGame.insertRight_le, PGame.half_add_half_equiv_one, Game.birthday_quot_le_pGameBirthday, PGame.memᵣ_add_iff, PGame.Impartial.exists_right_move_equiv_iff_fuzzy_zero, Surreal.Multiplication.ih24_neg, PGame.Relabelling.ge, Ordinal.toPGame_injective, Surreal.Multiplication.ih1_neg_right, PGame.mul_one, PGame.mul_neg, PGame.rightMoves_neg, PGame.neg_mk_mul_moveRight_inr, PGame.neg_le_zero_iff, PGame.star_moveLeft, PGame.neg_insertLeft_neg, Ordinal.toPGame_le_iff, PGame.inv'_zero_equiv, PGame.grundyValue_iff_equiv_zero, PGame.isEmpty_nat_rightMoves, PGame.neg_identical_neg, Surreal.Multiplication.P3_neg, PGame.Numeric.moveLeft_lt, PGame.lt_of_lf, PGame.quot_neg_mul_neg, PGame.neg_nim, PGame.instIrreflLF, PGame.zero_le_lf, PGame.addLeftStrictMono, PGame.Impartial.neg_equiv_self, PGame.powHalf_zero, PGame.mul_comm, PGame.quot_zero, PGame.add_comm, Surreal.mk_lt_mk, PGame.quot_add, Surreal.mk_add, PGame.neg_mul, PGame.quot_sub, PGame.add_neg_cancel_le_zero, PGame.lf_iff_lt, PGame.neg_add_cancel_le_zero, PGame.add_zero, PGame.zero_lf_neg_iff, Ordinal.toPGame_lt, PGame.nim_add_nim_equiv, PGame.ofLists_moveLeft', PGame.zero_equiv_neg_iff, PGame.lf_iff_game_lf, Ordinal.toPGameEmbedding_apply, PGame.Identical.add_right, PGame.Impartial.impartial_zero, PGame.mul_zero, PGame.le_insertLeft, PGame.Numeric.le_moveRight, Ordinal.toPGame_equiv_iff, PGame.zero_fuzzy_neg_iff, PGame.neg_birthday_le, Surreal.mk_le_mk, PGame.grundyValue_add, PGame.inv_one, PGame.neg_def, PGame.neg_down, PGame.isEmpty_rightMoves_add, PGame.numeric_nat, Surreal.Multiplication.P4_neg_right, PGame.le_iff_forall_lf, PGame.le_of_lf, PGame.lf_iff_lt_or_fuzzy, PGame.moveLeft_neg
|
| Name | Category | Theorems |
|---|
Identical 📖 | MathDef | 37 mathmath: identical_comm, Identical.refl, Identical.rfl, memₗ_def, instIsTransIdentical, instReflIdentical, sub_zero, add_eq_zero, zero_mul, instSymmIdentical, memᵣ_def, zero_add, add_assoc, identical_zero_iff, identical_zero, neg_add_rev, memᵣ_neg_iff, identical_of_isEmpty, memₗ_add_iff, inv'_one, Identical.ext_iff, identical_of_eq, one_mul, identical_iff', instIsEquivIdentical, memₗ_neg_iff, memᵣ_add_iff, mul_one, identical_iff, neg_identical_neg, Identical.ext, mul_comm, add_comm, neg_mul, add_zero, mul_zero, inv_one
|
IsOption 📖 | CompData | 6 mathmath: isOption_neg, isOption_neg_neg, IsOption.mk_right, IsOption.mk_left, isOption_iff, wf_isOption
|
LeftMoves 📖 | CompOp | 53 mathmath: grundyValue_eq_sInf_moveLeft, one_leftMoves, exists_leftMoves_neg, relabel_moveLeft', add_moveLeft_inl, isEmpty_leftMoves_mul, isEmpty_nim_zero_leftMoves, Ordinal.one_toPGame_leftMoves_default_eq, leftMoves_add, mul_moveRight_inl, powHalf_leftMoves, mulOption_neg_neg, mul_moveRight_inr, mul_moveLeft_inl, up_leftMoves, Ordinal.isEmpty_zero_toPGame_leftMoves, star_leftMoves, mul_moveLeft_inr, relabel_moveLeft, zero_leftMoves, down_leftMoves, default_nim_one_leftMoves_eq, moveRight_neg, forall_rightMoves_neg, forall_leftMoves_neg, identical_zero_iff, birthday_def, leftMoves_nim, rightMoves_mul, birthday_eq_zero, moveLeft_neg_toLeftMovesNeg, Ordinal.toPGame_leftMoves, add_moveLeft_inr, toLeftMovesNim_symm_lt, moveRight_neg_toRightMovesNeg, isEmpty_zero_leftMoves, exists_rightMoves_neg, leftMoves_neg, moveLeft_toLeftMovesNim, Ordinal.toPGame_moveLeft, leftMoves_mul, leftMoves_ofLists, isEmpty_leftMoves_add, leftMoves_mk, Ordinal.to_leftMoves_one_toPGame_symm, identical_iff, rightMoves_neg, Relabelling.mk'_leftMovesEquiv, Ordinal.toLeftMovesToPGame_symm_lt, moveLeft_nim, toLeftMovesNim_one_symm, Ordinal.toPGame_moveLeft', moveLeft_neg
|
Relabelling 📖 | CompData | — |
RightMoves 📖 | CompOp | 52 mathmath: default_nim_one_rightMoves_eq, zero_rightMoves, exists_leftMoves_neg, one_rightMoves, Ordinal.isEmpty_toPGame_rightMoves, rightMoves_add, isEmpty_powHalf_zero_rightMoves, relabel_moveRight, rightMoves_mk, add_moveRight_inr, mul_moveRight_inl, Ordinal.toPGame_rightMoves, mulOption_neg_neg, mul_moveRight_inr, mul_moveLeft_inl, toRightMovesNim_one_symm, mul_moveLeft_inr, up_rightMoves, Relabelling.mk'_rightMovesEquiv, grundyValue_eq_sInf_moveRight, moveRight_nim, isEmpty_zero_rightMoves, rightMoves_ofLists, isEmpty_one_rightMoves, moveRight_neg, forall_rightMoves_neg, forall_leftMoves_neg, identical_zero_iff, rightMoves_nim, relabel_moveRight', birthday_def, rightMoves_mul, birthday_eq_zero, moveLeft_neg_toLeftMovesNeg, add_moveRight_inl, moveRight_neg_toRightMovesNeg, exists_rightMoves_neg, leftMoves_neg, leftMoves_mul, powHalf_succ_rightMoves, isEmpty_rightMoves_mul, identical_iff, rightMoves_neg, isEmpty_nat_rightMoves, down_rightMoves, star_rightMoves, powHalf_zero_rightMoves, moveRight_toRightMovesNim, isEmpty_nim_zero_rightMoves, toRightMovesNim_symm_lt, isEmpty_rightMoves_add, moveLeft_neg
|
Subsequent 📖 | MathDef | 11 mathmath: Subsequent.moveRight_mk_left, Subsequent.mk_left, Subsequent.moveRight, wf_subsequent, Subsequent.moveLeft_mk_right, Subsequent.mk_right, Subsequent.mk_right', instIsTransSubsequent, Subsequent.moveLeft_mk_left, Subsequent.moveRight_mk_right, Subsequent.moveLeft
|
identicalSetoid 📖 | CompOp | — |
insertLeft 📖 | CompOp | 6 mathmath: neg_insertRight_neg, insertLeft_equiv_of_lf, insertRight_insertLeft, neg_insertLeft_neg, insertLeft_numeric, le_insertLeft
|
insertRight 📖 | CompOp | 6 mathmath: neg_insertRight_neg, insertRight_numeric, insertRight_insertLeft, insertRight_equiv_of_lf, insertRight_le, neg_insertLeft_neg
|
instInhabited 📖 | CompOp | — |
instOnePGame 📖 | CompOp | 27 mathmath: one_leftMoves, one_rightMoves, powHalf_succ_lt_one, quot_one, one_mul_equiv, birthday_one, inv_one_equiv, quot_mul_one, powHalf_le_one, one_moveLeft, mul_one_equiv, nat_succ, Ordinal.toPGame_one, zero_lf_one, quot_one_mul, inv'_one_equiv, zero_lt_one, isEmpty_one_rightMoves, instZeroLEOneClass, inv'_one, one_mul, numeric_one, half_add_half_equiv_one, mul_one, inv'_zero_equiv, powHalf_zero, inv_one
|
instWellFoundedRelation 📖 | CompOp | — |
instZero 📖 | CompOp | 105 mathmath: nim_add_equiv_zero_iff, star_lf_zero, zero_le_of_isEmpty_rightMoves, Impartial.fuzzy_zero_iff_gf, zero_rightMoves, Impartial.le_zero_iff, sub_self_equiv, Surreal.zero_def, Impartial.equiv_zero_iff_le, Impartial.add_self, invVal_isEmpty, neg_lt_zero_iff, Ordinal.toPGame_zero, lf_zero_le, star_moveRight, SetTheory.Game.zero_def, star_fuzzy_zero, Impartial.nonneg, one_moveLeft, lt_iff_sub_pos, grundyValue_zero, lf_iff_sub_zero_lf, sub_zero, Equiv.isEmpty, sub_zero_eq_add_zero, add_eq_zero, mul_zero_equiv, neg_fuzzy_zero_iff, nim_fuzzy_zero_of_ne_zero, Impartial.exists_left_move_equiv_iff_fuzzy_zero, zero_leftMoves, zero_lf_one, Impartial.equiv_zero_iff_ge, zero_add_equiv, zero_mul, Surreal.zero_lt_mk, neg_equiv_zero_iff, le_zero, lf_zero, isEmpty_zero_rightMoves, birthday_zero, Impartial.equiv_iff_add_equiv_zero, zero_lt_one, zero_add, zero_le, Impartial.not_fuzzy_zero_iff, Impartial.lf_zero_iff, le_zero_of_isEmpty_leftMoves, zero_lf_star, Ordinal.toPGame_nonneg, nim_add_fuzzy_zero_iff, Impartial.not_equiv_zero_iff, zero_lf_le, le_zero_lf, Impartial.nonpos, up_neg, identical_zero_iff, identical_zero, neg_add_cancel_equiv, Impartial.fuzzy_zero_iff_lf, Impartial.equiv_or_fuzzy_zero, add_zero_equiv, nim_zero_equiv, zero_lt_neg_iff, zero_lf_inv', add_neg_cancel_equiv, quot_mul_zero, up_moveLeft, instZeroLEOneClass, zero_le_add_neg_cancel, powHalf_moveLeft, powHalf_pos, zero_le_neg_add_cancel, zero_mul_equiv, neg_lf_zero_iff, zero_le_powHalf, Impartial.forall_rightMoves_fuzzy_iff_equiv_zero, isEmpty_zero_leftMoves, inv_zero, le_iff_sub_nonneg, down_moveRight, Surreal.zero_le_mk, zero_le_neg_iff, down_neg, Surreal.mk_eq_zero, numeric_zero, quot_zero_mul, Impartial.equiv_iff_add_equiv_zero', Impartial.forall_leftMoves_fuzzy_iff_equiv_zero, zero_lf, Impartial.exists_right_move_equiv_iff_fuzzy_zero, neg_le_zero_iff, star_moveLeft, inv'_zero_equiv, grundyValue_iff_equiv_zero, zero_le_lf, quot_zero, add_neg_cancel_le_zero, neg_add_cancel_le_zero, add_zero, zero_lf_neg_iff, zero_equiv_neg_iff, Impartial.impartial_zero, mul_zero, zero_fuzzy_neg_iff
|
memᵣ 📖 | MathDef | 9 mathmath: memᵣ.congr_right, memᵣ_def, moveRight_memᵣ, memᵣ_neg_iff, Identical.ext_iff, identical_iff', memₗ_neg_iff, memᵣ_add_iff, memᵣ.congr_left
|
memₗ 📖 | MathDef | 9 mathmath: memₗ_def, memₗ.congr_right, memᵣ_neg_iff, memₗ_add_iff, Identical.ext_iff, identical_iff', memₗ_neg_iff, memₗ.congr_left, moveLeft_memₗ
|
moveLeft 📖 | CompOp | 83 mathmath: grundyValue_eq_sInf_moveLeft, relabel_moveLeft', ofLists_moveLeft, lt_iff_exists_le, add_moveLeft_inl, Surreal.Multiplication.mulOption_lt_mul_iff_P3, Surreal.Multiplication.ih3_of_ih, lf_iff_exists_le, birthday_moveLeft_lt, rightResponse_spec, moveLeft_mk, mul_moveRight_inl, mul_moveRight_inr, memₗ_def, mul_moveLeft_inl, neg_mk_mul_moveLeft_inr, leftResponse_spec, le_iff_forall_lt, one_moveLeft, lt_birthday_iff, mk_add_moveLeft, le_def, mul_moveLeft_inr, Numeric.moveLeft, mk_add_moveLeft_inr, Impartial.exists_left_move_equiv_iff_fuzzy_zero, relabel_moveLeft, Numeric.left_lt_right, nim_one_moveLeft, le_zero, lf_zero, Ordinal.one_toPGame_moveLeft, Subsequent.moveLeft_mk_right, zero_le, Surreal.Multiplication.P3_of_ih, Surreal.mk_moveLeft_lt_mk, lf_def, leftMoves_mul_iff, moveRight_neg, zero_lf_le, le_zero_lf, Impartial.moveLeft_impartial, lt_def, isOption_iff, Surreal.Multiplication.P24_of_ih, impartial_def, birthday_def, Surreal.Multiplication.mulOption_lt_iff_P1, moveLeft_neg_toLeftMovesNeg, up_moveLeft, powHalf_moveLeft, add_moveLeft_inr, moveRight_neg_toRightMovesNeg, moveLeft_toLeftMovesNim, Ordinal.toPGame_moveLeft, moveLeft_lf, mk_mul_moveLeft_inl, LE.le.moveLeft_lf, identical_iff', Identical.moveLeft, exists_grundyValue_moveLeft_of_lt, Ordinal.toPGame_moveLeft_hEq, Impartial.forall_leftMoves_fuzzy_iff_equiv_zero, Numeric.moveLeft_le, mk_add_moveLeft_inl, zero_lf, neg_mk_mul_moveLeft_inl, numeric_def, mk_mul_moveLeft_inr, Subsequent.moveLeft_mk_left, identical_iff, star_moveLeft, down_moveLeft, Subsequent.moveLeft, Numeric.moveLeft_lt, moveLeft_nim_heq, moveLeft_nim, moveLeft_lf_of_le, ofLists_moveLeft', moveLeft_memₗ, Ordinal.toPGame_moveLeft', le_iff_forall_lf, moveLeft_neg
|
moveRecOn 📖 | CompOp | — |
moveRight 📖 | CompOp | 72 mathmath: Surreal.mk_lt_mk_moveRight, mk_mul_moveRight_inl, Identical.moveRight, lt_iff_exists_le, lf_iff_exists_le, neg_mk_mul_moveRight_inl, mk_add_moveRight_inl, relabel_moveRight, Subsequent.moveRight_mk_left, rightResponse_spec, add_moveRight_inr, mul_moveRight_inl, rightMoves_mul_iff, lf_zero_le, mul_moveRight_inr, star_moveRight, exists_grundyValue_moveRight_of_lt, ofLists_moveRight, leftResponse_spec, le_iff_forall_lt, lt_birthday_iff, le_def, mul_moveLeft_inr, ofLists_moveRight', Impartial.moveRight_impartial, grundyValue_eq_sInf_moveRight, moveRight_nim, Subsequent.moveRight, Numeric.left_lt_right, memᵣ_def, le_zero, lf_zero, moveRight_memᵣ, zero_le, lf_def, moveRight_neg, lt_def, isOption_iff, impartial_def, relabel_moveRight', birthday_def, moveLeft_neg_toLeftMovesNeg, mk_add_moveRight, add_moveRight_inl, LE.le.lf_moveRight, Numeric.lt_moveRight, moveRight_neg_toRightMovesNeg, Impartial.forall_rightMoves_fuzzy_iff_equiv_zero, up_moveRight, birthday_moveRight_lt, mk_add_moveRight_inr, down_moveRight, lf_moveRight, identical_iff', Numeric.moveRight, mk_mul_moveRight_inr, nim_one_moveRight, zero_lf, numeric_def, Impartial.exists_right_move_equiv_iff_fuzzy_zero, identical_iff, neg_mk_mul_moveRight_inr, Subsequent.moveRight_mk_right, moveRight_nim_heq, zero_le_lf, lf_moveRight_of_le, powHalf_succ_moveRight, moveRight_toRightMovesNim, Numeric.le_moveRight, moveRight_mk, le_iff_forall_lf, moveLeft_neg
|
ofLists 📖 | CompOp | 7 mathmath: ofLists_moveLeft, ofLists_moveRight, ofLists_moveRight', neg_ofLists, rightMoves_ofLists, leftMoves_ofLists, ofLists_moveLeft'
|
relabel 📖 | CompOp | 4 mathmath: relabel_moveLeft', relabel_moveRight, relabel_moveLeft, relabel_moveRight'
|
relabelRelabelling 📖 | CompOp | — |
tacticPgame_wf_tac 📖 | CompOp | — |
toOfListsLeftMoves 📖 | CompOp | — |
toOfListsRightMoves 📖 | CompOp | — |
uniqueOneLeftMoves 📖 | CompOp | — |
«binderPred∈ᵣ_» 📖 | CompOp | — |
«binderPred∈ₗ_» 📖 | CompOp | — |
«term_∈ᵣ_» 📖 | CompOp | — |
«term_∈ₗ_» 📖 | CompOp | — |
«term_≡_» 📖 | CompOp | — |
«term_≡r_» 📖 | CompOp | — |