Single mathematics that was written in THEAX language is called text. Text starts with a line of
and finishes with a line of
Here, line means letter lines that are sectioned by semicolons (;). <text name> can be chosen from optional names(within 35 letters). Text is constructed by repeating parts of <text block> and that <text block> is either a <axiom block> or a <definition block>. This corresponds to the fact that mathematics is compounded by the repetition of the axiom, theorem, or definition.
(The following part, "Referred" function, has not been achieved in the first version of the checker >>>)
Text fundamentally concludes itself; however, in some cases, it wants to quote the axiom, theory, or definition of other texts. In this case, we insert this special block after the text (in front of other blocks). For instance, when there is a text like figure A, if figure B's text had citation blocks, figure B is considered to be the same kind of text as figure C. Therefore, there is a function that rewrites labels and names according to the direction within the citation blocks. This is helpful to avoid the confusion of symbols when some of the texts get connected. However, this function will be used only after a proper organization is made in the future, registers publicly advertised texts, and opens to the public so that anyone will be able to cite. We hope that in the future, many theories will be stored in the computer and be data based.
Further, real texts are written after putting apostrophes and numbers of every 10 numbers for each line like figures A, B, and C. Many basic texts for personal computers arbitrate this as an annotation line; because of this, we can write optional letter lines and it is useful to utilize personal computers for making THEAX texts.
00040' A:(All x)(All y)(All z)(Smaller (x,y)and
00050' Smaller(y,z)imp Smaller(x,z));
00070' C: Smaller(Cricket,Grasshopper);
Figure A TEXT Grasshopper
00020' (L:A to D,Ant to Mars,Cricket to Evening-Glow,
00030 Grasshopper to Wind,Smaller to Higher);
00050'Lemma; A: Higher(Mars,Wind);
00060'Proof; a1:Higher(Mars,Evening-Glow)and Higher(
00070' Evening-Glow,Wind)imp Higher(Mars,Wind) by ALS(D);
00080' a2:Higher(Mars,Wind) by LOGIC(a1,B,C);
Figure B Text that cited Grasshopper, Mars
00040' D:(All x)(All y)(All z)(Higher(x,y)and
00050' Higher(y,z)imp Higher(x,z));
00060' B: Higher(Mars,Evening-Glow);
00070' C: Higher(Evening-Glow,Wind);
00100'Proof; a1:Higher(Mars,Evening-Glow)and Higher(
00110' Evening-Glow,Wind)imp Higher(Mars,Wind) by ALS(D);
00120' a2:Higher(Mars,Wind) by LOGIC(a1,B,C);
Figure C Figure B's text can be rewritten like this in a text.