MathCheck Brief Instructions
This document is as of 20211116.
It lacks all more recent features of MathCheck.
In readymade problems, the use of commands may have been
restricted to those relevant for the problem.
Arithmetic and Parentheses
`54321`  54321 
`frac(54)(321)`  54/321 
`54 frac(3)(21)`  54 3/21 
`54.321`  54.321 
`pi`  pi 
`e`  e 

`+`  + 
`−`   
`*`  * 
`x/y`  x/y 
`frac(x+1)(2y)`  (x+1)/(2y) 
`x^y`  x^y 
`x^(y z)`  x^(y z) 

`(`  ( 
`)`  ) 
`(`  #( 
`)`  #) 
`[`  [ 
`]`  ] 
`\ text(div)\ `  div 
`mod`  mod 
`n!`  n! 

`sqrt x+1`  sqrt x+1 
`sqrt(x+1)`  sqrt(x+1) 
`root(n)(x+1)`  root(n)(x+1) 
`x+1`  x+1 abs(x+1) 
`__x+1__`  _x+1_ floor(x+1) 
`~x+1~`  ^x+1^ ceil(x+1) 
`d/(d x) sin 5x`  DD x sin 5x 

`sin`  sin 
`cos`  cos 
`tan`  tan 
`cot`  cot 
`ln`  ln 
`log`  log 
`log_2`  log2 
`sinh`  sinh 
`cosh`  cosh 
`tanh`  tanh 

The input symbols ( and ) denote
ordinary parentheses and #( and #) denote hard
parentheses.
MathCheck removes unnecessary ordinary parentheses, but always prints hard
parentheses even if they are unnecessary.
Comparisons and Logic
`<=`  <= 
`<`  < 
`=`  = 
`!=`  != 
`>=`  >= 
`>`  > 

`not`  ! not 
`^^`  /\ and ^^ 
`vv`  \/ or vv 
`rarr`  > 
`harr`  <> 
`sf"F"`  FF 
`sf"U"`  UU 
`sf"T"`  TT 

`\ sf"&&"\ `  && 
`\ sf""\ `   
`AA x:`  AA x: 
`AA i; 1 <= i <= n:`  AA i; 1 <= i <= n: 
`EE x:`  EE x: 
`EE i; 1 <= i <= n:`  EE i; 1 <= i <= n: 

`rArr`  ==> 
`lArr`  <== 
`hArr`  <=> 
`=`  === 

Reasoning Chains
A reasoning chain may contain ⇐, ⇔, ⇒ and ≡, and the following:
assume x != 1 /\ y >= x;  Set a condition
that is assumed to hold throughout the (sub)proof. One may use enda
instead of ;. 
original  Refers to the first formula in a
reasoning chain. If original is the first formula of a subproof,
then it refers to the first formula of the parent proof. 
subend  Ends a subproof. 
subproof  Starts a subproof. 
What formulas in a reasoning chain may contain depends on the problem mode.
Typically most logical and comparison operators are allowed, but only a small
set of arithmetic operators.
Greek Letters
`alpha`  al 
`beta`  be 
`gamma`  ga 
`delta`  de 
`varepsilon`  ve 
`epsilon`  ep 
`zeta`  ze 

`eta`  et 
`theta`  th 
`vartheta`  vt 
`iota`  io 
`kappa`  ka 
`lambda`  la 
`mu`  mu 

`nu`  nu 
`xi`  xi 
`rho`  rh 
`sigma`  si 
`tau`  ta 
`upsilon`  up 

`phi`  ph 
`varphi`  vp 
`chi`  ch 
`psi`  ps 
`omega`  om 

`Gamma`  Ga GA 
`Delta`  De DE 
`Theta`  Th TH 
`Lambda`  La LA 
`Xi`  Xi XI 

`Pi`  Pi PI 
`Sigma`  Si SI 
`Phi`  Ph PH 
`Psi`  Ps PS 
`Omega`  Om OM 

Lexical Rules
Spaces and newlines may be freely used between tokens.
If a nonnumeric token ends and the next one starts with a letter or digit,
there must be at least one space or newline in between.
These symbols can also be given as Unicode characters:
¬ ² ³ Γ Δ Θ Λ Ξ Π Σ Φ Ψ Ω α β γ δ ε ζ η θ ι κ λ μ ν ξ π ρ σ τ υ φ χ ψ ω ϑ ϕ ϵ
← → ↔ ↠ ⇐ ⇒ ⇔ ∀ ∃ − √ ∧ ∨ ≠ ≡ ≤ ≥ ⋅ ⌈ ⌉ ⌊ ⌋
Special Commands
/**/  Start a new line. A new line may also
be started by putting the ⇔, ⇒, etc., to the very beginning of the line. In
problem modes that do not support them, put =, >, etc., to the very
beginning of the line. 
/* two to the `n` is `2^n` */  Write a
comment and start a new line. Passages surrounded by grave accent characters
will be shown as mathematics. 
assume x != 1 /\ y^2 < sin x;  Restrict
the range of variables. Any comparisons and propositional operators may be used
in the condition. One may use enda instead of ;. Works in
the arithmetic and draw function modes, and almost all problem modes that
support logical reasoning chains. Unless otherwise stated, this must be next to
the problem mode keyword. 