(*header{*Header Chapter Title Test*}*)
(*section{*The Axiom of Extension*}*)
(*--"\<^bold>I\<^bold>S\<^bold>A\<^bold>R \<^bold>(Theory name, imports, and begin.\<^bold>)"*)
theory sTs01
imports Complex_Main "i"
begin
--"\<^bold>[\<^bold>\<Theta>\<^bold>]"

subsection{*Test of inline, equation, multline, eqnarray, label, ref, cite*}

--"\<^isub>'I start off with the bibliography citations \<langle>\<^isub>`seGol.59\<^isub>`\<rangle> and \<langle>\<^isub>`seJec, loBil\<^isub>`\<rangle>.

Next is an index \<^isub>\<stileturn>entry\<^isub>\<turnstile> on the word \<hungarumlaut>entry\<hungarumlaut>, and an index entry where
\<hungarumlaut>\<^isub>\<stileturn>markup\<langle>!entry\<rangle>\<^isub>\<turnstile>\<hungarumlaut> is sub-indexed by using the option \<^isub>*!entry\<^isub>* in the \<^isub>*\<setminus>index\<^isub>*
command.

Footnotes? What I really want to say can only be said below. \<langle>\<^isub>*Some people could
be annoyed by all of this.\<^isub>*\<rangle>

I now go on to those very important inline equations and equation environments, 
so please consider the difficulty of the inline equation \<^isub>`x\<^isup>1+\<lfloor>1.2\<rfloor>=1\<^isub>`, and now 
the equation

       \<^isub>\<lhd>\<forall>q\<^isub>1.\<forall>q\<^isub>2.(\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>1 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>2) \<longleftrightarrow> (q\<^isub>1 = q\<^isub>2),\<^isub>\<rhd>                \<langle>aaaa60a\<rangle>

along with the very ugly \<^isub>*multline\<^isub>* environment,

      .\<^isub>\<lhd>(\<forall>q\<^isub>1.\<forall>q\<^isub>2.(\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>1 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>2) \<longleftrightarrow> (q\<^isub>1 = q\<^isub>2)) \<longleftrightarrow>
                                                    P x \<longleftrightarrow>
                 ((\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>3 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>4) \<longleftrightarrow> (q\<^isub>3 = q\<^isub>4)),\<^isub>\<rhd>.            \<langle>aaaa60b\<rangle>

at least when I stick that middle line in there.

The \<^isub>*eqnarray\<^isub>* environment with 3 columns specified by \<^isub>*[rcl]\<^isub>* is frequently used:

      \<^isub>\<lless>a \<^isub>\<lozenge>=\<^isub>\<lozenge> b
          \<^isub>\<lozenge>=\<^isub>\<lozenge> c
          \<^isub>\<lozenge>=\<^isub>\<lozenge> d.\<^isub>\<ggreater>

Having to tweak LaTeX raises its ugly head, so I replace Equation \<langle>aaaa60b\<rangle> with
a two column \<^isub>*eqnarray\<^isub>*, and change the default column alignment from \<^isub>*[rcl]\<^isub>* to
\<^isub>*[rl]\<^isub>*. I do that with my equation array environment prefix \<^isub>*\<langle>rl\<rangle>\<^isub>*. The \<^isub>*\<langle>rl\<rangle>\<^isub>* is
a prefix instead of a suffix, because the suffix position is taken up by the
optional reference label.

\<langle>rl\<rangle>   \<^isub>\<lless>(\<forall>q\<^isub>1.\<forall>q\<^isub>2.(\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>1 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>2) \<longleftrightarrow> (q\<^isub>1 = q\<^isub>2))\<^isub>\<lozenge>\<longleftrightarrow>
                                                    P x \<^isub>\<lozenge>\<longleftrightarrow>
                 ((\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>3 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>4) \<longleftrightarrow> (q\<^isub>3 = q\<^isub>4))\<^isub>\<lozenge>.\<^isub>\<ggreater>

I could have used the three column default, and left one column empty, but this
is for demonstration.

Here, I ask the question, \<hungarumlaut>Are what I've been calling equations really equations?\<hungarumlaut>
If we consider that the HOL \<longleftrightarrow> operator is merely notation for \<^isub>`=\<^isub>`, then I 
suppose they are equations, but as a matter of style, I would rather use 
\<hungarumlaut>Formula\<hungarumlaut>, and I have set it up to where \<hungarumlaut>Formula\<hungarumlaut> is a synonym for \<hungarumlaut>Equation\<hungarumlaut> 
when used with \<^isub>*\<setminus>label\<^isub>* and \<^isub>*\<setminus>eqref\<^isub>*.

After experimenting, I decided I can get rid of the \<^isub>*multline\<^isub>* environment.
The environment \<^isub>*eqnarray\<^isub>*, from the \<^isub>*mathenv\<^isub>* package, replaces the standard
\<^isub>*eqnarray\<^isub>* and it is a very versatile equation environment which can be used in
place of many other environments.

Here's the \<^isub>*multline\<^isub>* environment:

      .\<^isub>\<lhd>(\<forall>q\<^isub>1.\<forall>q\<^isub>2.(\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>1 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>2) \<longleftrightarrow> (q\<^isub>1 = q\<^isub>2)) \<longleftrightarrow>
                 ((\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>3 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>4) \<longleftrightarrow> (q\<^isub>3 = q\<^isub>4)).\<^isub>\<rhd>.             \<langle>lkr23j\<rangle>

And here's the same equation using the \<^isub>*eqnarray\<^isub>* environment, set for one right
justified column:
      \<langle>r\<rangle>
      \<^isub>\<lhd>(\<forall>q\<^isub>1.\<forall>q\<^isub>2.(\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>1 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>2) \<longleftrightarrow> (q\<^isub>1 = q\<^isub>2)) \<longleftrightarrow>
                 ((\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>3 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>4) \<longleftrightarrow> (q\<^isub>3 = q\<^isub>4)).\<^isub>\<rhd>              \<langle>lkr23k\<rangle>

Personally, I think Formula \<langle>lkr23k\<rangle> is formatted better than Formula \<langle>lkr23j\<rangle>.
And there are others ways to format Formula \<langle>lkr23j\<rangle> with \<^isub>*eqnarray\<^isub>*, like

      \<^isub>\<lless>(\<forall>q\<^isub>1.\<forall>q\<^isub>2.(\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>1 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>2)\<^isub>\<lozenge>\<longleftrightarrow>\<^isub>\<lozenge>(q\<^isub>1 = q\<^isub>2)) \<longleftrightarrow>
               ((\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>3 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>4)\<^isub>\<lozenge>\<longleftrightarrow>\<^isub>\<lozenge>(q\<^isub>3 = q\<^isub>4)),\<^isub>\<ggreater>

or
      \<^isub>\<lless>(\<forall>q\<^isub>1.\<forall>q\<^isub>2.(\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>1 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>2) \<longleftrightarrow> (q\<^isub>1 = q\<^isub>2))\<^isub>\<lozenge>\<longleftrightarrow>\<^isub>\<lozenge>
                              ((\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>3 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>4)\<^isub>\<lozenge>\<longleftrightarrow>\<^isub>\<lozenge>(q\<^isub>3 = q\<^isub>4)),\<^isub>\<ggreater>

This is why LaTeX can be a bad thing. I can spend way too much time tweaking
the formatting of equations."

subsection{*The primitive set type and membership predicate*}

--"\<^isub>'ZF sets is a first-order language which requires an infinite set of
variables, and it generally goes unsaid in the formalization of a first-order
language that the variables provided are of a single type.

However, in HOL there are a multitude of variable types, and additionally, we
are allowed to define a new type of variable so we can have a new variable type
that exists in its own domain.

For ZF sets, I define the primitive variable type \<^isub>*sT\<^isub>*, where the non-ASCII
notation for \<^isub>*sT\<^isub>* is \<sigma>\<^isub>\<iota>. The subscripted character for \<sigma>\<^isub>\<iota> is the Greek letter
iota."

--"\<^bold>T\<^bold>Y\<^bold>P\<^bold>E \<^bold>(The primitive set type \<^isub>*sT\<^isub>*: everything is a set.\<^bold>)"
typedecl sT ("\<sigma>\<^isub>\<iota>")
--"\<^bold>[\<^bold>\<Theta>\<^bold>]"

--"\<^isub>'ZF sets is specified to have one predicate, which is membership. The
ASCII and non-ASCII notation for membership are \<^isub>*inS\<^isub>* and \<in>\<^isub>\<iota>, along with
negation of membership, which is notated by \<^isub>*niS\<^isub>* and \<notin>\<^isub>\<iota>."

--"\<^bold>O\<^bold>P\<^bold>E\<^bold>R\<^bold>A\<^bold>T\<^bold>O\<^bold>R \<^bold>(Membership predicate \<^isub>*inS\<^isub>*: axiomatized by subsequent axioms.\<^bold>)"
consts inS :: "\<sigma>\<^isub>\<iota> \<Rightarrow> \<sigma>\<^isub>\<iota> \<Rightarrow> bool" (infixl "inS" 55)
  notation
    inS                         (infixl "\<in>\<^isub>\<iota>"  55)
  abbreviation
    niS :: "\<sigma>\<^isub>\<iota> \<Rightarrow> \<sigma>\<^isub>\<iota> \<Rightarrow> bool"    (infixl "niS" 55) where "x niS y == \<not>(x \<in>\<^isub>\<iota> y)"
  notation
    niS                         (infixl "\<notin>\<^isub>\<iota>"  55)
--"\<^bold>[\<^bold>\<Theta>\<^bold>]"

subsection{*Axiomatizing the two forms of the Axiom of Extension*}

--"\<^isub>'The standard Axiom of Extension is the formula

      \<^isub>\<lhd>\<forall>q\<^isub>1.\<forall>q\<^isub>2.(\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>1 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>2) \<longleftrightarrow> (q\<^isub>1 = q\<^isub>2).\<^isub>\<rhd>

The question is whether in Isabelle/HOL, this standard formula is equivalent to
the free variable form

      \<^isub>\<lhd>(\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>1 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>2) \<longleftrightarrow> (q\<^isub>1 = q\<^isub>2),\<^isub>\<rhd>

where \<^isub>`q\<^isub>1\<^isub>` and \<^isub>`q\<^isub>2\<^isub>`, because they are not in the scope of any quantifier, are
free variables.

Naively, the following counterexample seems to indicate that they are not
equivalent."

--"\<^bold>C\<^bold>O\<^bold>U\<^bold>N\<^bold>T\<^bold>E\<^bold>R\<^bold>X \<^bold>(A counterexample is found for the naive equivalence.\<^bold>)"
theorem
  "(\<forall>q\<^isub>1.\<forall>q\<^isub>2.(\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>1 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>2) \<longleftrightarrow> (q\<^isub>1 = q\<^isub>2)) \<longleftrightarrow>
              ((\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>3 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>4) \<longleftrightarrow> (q\<^isub>3 = q\<^isub>4))"
--"nitpick[sat_solver=SAT4J,timeout=60,verbose,user_axioms]"
--"Nitpick found a counterexample for card \<sigma>\<^isub>\<iota> = 2:
   Free variables: (q\<^isub>3\<Colon>\<sigma>\<^isub>\<iota>) = s1
                   (q\<^isub>4\<Colon>\<sigma>\<^isub>\<iota>) = s2"
  oops
--"\<^bold>[\<^bold>\<Theta>\<^bold>]"

--"\<^isub>'The problem is that the prover engine implicitly quantifies all free
variables in the statement of a theorem, so the formula in the above
counterexample is not the equivalence that we need to prove or disprove.

This quantification is done at the outermost level with universal quantifiers.
For example, the formula

     \<^isub>\<lless>(\<forall>q\<^isub>1.\<forall>q\<^isub>2.\<^isub>\<lozenge>\<^isub>\<lozenge>(\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>1 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>2) \<longleftrightarrow> (q\<^isub>1 = q\<^isub>2))
             \<longleftrightarrow>\<^isub>\<lozenge>\<^isub>\<lozenge>((\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>3 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>4) \<longleftrightarrow> (q\<^isub>3 = q\<^isub>4))\<^isub>\<ggreater>

can be considered to be equivalent to the quantified formula

     \<^isub>\<lless>\<forall>q\<^isub>3.\<forall>q\<^isub>4.(\<forall>q\<^isub>1.\<forall>q\<^isub>2.\<^isub>\<lozenge>\<^isub>\<lozenge>(\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>1 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>2) \<longleftrightarrow> (q\<^isub>1 = q\<^isub>2))
                     \<longleftrightarrow>\<^isub>\<lozenge>\<^isub>\<lozenge>((\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>3 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>4) \<longleftrightarrow>(q\<^isub>3 = q\<^isub>4)).\<^isub>\<ggreater>

I say \<hungarumlaut>considered\<hungarumlaut> because the quantification is actually being done at the
meta-logic level. To see that free variables are quantified by the meta-logic
quantifier \<And>, we can look at the output of \<^isub>*thm\<^isub>* in the following example."

--"\<^bold>E\<^bold>X\<^bold>A\<^bold>M\<^bold>P\<^bold>L\<^bold>E \<^bold>(Free variables are quantified at the meta-logic level.\<^bold>)\<langle>lkzv08a\<rangle>"
theorem
  free\<^isub>'variable\<^isub>'conjecture:
  "(\<forall>x\<Colon>'a. P x) \<longleftrightarrow> (P x)"
  sorry

theorem
  And\<^isub>'quantified\<^isub>'conjecture:
  "\<And>x.(\<forall>x\<Colon>'a. P x) \<longleftrightarrow> (P x)"
  sorry

thm
  free\<^isub>'variable\<^isub>'conjecture
  And\<^isub>'quantified\<^isub>'conjecture

--"thm output for both: (\<forall>(x\<Colon>?'a). ?P\<Colon>(?'a \<Rightarrow> bool) x) = (?P (?x\<Colon>?'a))."

theorem
  forall\<^isub>'quantified\<^isub>'conjecture:
  "\<forall>x.(\<forall>x\<Colon>'a. P x) \<longleftrightarrow> (P x)"
  sorry

thm
  forall\<^isub>'quantified\<^isub>'conjecture

--"thm output: \<forall>(x\<Colon>?'a). (\<forall>(x\<Colon>?'a). ?P\<Colon>(?'a \<Rightarrow> bool) x) = (?P x)."
--"\<^bold>[\<^bold>\<Theta>\<^bold>]"

--"\<^isub>'If we were to prove the first two conjectures in the above example, then the
resulting theorems would be the same, as shown by the output of \<^isub>*thm\<^isub>*. (Example
\<langle>lkzv08a\<rangle> also shows how free variables and \<And> quantified variables are tied
together by means of schematic variables.)

As shown by Example \<langle>lkzv08a\<rangle>, free variables are quantified by \<And>, and so I use
the fact that because free variable Formula \<langle>lkzv39a\<rangle>, shown here,

      \<^isub>\<lhd>(\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>1 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>2) \<longleftrightarrow> (q\<^isub>1 = q\<^isub>2),\<^isub>\<rhd>                         \<langle>lkzv39a\<rangle>

is equivalent to Formula \<langle>lkzv39b\<rangle>,

      \<^isub>\<lhd>\<And>q\<^isub>1.\<And>q\<^isub>2.(\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>1 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>2) \<longleftrightarrow> (q\<^isub>1 = q\<^isub>2),\<^isub>\<rhd>                \<langle>lkzv39b\<rangle>

then it is equivalent to this fully quantified Formula \<langle>lkzv39c\<rangle>,

      \<^isub>\<lhd>\<forall>q\<^isub>1.\<forall>q\<^isub>2.(\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>1 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>2) \<longleftrightarrow> (q\<^isub>1 = q\<^isub>2).\<^isub>\<rhd>                 \<langle>lkzv39c\<rangle>

This is the desired equivalence, that is, that the standard form of the Axiom of 
Extension is equivalent to the free variable form.

To prove this, because \<And> is a meta-logic operator, we must resort to meta-logic,
which I now do in the proof of Theorem \<langle>lkBh38a\<rangle>."

--"\<^bold>T\<^bold>H\<^bold>E\<^bold>O\<^bold>R\<^bold>E\<^bold>M \<^bold>(Standard and free variable Axiom of Extension equivalence.\<^bold>)\<langle>lkBh38a\<rangle>"
theorem extension\<^isub>'equivalence:
  "(Trueprop (\<forall>q\<^isub>1.\<forall>q\<^isub>2.(\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>1 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>2) \<longleftrightarrow> (q\<^isub>1 = q\<^isub>2))) \<equiv>
           (\<And>q\<^isub>3.\<And>q\<^isub>4.((\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>3 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>4) \<longleftrightarrow> (q\<^isub>3 = q\<^isub>4)))"
--"\<^bold>[\<^bold>\<Theta>\<^bold>]"

--"\<^bold>P\<^bold>R\<^bold>O\<^bold>O\<^bold>F\<langle>lkBg41a\<rangle>"
proof
  assume "\<forall>q\<^isub>1.\<forall>q\<^isub>2.(\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>1 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>2) \<longleftrightarrow> (q\<^isub>1 = q\<^isub>2)"
  then show "\<And>q\<^isub>3.\<And>q\<^isub>4.(\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>3 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>4) \<longleftrightarrow> (q\<^isub>3 = q\<^isub>4)"
  by simp
next
  assume "\<And>q\<^isub>3.\<And>q\<^isub>4.((\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>3 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>4) \<longleftrightarrow> (q\<^isub>3 = q\<^isub>4))"
  then show "\<forall>q\<^isub>1.\<forall>q\<^isub>2.(\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>1 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>2) \<longleftrightarrow> (q\<^isub>1 = q\<^isub>2)"
  by simp
qed
--"\<^bold>[\<^bold>\<Pi>\<^bold>]"

--"\<^isub>'The use of \<^isub>*simp\<^isub>* in Proof \<langle>lkBg41a\<rangle> \<langle>\<^isub>`pipSte121029\<^isub>`\<rangle> shows that the 
proof of Theorem \<langle>lkBh38a\<rangle> is trivial, which is not surprising, since we would 
expect meta-logic \<And> and the HOL operator \<forall> to both produce the same result. 
But though the proof is trivial, the theorem is not unimportant, since Formula
\<langle>lkzv39a\<rangle> will be stated as an axiom, and when it comes to extending HOL with 
axioms, due diligence should be exercised, although what is \<hungarumlaut>due diligence\<hungarumlaut> to 
one may be \<hungarumlaut>belaboring the point\<hungarumlaut> to another.

Of note is that Theorem \<langle>lkBh38a\<rangle> has been resorted to out of necessity, and 
it is tempting to also want to formally prove that Formula \<langle>lkzv39a\<rangle> is equivalent 
to Formula \<langle>lkzv39b\<rangle>, but we would end up in the same situation, that because 
there are free variables in Formula \<langle>lkzv39a\<rangle>, those variables would get 
quantified by \<And> if we tried to state, in a single formula, that Formula \<langle>lkzv39a\<rangle> 
and Formula \<langle>lkzv39b\<rangle> are equivalent. (In a single Isar hypothesis, there may be 
a way to state that two formulas are equivalent without using \<equiv>, \<longleftrightarrow>, or \<^isub>`=\<^isub>`, 
but if there is, I am not aware of it.)

Now, because it has been shown that the two forms of the Axiom of Extension
are equivalent, then we can axiomatize either form and get the other. However,
rather than just axiomatize one of the formulas, I axiomatize both. The \<^isub>*Nu\<^isub>*
form of \<^isub>*Ax\<^isub>'x\<^isub>* axiom will be used, whenever possible, for theorems with no free
variables. The \<^isub>*Nf\<^isub>* form will be used for theorems which contain free variables.
This allows the possibility of separating the axioms and theorems with free
variables from the axioms and theorems which contain no free variables."

--"\<^bold>A\<^bold>X\<^bold>I\<^bold>O\<^bold>M \<^bold>(The Axiom of Extension: set equality.\<^bold>)\<langle>lkBh07a\<rangle>"
axiomatization where
  Ax\<^isub>'x\<^isup>N\<^isup>u: "\<forall>q\<^isub>1.\<forall>q\<^isub>2.(\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>1 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>2) \<longleftrightarrow> (q\<^isub>1 = q\<^isub>2)" and
  Ax\<^isub>'x\<^isup>N\<^isup>f: "        (\<forall>x. x \<in>\<^isub>\<iota> q\<^isub>1 \<longleftrightarrow> x \<in>\<^isub>\<iota> q\<^isub>2) \<longleftrightarrow> (q\<^isub>1 = q\<^isub>2)"
--"\<^bold>[\<^bold>\<Theta>\<^bold>]"

section{*Rough LaTeX markup notes and documentation*}

--"\<^isub>'My rough notes and documentation on how I'm marking things up. They're 
commented out and don't show up in the PDF. 

There's no fool proof method behind my selection of what character to use to 
create a markup delimiter. I think a little, and then I start using a character 
until I think of something better or find out why a certain character is not 
going to work."

subsection{* Guidelines *}
(*
GUIDELINES FOR CHOOSING SUBSCRIPTED CHARACTERS FOR CREATING MARKUP DELIMITERS
0) With four characters and one type of delimiter, such as \<guillemotleft>...\<guillemotright>, by using the
   characters subscripted either on the inside or outside, you can create 8 different 
   delimiters.
1) Don't use subscripting or super scripting on two different characters that
   will look the same after subscripted. For example, a subscripted period looks
   about the same as a period: \<^isub>. and .
2) Don't subscript both an ASCII character and \<char> that will look the same.
   For example, subscripted ' and <acute> look about the same: \<^isub>' and \<^isub>\<acute>
3) Preferably, use the following four subscripted and superscripted characters to 
   create delimiters, since, after being subscripted they are fairly well centered, 
   discrete, and recognizable (recognizable if we know that a subscripted or 
   superscripted character used in a delimiter has to be one of these):
   *  \<^isub>*  subscript asterisk       \<^isub>*example\<^isub>*     \<^isub>*\<guillemotleft>example\<guillemotright>\<^isub>*     
   '  \<^isub>'  subscript tick           \<^isub>'example\<^isub>'
   `  \<^isub>`  subscript reverse tick   \<^isub>`example\<^isub>`
   ^  \<^isub>^  subscript caret          \<^isub>^example\<^isub>^
4) Other subscripted and superscripted characters that are fairly recognizable:
   ,  \<^isub>,  subscript comma          \<^isub>,example\<^isub>,     \<^isub>,\<guillemotleft>example\<guillemotright>\<^isub>,
   :  \<^isub>:  subscript colon          \<^isub>:example\<^isub>:
   +  \<^isub>+  subscript plus           \<^isub>+example\<^isub>+
   x  \<^isub>x  subscript x              \<^isub>xexample\<^isub>x   
   ,  \<^isup>,  superscript comma        \<^isup>,example\<^isup>,
   +  \<^isup>+  superscript plus         \<^isup>+example\<^isup>+
   x  \<^isup>x  superscript x            \<^isup>xexample\<^isup>x          
5) Non-subscripted characters to create delimiters that are somewhat discrete:
   .     period                   .example.    .\<guillemotleft>example\<guillemotright>.
   ,     comma                    ,example,
6) Subscripted \<...> commands         WILL IT BE SUBSCRIPTED IN EQUATIONS?
   \<^isub>\<stileturn> \<^isub>\<turnstile>   stileturn, turnstile
   \<^isub>\<lhd> \<^isub>\<rhd>   lhd, rhd
   \<^isub>\<unlhd> \<^isub>\<unrhd>   unlhd, unrhd
   \<^isub>\<and> \<^isub>\<and>   <and>
   \<^isub>\<lless> \<^isub>\<ggreater>  lless, ggreater
   \<^isub>\<lesssim> \<^isub>\<greatersim>   lesssim, greatersim
   \<^isub>\<lessapprox> \<^isub>\<greaterapprox>   lessapprox, greaterapprox
   \<^isub>\<box> \<^isub>\<box>   box
   \<^isub>\<circ> \<^isub>\<circ>    circ
   \<^isub>\<oplus> \<^isub>\<oplus>   oplus
   \<^isub>\<ominus> \<^isub>\<ominus>   ominus
   \<^isub>\<oslash> \<^isub>\<oslash>   oslash
   \<^isub>\<otimes> \<^isub>\<otimes>   otimes
   \<^isub>\<Oplus> \<^isub>\<Oplus>   Oplus
   \<^isub>\<Odot> \<^isub>\<Odot>   Odot
   \<^isub>\<Otimes> \<^isub>\<Otimes>   Otimes
   \<^isub>\<infinity> \<^isub>\<infinity>   infinity
   \<^isub>\<bar>  \<^isub>\<bar>   bar
   \<^isub>\<plusminus> \<^isub>\<plusminus>   plusminus
   \<^isub>\<minusplus> \<^isub>\<minusplus>   minusplus
   \<^isub>\<bullet> \<^isub>\<bullet>   bullet
   \<^isub>\<prec> \<^isub>\<succ>   prec, succ
   \<^isub>\<lfloor> \<^isub>\<rfloor>   lfloor, rfloor                  Probably, as greatest integer
   \<^isub>\<lceil> \<^isub>\<rceil>   lceil, rceil                    Probably, as least integer
*)

subsection{* Text and text formatting *}
(*
WHAT IT IS                  THE MARKUP                         EXAMPLE
text{*...*}                 --"<^isub>'text"                   --"\<^isub>'text"
double quotes               <hungarumlaut>text<hungarumlaut>  \<hungarumlaut>quoted text\<hungarumlaut>
italic                      <^isub>^text^<^isub>               \<^isub>^a\<^isub>^
\textt                      <^isub>*text*<^isub>               \<^isub>*text\<^isub>*
*)

subsection{* Equations *}
(*
\ensuremath{math}           <^isub>`math<^isub>`

\begin{eqnarray}[c]         <^isub><lhd>equation<^isub><lhd>
    
\begin{eqnarray}[rcl]       <^isub><lless>equation<^isub><ggreater>                 
  a) "&" will be substituted for <^isub><lozenge>
  b) "\\" will be inserted at newlines.
*)

subsection{* cite, index, footnote ref, label *}
(*
\cite      \<langle>\<^isub>`seGol.59, seJec, loBil.20\<^isub>`\<rangle>

\index     \<^isub>\<stileturn>anRud \<langle>59\<rangle>\<^isub>\<turnstile>  

\footnote  \<langle>\<^isub>*footnote\<^isub>*\<rangle>

\ref  
  Reference_type \<langle>abcd59a\<rangle>
  a) "Reference_type" must exactly match a word which corresponds to a command
     for which a \label can be assigned, which are:
       Chapter
       Section
       Equation
  
\label 
  \<langle>ymdhMMs\<rangle>
  a) Chars: a-z A-Z period (I could make it any characters \label will accept)
  b) Append reference labels on an as needed basis.
  c) Example equ.:   \<guillemotleft>equation\<guillemotright> \<langle>ymdhMMs\<rangle>
  d) Example sec:    section{ * a title * } --"\<langle>ymdhMMs\<rangle>" 
  e) Abbreviations:
     y   year      a-z means 1 to 26
     m   month     a-l means 1 to 12
     d   day       a-z-A-E means 1 to 31
     h   hour      a-w means 1 to 23, 0 means the zero hour
     MM  minutes   0-59 minutes
     s   seconds   a-l means 1 to 12, so s = floor(second/5)
    
     When making notes on a textbook, it means [page.pagePart.characterRef].
    
     a=1   b=2   c=3   d=4   e=5   f=6   g=7   h=8   i=9  j=10  k=11  l=12  m=13
     n=14  o=15  p=16  q=17  r=18  s=19  t=20  u=21  v=22 w=23  x=24  y=25  z=26
     A=27  B=28  C=29  D=30  E=31
*)

--"\<^bold>I\<^bold>S\<^bold>A\<^bold>R \<^bold>(Theory end.\<^bold>)"
end
--"\<^bold>[\<^bold>\<Theta>\<^bold>]"