| Metric | Count |
|---|
DefinitionsaddCongr, negCongr, subCongr, addAssocRelabelling, addCommRelabelling, addZeroRelabelling, down, instAdd, instInvolutiveNeg, instNatCast, instNeg, instNegZeroClass, instSub, neg, negAddRelabelling, toLeftMovesAdd, toLeftMovesNeg, toRightMovesAdd, toRightMovesNeg, uniqueStarLeftMoves, uniqueStarRightMoves, up, zeroAddRelabelling | 23 |
Theoremsadd, add_left, add_right, neg, of_neg, sub, addLeftMono, addLeftStrictMono, addRightMono, addRightStrictMono, add_assoc, add_assoc_equiv, add_comm, add_comm_equiv, add_comm_le, add_congr, add_congr_left, add_congr_right, add_eq_zero, add_lf_add_left, add_lf_add_of_le_of_lf, add_lf_add_of_lf_of_le, add_lf_add_right, add_moveLeft_inl, add_moveLeft_inr, add_moveRight_inl, add_moveRight_inr, add_neg_cancel_equiv, add_neg_cancel_le_zero, add_zero, add_zero_equiv, down_leftMoves, down_moveLeft, down_moveRight, down_neg, down_rightMoves, exists_leftMoves_neg, exists_rightMoves_neg, forall_leftMoves_neg, forall_rightMoves_neg, identical_zero, identical_zero_iff, instZeroLEOneClass, isEmpty_leftMoves_add, isEmpty_nat_rightMoves, isEmpty_rightMoves_add, isOption_neg, isOption_neg_neg, le_iff_sub_nonneg, le_neg_iff, leftMoves_add, leftMoves_add_cases, leftMoves_neg, leftMoves_neg_cases, lf_iff_sub_zero_lf, lf_neg_iff, lt_iff_sub_pos, lt_neg_iff, memα΅£_add_iff, memα΅£_neg_iff, memβ_add_iff, memβ_neg_iff, mk_add_moveLeft, mk_add_moveLeft_inl, mk_add_moveLeft_inr, mk_add_moveRight, mk_add_moveRight_inl, mk_add_moveRight_inr, moveLeft_neg, moveLeft_neg_toLeftMovesNeg, moveRight_neg, moveRight_neg_toRightMovesNeg, nat_succ, neg_add, neg_add_cancel_equiv, neg_add_cancel_le_zero, neg_add_le, neg_add_rev, neg_def, neg_down, neg_equiv_iff, neg_equiv_neg_iff, neg_equiv_zero_iff, neg_fuzzy_iff, neg_fuzzy_neg_iff, neg_fuzzy_zero_iff, neg_identical_neg, neg_insertLeft_neg, neg_insertRight_neg, neg_le_iff, neg_le_neg_iff, neg_le_zero_iff, neg_lf_iff, neg_lf_neg_iff, neg_lf_zero_iff, neg_lt_iff, neg_lt_neg_iff, neg_lt_zero_iff, neg_ofLists, neg_star, neg_sub', neg_up, rightMoves_add, rightMoves_add_cases, rightMoves_neg, rightMoves_neg_cases, star_fuzzy_down, star_fuzzy_up, star_fuzzy_zero, star_leftMoves, star_lf_zero, star_moveLeft, star_moveRight, star_rightMoves, sub_congr, sub_congr_left, sub_congr_right, sub_self_equiv, sub_zero, sub_zero_eq_add_zero, up_leftMoves, up_moveLeft, up_moveRight, up_neg, up_rightMoves, zero_add, zero_add_equiv, zero_equiv_neg_iff, zero_fuzzy_neg_iff, zero_le_add_neg_cancel, zero_le_neg_add_cancel, zero_le_neg_iff, zero_lf_neg_iff, zero_lf_one, zero_lf_star, zero_lt_neg_iff, zero_lt_one | 137 |
| Total | 160 |
| Name | Category | Theorems |
|---|
addAssocRelabelling π | CompOp | β |
addCommRelabelling π | CompOp | β |
addZeroRelabelling π | CompOp | β |
down π | CompOp | 8 mathmath: down_leftMoves, star_fuzzy_down, neg_up, down_moveRight, down_neg, down_moveLeft, down_rightMoves, neg_down
|
instAdd π | CompOp | 83 mathmath: nim_add_equiv_zero_iff, birthday_add, rightMoves_add, right_distrib_equiv, mk_mul_moveRight_inl, addLeftMono, grundyValue_nim_add_nim, add_moveLeft_inl, Impartial.add_self, neg_mk_mul_moveRight_inl, mk_add_moveRight_inl, leftMoves_add, add_moveRight_inr, mul_moveRight_inl, mul_moveRight_inr, neg_add, mul_moveLeft_inl, neg_mk_mul_moveLeft_inr, addRightMono, mk_add_moveLeft, addRightStrictMono, Identical.add, nat_succ, mul_moveLeft_inr, sub_zero_eq_add_zero, add_eq_zero, add_comm_le, mk_add_moveLeft_inr, Identical.add_left, add_lf_add_right, quot_left_distrib, zero_add_equiv, left_distrib_equiv, add_congr_left, add_comm_equiv, add_lf_add_of_lf_of_le, Impartial.equiv_iff_add_equiv_zero, zero_add, add_lf_add_left, add_assoc_equiv, nim_add_fuzzy_zero_iff, add_assoc, Numeric.add, neg_add_cancel_equiv, add_zero_equiv, neg_add_rev, add_congr, add_neg_cancel_equiv, memβ_add_iff, mk_add_moveRight, zero_le_add_neg_cancel, add_moveRight_inl, add_moveLeft_inr, zero_le_neg_add_cancel, add_powHalf_succ_self_eq_powHalf, add_lf_add_of_le_of_lf, neg_add_le, mk_add_moveRight_inr, isEmpty_leftMoves_add, mk_mul_moveLeft_inl, mk_mul_moveRight_inr, quot_right_distrib, Impartial.impartial_add, Ordinal.toPGame_nadd, Impartial.equiv_iff_add_equiv_zero', mk_add_moveLeft_inl, neg_mk_mul_moveLeft_inl, mk_mul_moveLeft_inr, half_add_half_equiv_one, memα΅£_add_iff, neg_mk_mul_moveRight_inr, add_congr_right, addLeftStrictMono, add_comm, quot_add, Surreal.mk_add, add_neg_cancel_le_zero, neg_add_cancel_le_zero, add_zero, nim_add_nim_equiv, Identical.add_right, grundyValue_add, isEmpty_rightMoves_add
|
instInvolutiveNeg π | CompOp | β |
instNatCast π | CompOp | 6 mathmath: quot_natCast, nat_succ, Ordinal.toPGame_natCast, birthday_natCast, isEmpty_nat_rightMoves, numeric_nat
|
instNeg π | CompOp | 94 mathmath: Identical.neg, Surreal.Multiplication.P2_neg_left, exists_leftMoves_neg, Surreal.Multiplication.ih4_neg, Surreal.Multiplication.P24_neg_right, quot_neg_mul, neg_lf_neg_iff, isOption_neg, neg_le_neg_iff, neg_mk_mul_moveRight_inl, neg_lt_zero_iff, neg_lt_neg_iff, isOption_neg_neg, quot_mul_neg, mulOption_neg_neg, neg_star, rightMoves_mul_iff, neg_add, Surreal.Multiplication.ih1_neg_left, neg_mk_mul_moveLeft_inr, lt_neg_iff, neg_equiv_iff, neg_ofLists, neg_fuzzy_zero_iff, neg_insertRight_neg, neg_fuzzy_neg_iff, Surreal.Multiplication.mulOption_lt, Surreal.Multiplication.P24_neg_left, neg_equiv_zero_iff, Surreal.Multiplication.P4_neg_left, lf_neg_iff, Surreal.Multiplication.P3_of_ih, le_neg_iff, leftMoves_mul_iff, moveRight_neg, grundyValue_neg, neg_fuzzy_iff, forall_rightMoves_neg, forall_leftMoves_neg, neg_lt_iff, neg_sub', Numeric.neg, Surreal.Multiplication.mulOptionsLTMul_of_numeric, neg_add_cancel_equiv, neg_equiv_neg_iff, impartial_def, zero_lt_neg_iff, neg_add_rev, Surreal.Multiplication.mulOption_lt_iff_P1, memα΅£_neg_iff, moveLeft_neg_toLeftMovesNeg, add_neg_cancel_equiv, Impartial.impartial_neg, zero_le_add_neg_cancel, zero_le_neg_add_cancel, neg_lf_zero_iff, inv_eq_of_lf_zero, neg_add_le, birthday_neg, moveRight_neg_toRightMovesNeg, exists_rightMoves_neg, leftMoves_neg, Surreal.Multiplication.mulOption_lt_of_lt, neg_up, quot_neg, zero_le_neg_iff, neg_lf_iff, memβ_neg_iff, neg_le_iff, neg_mk_mul_moveLeft_inl, Surreal.Multiplication.P2_neg_right, Surreal.Multiplication.ih24_neg, Surreal.Multiplication.ih1_neg_right, mul_neg, rightMoves_neg, neg_mk_mul_moveRight_inr, neg_le_zero_iff, neg_insertLeft_neg, neg_identical_neg, Surreal.Multiplication.P3_neg, quot_neg_mul_neg, neg_nim, Impartial.neg_equiv_self, neg_mul, add_neg_cancel_le_zero, neg_add_cancel_le_zero, zero_lf_neg_iff, zero_equiv_neg_iff, zero_fuzzy_neg_iff, neg_birthday_le, neg_def, neg_down, Surreal.Multiplication.P4_neg_right, moveLeft_neg
|
instNegZeroClass π | CompOp | β |
instSub π | CompOp | 29 mathmath: sub_self_equiv, sub_congr_right, sub_congr, mk_mul_moveRight_inl, quot_right_distrib_sub, neg_mk_mul_moveRight_inl, Numeric.sub, sub_congr_left, mul_moveRight_inl, mul_moveRight_inr, Identical.sub, mul_moveLeft_inl, birthday_sub, neg_mk_mul_moveLeft_inr, quot_left_distrib_sub, lt_iff_sub_pos, lf_iff_sub_zero_lf, mul_moveLeft_inr, sub_zero, sub_zero_eq_add_zero, neg_sub', le_iff_sub_nonneg, mk_mul_moveLeft_inl, mk_mul_moveRight_inr, neg_mk_mul_moveLeft_inl, Surreal.mk_sub, mk_mul_moveLeft_inr, neg_mk_mul_moveRight_inr, quot_sub
|
neg π | CompOp | β |
negAddRelabelling π | CompOp | β |
toLeftMovesAdd π | CompOp | 2 mathmath: add_moveLeft_inl, add_moveLeft_inr
|
toLeftMovesNeg π | CompOp | 5 mathmath: exists_leftMoves_neg, mulOption_neg_neg, forall_leftMoves_neg, moveLeft_neg_toLeftMovesNeg, moveLeft_neg
|
toRightMovesAdd π | CompOp | 2 mathmath: add_moveRight_inr, add_moveRight_inl
|
toRightMovesNeg π | CompOp | 5 mathmath: mulOption_neg_neg, moveRight_neg, forall_rightMoves_neg, moveRight_neg_toRightMovesNeg, exists_rightMoves_neg
|
uniqueStarLeftMoves π | CompOp | β |
uniqueStarRightMoves π | CompOp | β |
up π | CompOp | 8 mathmath: up_leftMoves, up_rightMoves, up_neg, up_moveLeft, star_fuzzy_up, up_moveRight, neg_up, neg_down
|
zeroAddRelabelling π | CompOp | β |