Filip Cernatescu asked me to post this.
-------- Forwarded Message --------
Subject: New metamath game on Android
Resent-From: nm
Date: Tue, 1 Sep 2020 12:22:06 +0000 (UTC)
From: Cernatescu Filip <cernatescufilip at yahoo.com>
To: Norman Megill
Hi Norm!
I have created an Android App called XPuzzle. It is a puzzle with math
formulas derived from the Metamath system, it is a lightweight Metamath.
Problems and formulas are stored in a .mm file.
Formulas are axioms ($a) and they belong to public domain, problems ($p)
are theorems and they are registered to my name. I have attached the .mm
file to the email, and it is included in the .apk file. For now the other
properties of the formulas and problems are hard coded in the java program,
but it the future if the game has a public, these properties will be
written in a .mm file comment.
Xpuzzle has a web page: https://www.xpuzzle.co and at the bottom of that
page is a link to the Google Play Store, where the app can be found.
Please put this web page to the us.metamath.org. If my game has a public,
I will put ads on the app and I will donate a percent from the income to
the Metamath Foundation. Please also put an announcement to the Metamath
forum (I am unsubscribed).
Thank you very much!
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to metamath+unsubscr...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/0d4b3ac0-6ce6-4745-967a-bf6191eb3296n%40googlegroups.com.
$(
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
Axioms(a), constants(c) and variables(v,f) belong to the public domain
but the problems(p) and related data belong to Filip Cernatescu
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
$)
$c wff $. $( Well-formed formula symbol (read: "the following symbol
sequence is a wff") $)
$c |- $. $( Turnstile (read: "the following symbol sequence is provable" or
'a proof exists for") $)
$c class $.
$v ph $. $( Greek phi $)
$v ps $. $( Greek psi $)
$v ch $. $( Greek chi $)
$( Let variable ` ph ` be a wff. $)
wph $f wff ph $.
$( Let variable ` ps ` be a wff. $)
wps $f wff ps $.
$( Let variable ` ch ` be a wff. $)
wch $f wff ch $.
$( Declare the primitive constant symbols for propositional calculus. $)
$c ( $. $( Left parenthesis $)
$c ) $. $( Right parenthesis $)
$c -> $. $( Right arrow (read: "implies") $)
$c -. $. $( Right handle (read: "not") $)
$v A $.
$v B $.
$v C $.
$v D $.
$v M $.
$v N $.
$( Let ` A ` be a class variable. $)
cA $f class A $.
$( Let ` B ` be a class variable. $)
cB $f class B $.
$( Let ` C ` be a class variable. $)
cC $f class C $.
$( Let ` D ` be a class variable. $)
cD $f class D $.
$( Let ` M ` be a class variable. $)
cM $f class M $.
$( Let ` N ` be a class variable. $)
cN $f class N $.
$v X $.
$v Y $.
$v Z $.
$( Let ` X ` be a class variable. $)
cX $f class X $.
$( Let ` Y ` be a class variable. $)
cY $f class Y $.
$( Let ` Z ` be a class variable. $)
cZ $f class Z $.
$c x $.
$c y $.
$c z $.
$( Let ` x ` be a class constant,it is used as variable in equations. $)
c0x $a class x $.
$( Let ` y ` be a class constant,it is used as variable in equations. $)
c0y $a class y $.
$( Let ` z ` be a class constant,it is used as variable in equations. $)
c0z $a class z $.
$c = $. $( Equal sign (read: 'is equal to') $)
$( Declare the membership predicate symbol. $)
$c e. $. $( Stylized epsilon $)
wceq $a wff A = B $.
wcel $a wff A e. B $.
$( Declare new connectives. $)
$c =/= $. $( Not equal to (equal sign with slash through it). $)
$c e/ $. $( Not an element of (epsilon with slash through it). $)
$( Extend wff notation to include inequality. $)
wne $a wff A =/= B $.
$( Extend wff notation to include negated membership. $)
wnel $a wff A e/ B $.
$v R $.
$( Let ` R ` be a class variable. $)
cR $f class R $.
wbr $a wff A R B $.
wn $a wff -. ph $.
wi $a wff ( ph -> ps ) $.
$c <-> $. $( Double arrow (read: 'if and only if' or
'is logically equivalent to') $)
wb $a wff ( ph <-> ps ) $.
$( Declare connectives for disjunction ('or') and conjunction ('and'). $)
$c \/ $. $( Vee (read: 'or') $)
$c /\ $. $( Wedge (read: 'and') $)
$( Extend wff definition to include disjunction ('or'). $)
wo $a wff ( ph \/ ps ) $.
$( Extend wff definition to include conjunction ('and'). $)
wa $a wff ( ph /\ ps ) $.
$( Extend wff definition to include 3-way disjunction ('or'). $)
w3o $a wff ( ph \/ ps \/ ch ) $.
$( Extend wff definition to include 3-way conjunction ('and'). $)
w3a $a wff ( ph /\ ps /\ ch ) $.
$v F $.
$( Let ` F ` be a class variable. $)
cF $f class F $.
co $a class ( A F B ) $.
$c CC $. $( The set of complex numbers (blackboard bold C) $)
$c RR $. $( The set of real numbers (blackboard bold R) $)
$c NN0 $. $( The set of natural numbers $)
$c ZZ $. $( The set of integers (blackboard bold Z). $)
$c 0 $. $( The real number 0. $)
$c 1 $. $( The real number 1. $)
$c _i $. $( Letter i (the imaginary unit = square root of -1) $)
$c + $. $( Plus (addition) symbol $)
$c x. $. $( Multiplication symbol (center dot) $)
$c / $. $( Slash. $)
$c - $. $( Subtraction (binary minus). $)
$c -u $. $( Unary minus sign. $)
$( Class of complex numbers. $)
cc $a class CC $.
$( Class of real numbers. $)
cr $a class RR $.
$( Class of natural numbers. $)
cnn0 $a class NN0 $.
$( Extend class notation to include the class of integers. $)
cz $a class ZZ $.
$( Extend class notation to include the complex number 0. $)
cc0 $a class 0 $.
$( Extend class notation to include the complex number 1. $)
c1 $a class 1 $.
$( Extend class notation to include the complex number i. $)
ci $a class _i $.
$( Addition on complex numbers. $)
caddc $a class + $.
$( Multiplication on complex numbers. The token ` x. ` is a center dot. $)
cmul $a class x. $.
$( Extend class notation to include division. $)
cdiv $a class / $.
$( Extend class notation to include subtraction. $)
cmin $a class - $.
$( Extend class notation to include unary minus. The symbol ` -u ` is not a
class by itself but part of a compound class definition. We do this
rather than making it a formal function since it is so commonly used.
Note: We use different symbols for unary minus ( ` -u ` ) and subtraction
~ cmin ( ` - ` ) to prevent syntax ambiguity. For example, looking at the
syntax definition ~ co , if we used the same symbol
then " ` ( - A - B ) ` " could mean either " ` - A ` " minus " ` B ` ", or
it could represent the (meaningless) operation of
classes " ` - ` " and " ` - B ` " connected with "operation" " ` A ` ".
On the other hand, " ` ( -u A - B ) ` " is unambiguous. $)
cneg $a class -u A $.
$c ; $.
$( Constant used for decimal constructor. $)
cdc $a class ; A B $.
$c 2 $. $( The decimal number 2 $)
$c 3 $. $( The decimal number 3 $)
$c 4 $. $( The decimal number 4 $)
$c 5 $. $( The decimal number 5 $)
$c 6 $. $( The decimal number 6 $)
$c 7 $. $( The decimal number 7 $)
$c 8 $. $( The decimal number 8 $)
$c 9 $. $( The decimal number 9 $)
$c 10 $. $( The decimal number 10 $)
$( Extend class notation to include the number 2. $)
c2 $a class 2 $.
$( Extend class notation to include the number 3. $)
c3 $a class 3 $.
$( Extend class notation to include the number 4. $)
c4 $a class 4 $.
$( Extend class notation to include the number 5. $)
c5 $a class 5 $.
$( Extend class notation to include the number 6. $)
c6 $a class 6 $.
$( Extend class notation to include the number 7. $)
c7 $a class 7 $.
$( Extend class notation to include the number 8. $)
c8 $a class 8 $.
$( Extend class notation to include the number 9. $)
c9 $a class 9 $.
$( Extend class notation to include the number 10. $)
c10 $a class 10 $.
$c sqrt $. $( Positive square root of a positive real number. $)
$( Extend class notation to include square root of a real number. $)
csqrt $a class sqrt $.
$c ` $. $( Left apostrophe (function value symbol) $)
$( Extend the definition of a class to include the value of a function.
(Read: The value of ` F ` at ` A ` , or " ` F ` of ` A ` .") $)
cfv $a class ( F ` A ) $.
$c ^ $. $( Exponentiation. $)
$( Extend class notation to include exponentiation of a real number to an
integer power. $)
cexp $a class ^ $.
$c <_ $. $( Less or equal to. $)
cle $a class <_ $.
${
addcomi.1 $e |- A e. RR $.
addcomi.2 $e |- B e. RR $.
$( Addition commutes $)
addcomi $a |- ( A + B ) = ( B + A ) $.
$}
${
addassi.1 $e |- A e. RR $.
addassi.2 $e |- B e. RR $.
addassi.3 $e |- C e. RR $.
$( Associative law for addition 1 $)
addassi $a |- ( ( A + B ) + C ) = ( A + ( B + C ) ) $.
$( Associative law for addition 2 $)
addassi2 $a |- ( A + ( B + C ) ) = ( ( A + B ) + C ) $.
$( Associative-type law for addition and subtraction $)
addsubass $a |- ( A + ( B - C ) ) = ( ( A + B ) - C ) $.
$}
${
divdiri.1 $e |- A e. RR $.
divdiri.2 $e |- B e. RR $.
divdiri.3 $e |- C e. RR $.
divdiri.4 $e |- C =/= 0 $.
$( Distribution of division over addition 1 $)
divdiri1 $a |- ( ( A + B ) / C ) = ( ( A / C ) + ( B / C ) ) $.
$( Distribution of division over addition 2 $)
divdiri2 $a |- ( ( A / C ) + ( B / C ) ) = ( ( A + B ) / C ) $.
$}
${
divcan5i.1 $e |- A e. RR $.
divcan5i.2 $e |- B e. RR $.
divcan5i.3 $e |- C e. RR $.
divcan5i.4 $e |- C =/= 0 $.
divcan5i.5 $e |- B =/= 0 $.
$( Cancellation of common factor in a ratio $)
divcan5i1 $a |- ( ( C x. A ) / ( C x. B ) ) = ( A / B ) $.
$( Amplify a ratio by a factor $)
divcan5i2 $a |- ( A / B ) = ( ( C x. A ) / ( C x. B ) ) $.
$}
${
c1pro1 $p |- ( ( 1 / 2 ) + ( 2 / 3 ) ) = ( 7 / 6 ) $= $.
$}
${
c1pro2.1 $e |- x e. RR $.
c1pro2.2 $e |- y e. RR $.
c1pro2 $p |- ( ( 2 + y ) + ( x + 3 ) ) = ( ( x + y ) + 5 ) $= $.
$}
${
c1pro3.1 $e |- x e. RR $.
c1pro3.2 $e |- y e. RR $.
c1pro3.3 $e |- z e. RR $.
$( Prove a simple equality $)
c1pro3 $p |- ( ( z + y ) + x ) = ( ( x + y ) + z ) $= $.
$}
${
divcan3i.1 $e |- A e. RR $.
divcan3i.2 $e |- B e. RR $.
divcan3i.3 $e |- B =/= 0 $.
$( A cancellation law for division $)
divcan3i1 $a |- ( ( B x. A ) / B ) = A $.
$( Tranform a number into a ratio $)
divcan3i2 $a |- A = ( ( B x. A ) / B ) $.
$}
${
divmuldivi.1 $e |- A e. RR $.
divmuldivi.2 $e |- B e. RR $.
divmuldivi.3 $e |- C e. RR $.
divmuldivi.4 $e |- D e. RR $.
divmuldivi.5 $e |- C =/= 0 $.
divmuldivi.6 $e |- D =/= 0 $.
$( Multiplication of two ratios $)
divmuldivi $a |- ( ( A / C ) x. ( B / D ) ) = ( ( A x. B ) / ( C x. D ) )
$.
$}
${
divdivdivi.1 $e |- A e. RR $.
divdivdivi.2 $e |- B e. RR $.
divdivdivi.3 $e |- C e. RR $.
divdivdivi.4 $e |- C =/= 0 $.
divdivdivi.5 $e |- B =/= 0 $.
$( Division with a ratio $)
divdivdivi $a |- ( A / ( B / C ) ) = ( A x. ( C / B ) ) $.
$}
${
divsubdiri.1 $e |- A e. RR $.
divsubdiri.2 $e |- B e. RR $.
divsubdiri.3 $e |- C e. RR $.
divsubdiri.4 $e |- C =/= 0 $.
$( Distribution of division over subtraction 1 $)
divsubdiri1 $a |- ( ( A - B ) / C ) = ( ( A / C ) - ( B / C ) ) $.
$( Distribution of division over subtraction 2 $)
divsubdiri2 $a |- ( ( A / C ) - ( B / C ) ) = ( ( A - B ) / C ) $.
$}
${
mulcomi.1 $e |- A e. RR $.
mulcomi.2 $e |- B e. RR $.
$( Commutative law for multiplication $)
mulcomi $a |- ( A x. B ) = ( B x. A ) $.
$}
${
mulassi.1 $e |- A e. RR $.
mulassi.2 $e |- B e. RR $.
mulassi.3 $e |- C e. RR $.
$( Associative law for multiplication 1 $)
mulassi1 $a |- ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) $.
$( Associative law for multiplication 2 $)
mulassi2 $a |- ( A x. ( B x. C ) ) = ( ( A x. B ) x. C ) $.
$}
${
c1pro4 $p |- ( ( ( 1 / 3 ) + ( ( 1 / 3 ) / ( 1 - ( 1 / 3 ) ) ) ) / ( 3 / 2 )
) = ( 5 / 9 ) $= $.
$}
${
c1pro5 $p |- ( ( ( ( ( ; 2 1 / ; 1 0 ) + ( 1 / 2 ) ) / ( 6 / 5 ) ) + ( 6 /
5 ) ) - ( 4 / ; 1 0 ) ) = ( ; 8 9 / ; 3 0 ) $= $.
$}
${
c1pro6 $p |- ( ( ( ( 3 + ( 1 / 4 ) ) + ( 1 + ( 2 / 7 ) ) ) - ( 1 + ( ; 1 7 /
; 2 8 ) ) ) x. ( 1 + ( ; 1 5 / ; 4 1 ) ) ) = 4 $= $.
$}
${
sqrtmsq.1 $e |- A e. RR $.
sqrtmsq.2 $e |- 0 <_ A $.
$( Square root of square $)
sqrtmsq $a |- ( sqrt ` ( A x. A ) ) = A $.
$}
${
sqrtmul.1 $e |- A e. RR $.
sqrtmul.2 $e |- 0 <_ A $.
sqrtmul.3 $e |- B e. RR $.
sqrtmul.4 $e |- 0 <_ B $.
$( Square root distributes over multiplication $)
sqrtmul $a |- ( sqrt ` ( A x. B ) ) = ( ( sqrt ` A ) x. ( sqrt ` B ) ) $.
$}
${
sqval.1 $e |- A e. RR $.
$( Value of the square of a real number $)
sqval $a |- ( A x. A ) = ( A ^ 2 ) $.
$}
${
c2pro1 $p |- ( sqrt ` ( ; 1 6 + ( sqrt ` ; 8 1 ) ) ) = 5 $= $.
$}
${
subdir.1 $e |- A e. RR $.
subdir.2 $e |- B e. RR $.
subdir.3 $e |- C e. RR $.
$( Distribution of multiplication over subtraction $)
subdir $a |- ( ( A x. C ) - ( B x. C ) ) = ( ( A - B ) x. C ) $.
$( Distribution of multiplication over subtraction $)
subdir2 $a |- ( C x. ( A - B ) ) = ( ( C x. A ) - ( C x. B ) ) $.
$( Distribution of multiplication over subtraction $)
subdir3 $a |- ( ( A - B ) x. C ) = ( ( A x. C ) - ( B x. C ) ) $.
$( Distribution of multiplication over addition $)
adddir $a |- ( ( A x. C ) + ( B x. C ) ) = ( ( A + B ) x. C ) $.
$( Distribution of multiplication over addition $)
adddir2 $a |- ( C x. ( A + B ) ) = ( ( C x. A ) + ( C x. B ) ) $.
$}
${
c2pro2 $p |- ( ( ( ( 3 x. ( sqrt ` 5 ) ) - ( 4 x. ( sqrt ` 5 ) ) ) + ( 7 x.
( sqrt ` 5 ) ) ) - ( 3 x. ( sqrt ` 5 ) ) ) = ( 3 x. ( sqrt ` 5 ) ) $= $.
$}
${
c2pro3 $p |- ( ( ( ( sqrt ` ; 3 2 ) - ( sqrt ` ; 5 0 ) ) - ( sqrt `
; 9 8 ) ) + ( sqrt ` ; ; 2 4 2 ) ) = ( 3 x. ( sqrt ` 2 ) ) $= $.
$}
${
expadd.1 $e |- A e. RR $.
expadd.2 $e |- M e. NN0 $.
expadd.3 $e |- N e. NN0 $.
$( Sum of exponents law $)
expadd $a |- ( ( A ^ M ) x. ( A ^ N ) ) = ( A ^ ( M + N ) ) $.
$( Exponent subtraction law $)
expsubd $a |- ( ( A ^ M ) / ( A ^ N ) ) = ( A ^ ( M - N ) ) $.
$( Product of exponents law $)
expmuld $a |- ( ( A ^ M ) ^ N ) = ( A ^ ( M x. N ) ) $.
$}
$( Number decomposition $)
9e3pw2 $a |- 9 = ( 3 ^ 2 ) $.
$( Number decomposition $)
27e3pw3 $a |- ; 2 7 = ( 3 ^ 3 ) $.
${
c3pro1 $p |- ( ( ( 5 ^ 3 ) x. ( 5 ^ 5 ) ) / ( 5 ^ 6 ) ) = ( 5 ^ 2 )
$= $.
$}
${
c3pro2 $p |- ( ( ( 2 ^ 5 ) ^ 3 ) x. ( ( 2 ^ 4 ) ^ 3 ) ) = ( 2 ^ ; 2 7 )
$= $.
$}
${
c3pro3 $p |- ( ( ( 9 ^ 5 ) ^ 3 ) x. ( ( ; 2 7 ^ 2 ) ^ 4 ) ) = ( 3 ^ ; 5
4 ) $= $.
$}
${
c4pro5.1 $e |- ( ( 3 x. x ) + ( 6 - 2 ) ) = ; 1 6 $.
c4pro5.2 $e |- x e. RR $.
$( Solve for x the equation $)
c4pro5 $p |- x = 4 $= $.
$}
${
subadd.1 $e |- A e. RR $.
subadd.2 $e |- B e. RR $.
subadd.3 $e |- C e. RR $.
$( Relationship between subtraction and addition $)
subadd1 $a |- ( ( A - B ) = C <-> A = ( C + B ) ) $.
$( Relationship between subtraction and addition $)
subadd1b $a |- ( ( A + B ) = C <-> A = ( C - B ) ) $.
$( Relationship between subtraction and addition $)
subadd2 $a |- ( C = ( A + B ) <-> ( C - A ) = B ) $.
$( Relationship between subtraction and addition $)
subadd2b $a |- ( C = ( A - B ) <-> ( C - A ) = -u B ) $.
$( Cancellation of a number on both sides of the equality $)
subadd3 $a |- ( ( A + B ) = ( A + C ) <-> B = C ) $.
$}
${
divmul.1 $e |- A e. RR $.
divmul.2 $e |- B e. RR $.
divmul.3 $e |- C e. RR $.
divmul.4 $e |- C =/= 0 $.
$( Relationship between division and multiplication $)
divmul $a |- ( ( C x. B ) = A <-> B = ( A / C ) ) $.
$}
${
c4pro1.1 $e |- ( ( 7 x. x ) + ( 3 x. ( ( 2 x. x ) - 1 ) ) ) = ( ( ; 1
0 x. x ) + 9 ) $.
c4pro1.2 $e |- x e. RR $.
$( Solve for x the equation $)
c4pro1 $p |- x = 4 $= $.
$}
${
divmuleq.1 $e |- A e. RR $.
divmuleq.2 $e |- B e. RR $.
divmuleq.3 $e |- C e. RR $.
divmuleq.4 $e |- D e. RR $.
divmuleq.5 $e |- C =/= 0 $.
divmuleq.6 $e |- D =/= 0 $.
$( Cross-multiply in an equality of ratios $)
divmuleq $a |- ( ( A / C ) = ( B / D ) <-> ( A x. D ) = ( C x. B ) ) $.
$}
${
div2neg.1 $e |- A e. RR $.
div2neg.2 $e |- B e. RR $.
div2neg.3 $e |- B =/= 0 $.
$( Quotient of two negatives $)
div2neg $a |- ( -u A / -u B ) = ( A / B ) $.
$}
${
c4pro2.1 $e |- ( ( ( 7 x. x ) / 6 ) - ( 3 + ( 1 / 3 ) ) ) = ( ( ( 7 x. x
) + ; 1 6 ) / ; 1 5 ) $.
c4pro2.2 $e |- x e. RR $.
$( Solve for x the equation $)
c4pro2 $p |- x = ( ; ; 3 9 6 / ; 6 3 ) $= $.
$}
${
binom2subi.1 $e |- A e. CC $.
binom2subi.2 $e |- B e. CC $.
$( Expand the square of a subtraction $)
binom2subi $a |- ( ( A - B ) ^ 2 ) = ( ( ( A ^ 2 ) - ( 2 x. ( A x. B ) ) )
+ ( B ^ 2 ) ) $.
$}
$( 1 to the power of 2 $)
1pw2e1 $a |- ( 1 ^ 2 ) = 1 $.
$( 2 to the power of 2 $)
2pw2e4 $a |- ( 2 ^ 2 ) = 4 $.
${
mulexpz.1 $e |- A e. RR $.
mulexpz.2 $e |- A =/= 0 $.
mulexpz.3 $e |- B e. RR $.
mulexpz.4 $e |- B =/= 0 $.
mulexpz.4 $e |- N e. ZZ $.
$( Integer exponentiation of a product $)
mulexpz $a |- ( ( A x. B ) ^ N ) = ( ( A ^ N ) x. ( B ^ N ) ) $.
$}
${
negsubi.1 $e |- A e. RR $.
negsubi.2 $e |- B e. RR $.
$( Relationship between subtraction and negative $)
negsubi $a |- ( A - B ) = ( A + -u B ) $.
$( Negative of product $)
mulneg1i $a |- -u ( A x. B ) = ( -u A x. B ) $.
$( Relationship between subtraction and negative $)
subnegi $a |- ( A - -u B ) = ( A + B ) $.
$}
${
c4pro3.1 $e |- ( ( ( 1 - ( 2 x. x ) ) ^ 2 ) - 6 ) = ( ( ( 4 x. x ) x. ( x
- 2 ) ) + 3 ) $.
c4pro3.2 $e |- x e. RR $.
$( Solve for x the equation $)
c4pro3 $p |- x = 2 $= $.
$}
$( Number decomposition $)
72e6m6m2 $a |- ; 7 2 = ( ( 6 x. 6 ) x. 2 ) $.
$( Number decomposition $)
50e5m5m2 $a |- ; 5 0 = ( ( 5 x. 5 ) x. 2 ) $.
${
c4pro4.1 $e |- ( ( ( sqrt ` 2 ) x. ( x - 4 ) ) - ( sqrt ` ; 7 2 ) ) = (
sqrt ` ; 5 0 ) $.
c4pro4.2 $e |- x e. RR $.
$( Solve for x the equation $)
c4pro4 $p |- x = ; 1 5 $= $.
$}
