--- a/doc-src/ProgProve/Makefile Mon Apr 02 21:26:46 2012 +0100
+++ b/doc-src/ProgProve/Makefile Tue Apr 03 08:55:06 2012 +0200
@@ -10,7 +10,7 @@
NAME = prog-prove
FILES = prog-prove.tex prog-prove.bib Thys/document/*.tex prelude.tex \
- svmono.cls mathpartir.sty isabelle.sty isabellesym.sty
+ svmono.cls mathpartir.sty isabelle.sty isabellesym.sty Thys/MyList.thy
dvi: $(NAME).dvi
--- a/doc-src/ProgProve/Thys/Bool_nat_list.thy Mon Apr 02 21:26:46 2012 +0100
+++ b/doc-src/ProgProve/Thys/Bool_nat_list.thy Tue Apr 03 08:55:06 2012 +0200
@@ -387,10 +387,11 @@
@{text"length :: 'a list \<Rightarrow> nat"} (with the obvious definition),
and the map function that applies a function to all elements of a list:
\begin{isabelle}
-\isacom{fun} @{text "map :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"}\\
-@{thm map.simps(1)} @{text"|"}\\
-@{thm map.simps(2)}
+\isacom{fun} @{const map} @{text"::"} @{typ[source] "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"}\\
+@{text"\""}@{thm map.simps(1)}@{text"\" |"}\\
+@{text"\""}@{thm map.simps(2)}@{text"\""}
\end{isabelle}
+\sem
Also useful are the \concept{head} of a list, its first element,
and the \concept{tail}, the rest of the list:
\begin{isabelle}
@@ -405,6 +406,8 @@
Note that since HOL is a logic of total functions, @{term"hd []"} is defined,
but we do now know what the result is. That is, @{term"hd []"} is not undefined
but underdefined.
+\endsem
+%
*}
(*<*)
end
--- a/doc-src/ProgProve/Thys/Isar.thy Mon Apr 02 21:26:46 2012 +0100
+++ b/doc-src/ProgProve/Thys/Isar.thy Tue Apr 03 08:55:06 2012 +0200
@@ -178,7 +178,7 @@
\subsection{Structured lemma statements: \isacom{fixes}, \isacom{assumes}, \isacom{shows}}
Lemmas can also be stated in a more structured fashion. To demonstrate this
-feature with Cantor's theorem, we rephrase \noquotes{@{prop[source]"\<not> surj f"}}
+feature with Cantor's theorem, we rephrase @{prop"\<not> surj f"}
a little:
*}
@@ -190,7 +190,8 @@
txt{* The optional \isacom{fixes} part allows you to state the types of
variables up front rather than by decorating one of their occurrences in the
formula with a type constraint. The key advantage of the structured format is
-the \isacom{assumes} part that allows you to name each assumption. The
+the \isacom{assumes} part that allows you to name each assumption; multiple
+assumptions can be separated by \isacom{and}. The
\isacom{shows} part gives the goal. The actual theorem that will come out of
the proof is @{prop"surj f \<Longrightarrow> False"}, but during the proof the assumption
@{prop"surj f"} is available under the name @{text s} like any other fact.
@@ -393,7 +394,8 @@
text_raw{*
\begin{isamarkuptext}%
-How to prove set equality and subset relationship:
+
+Finally, how to prove set equality and subset relationship:
\end{isamarkuptext}%
\begin{tabular}{@ {}ll@ {}}
\begin{minipage}[t]{.4\textwidth}
@@ -544,7 +546,7 @@
\subsection{Raw proof blocks}
-Sometimes one would like to prove some lemma locally with in a proof.
+Sometimes one would like to prove some lemma locally within a proof.
A lemma that shares the current context of assumptions but that
has its own assumptions and is generalised over its locally fixed
variables at the end. This is what a \concept{raw proof block} does:
@@ -745,7 +747,7 @@
\begin{quote}
\isacom{fix} @{text n}\\
\isacom{assume} @{text"Suc:"}
- \begin{tabular}[t]{l}@{text"A(n) \<Longrightarrow> P(n)"}\\@{text"A(Suc n)"}\end{tabular}\\
+ \begin{tabular}[t]{l}@{text"\"A(n) \<Longrightarrow> P(n)\""}\\@{text"\"A(Suc n)\""}\end{tabular}\\
\isacom{let} @{text"?case = \"P(Suc n)\""}
\end{quote}
The list of assumptions @{text Suc} is actually subdivided
@@ -812,8 +814,8 @@
~\\
\isacom{fix} @{text n}\\
\isacom{assume} @{text"evSS:"}
- \begin{tabular}[t]{l} @{text"ev n"}\\@{text"even n"}\end{tabular}\\
-\isacom{let} @{text"?case = even(Suc(Suc n))"}\\
+ \begin{tabular}[t]{l} @{text"\"ev n\""}\\@{text"\"even n\""}\end{tabular}\\
+\isacom{let} @{text"?case = \"even(Suc(Suc n))\""}\\
\end{minipage}
\end{tabular}
\medskip
--- a/doc-src/ProgProve/Thys/Logic.thy Mon Apr 02 21:26:46 2012 +0100
+++ b/doc-src/ProgProve/Thys/Logic.thy Tue Apr 03 08:55:06 2012 +0200
@@ -438,7 +438,7 @@
inductive ev :: "nat \<Rightarrow> bool" where
ev0: "ev 0" |
evSS: (*<*)"ev n \<Longrightarrow> ev (Suc(Suc n))"(*>*)
-text_raw{* @{prop"ev n \<Longrightarrow> ev (n + 2)"} *}
+text_raw{* @{prop[source]"ev n \<Longrightarrow> ev (n + 2)"} *}
text{* To get used to inductive definitions, we will first prove a few
properties of @{const ev} informally before we descend to the Isabelle level.
--- a/doc-src/ProgProve/Thys/Types_and_funs.thy Mon Apr 02 21:26:46 2012 +0100
+++ b/doc-src/ProgProve/Thys/Types_and_funs.thy Tue Apr 03 08:55:06 2012 +0200
@@ -55,7 +55,7 @@
As an example, consider binary trees:
*}
-datatype 'a tree = Tip | Node "('a tree)" 'a "('a tree)"
+datatype 'a tree = Tip | Node "'a tree" 'a "'a tree"
text{* with a mirror function: *}
@@ -86,8 +86,8 @@
done
(*>*)
fun lookup :: "('a * 'b) list \<Rightarrow> 'a \<Rightarrow> 'b option" where
-"lookup [] x' = None" |
-"lookup ((x,y) # ps) x' = (if x = x' then Some y else lookup ps x')"
+"lookup [] x = None" |
+"lookup ((a,b) # ps) x = (if a = x then Some b else lookup ps x)"
text{*
Note that @{text"\<tau>\<^isub>1 * \<tau>\<^isub>2"} is the type of pairs, also written @{text"\<tau>\<^isub>1 \<times> \<tau>\<^isub>2"}.
--- a/doc-src/ProgProve/Thys/document/Bool_nat_list.tex Mon Apr 02 21:26:46 2012 +0100
+++ b/doc-src/ProgProve/Thys/document/Bool_nat_list.tex Tue Apr 03 08:55:06 2012 +0200
@@ -557,10 +557,11 @@
\isa{length\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat} (with the obvious definition),
and the map function that applies a function to all elements of a list:
\begin{isabelle}
-\isacom{fun} \isa{map\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ list}\\
-\isa{map\ f\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} \isa{{\isaliteral{7C}{\isacharbar}}}\\
-\isa{map\ f\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{23}{\isacharhash}}\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ x\ {\isaliteral{23}{\isacharhash}}\ map\ f\ xs}
+\isacom{fun} \isa{map} \isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}} \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ list{\isaliteral{22}{\isachardoublequote}}}\\
+\isa{{\isaliteral{22}{\isachardoublequote}}}\isa{map\ f\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}}\isa{{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{7C}{\isacharbar}}}\\
+\isa{{\isaliteral{22}{\isachardoublequote}}}\isa{map\ f\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{23}{\isacharhash}}\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ x\ {\isaliteral{23}{\isacharhash}}\ map\ f\ xs}\isa{{\isaliteral{22}{\isachardoublequote}}}
\end{isabelle}
+\sem
Also useful are the \concept{head} of a list, its first element,
and the \concept{tail}, the rest of the list:
\begin{isabelle}
@@ -574,7 +575,9 @@
\end{isabelle}
Note that since HOL is a logic of total functions, \isa{hd\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} is defined,
but we do now know what the result is. That is, \isa{hd\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} is not undefined
-but underdefined.%
+but underdefined.
+\endsem
+%%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/ProgProve/Thys/document/Isar.tex Mon Apr 02 21:26:46 2012 +0100
+++ b/doc-src/ProgProve/Thys/document/Isar.tex Tue Apr 03 08:55:06 2012 +0200
@@ -269,7 +269,7 @@
\subsection{Structured lemma statements: \isacom{fixes}, \isacom{assumes}, \isacom{shows}}
Lemmas can also be stated in a more structured fashion. To demonstrate this
-feature with Cantor's theorem, we rephrase \noquotes{\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ surj\ f{\isaliteral{22}{\isachardoublequote}}}}
+feature with Cantor's theorem, we rephrase \isa{{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ surj\ f}
a little:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -288,7 +288,8 @@
The optional \isacom{fixes} part allows you to state the types of
variables up front rather than by decorating one of their occurrences in the
formula with a type constraint. The key advantage of the structured format is
-the \isacom{assumes} part that allows you to name each assumption. The
+the \isacom{assumes} part that allows you to name each assumption; multiple
+assumptions can be separated by \isacom{and}. The
\isacom{shows} part gives the goal. The actual theorem that will come out of
the proof is \isa{surj\ f\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ False}, but during the proof the assumption
\isa{surj\ f} is available under the name \isa{s} like any other fact.%
@@ -672,7 +673,8 @@
\endisadelimproof
%
\begin{isamarkuptext}%
-How to prove set equality and subset relationship:
+
+Finally, how to prove set equality and subset relationship:
\end{isamarkuptext}%
\begin{tabular}{@ {}ll@ {}}
\begin{minipage}[t]{.4\textwidth}
@@ -942,7 +944,7 @@
\subsection{Raw proof blocks}
-Sometimes one would like to prove some lemma locally with in a proof.
+Sometimes one would like to prove some lemma locally within a proof.
A lemma that shares the current context of assumptions but that
has its own assumptions and is generalised over its locally fixed
variables at the end. This is what a \concept{raw proof block} does:
@@ -1307,7 +1309,7 @@
\begin{quote}
\isacom{fix} \isa{n}\\
\isacom{assume} \isa{Suc{\isaliteral{3A}{\isacharcolon}}}
- \begin{tabular}[t]{l}\isa{A{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}}\\\isa{A{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}}\end{tabular}\\
+ \begin{tabular}[t]{l}\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\end{tabular}\\
\isacom{let} \isa{{\isaliteral{3F}{\isacharquery}}case\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}P{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}
\end{quote}
The list of assumptions \isa{Suc} is actually subdivided
@@ -1399,8 +1401,8 @@
~\\
\isacom{fix} \isa{n}\\
\isacom{assume} \isa{evSS{\isaliteral{3A}{\isacharcolon}}}
- \begin{tabular}[t]{l} \isa{ev\ n}\\\isa{even\ n}\end{tabular}\\
-\isacom{let} \isa{{\isaliteral{3F}{\isacharquery}}case\ {\isaliteral{3D}{\isacharequal}}\ even{\isaliteral{28}{\isacharparenleft}}Suc{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}}\\
+ \begin{tabular}[t]{l} \isa{{\isaliteral{22}{\isachardoublequote}}ev\ n{\isaliteral{22}{\isachardoublequote}}}\\\isa{{\isaliteral{22}{\isachardoublequote}}even\ n{\isaliteral{22}{\isachardoublequote}}}\end{tabular}\\
+\isacom{let} \isa{{\isaliteral{3F}{\isacharquery}}case\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}even{\isaliteral{28}{\isacharparenleft}}Suc{\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\
\end{minipage}
\end{tabular}
\medskip
--- a/doc-src/ProgProve/Thys/document/Logic.tex Mon Apr 02 21:26:46 2012 +0100
+++ b/doc-src/ProgProve/Thys/document/Logic.tex Tue Apr 03 08:55:06 2012 +0200
@@ -570,7 +570,7 @@
\ ev\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
ev{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}\ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}ev\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
evSS{\isaliteral{3A}{\isacharcolon}}\ \ %
-\isa{ev\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ ev\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}}
+\isa{{\isaliteral{22}{\isachardoublequote}}ev\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ ev\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}
%
\begin{isamarkuptext}%
To get used to inductive definitions, we will first prove a few
--- a/doc-src/ProgProve/Thys/document/Types_and_funs.tex Mon Apr 02 21:26:46 2012 +0100
+++ b/doc-src/ProgProve/Thys/document/Types_and_funs.tex Tue Apr 03 08:55:06 2012 +0200
@@ -68,7 +68,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{datatype}\isamarkupfalse%
-\ {\isaliteral{27}{\isacharprime}}a\ tree\ {\isaliteral{3D}{\isacharequal}}\ Tip\ {\isaliteral{7C}{\isacharbar}}\ Node\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ tree{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ tree{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+\ {\isaliteral{27}{\isacharprime}}a\ tree\ {\isaliteral{3D}{\isacharequal}}\ Tip\ {\isaliteral{7C}{\isacharbar}}\ Node\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ tree{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{27}{\isacharprime}}a\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ tree{\isaliteral{22}{\isachardoublequoteclose}}%
\begin{isamarkuptext}%
with a mirror function:%
\end{isamarkuptext}%
@@ -122,8 +122,8 @@
\endisadelimproof
\isacommand{fun}\isamarkupfalse%
\ lookup\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}lookup\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ x{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ None{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}lookup\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{23}{\isacharhash}}\ ps{\isaliteral{29}{\isacharparenright}}\ x{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ x\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{27}{\isacharprime}}\ then\ Some\ y\ else\ lookup\ ps\ x{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+{\isaliteral{22}{\isachardoublequoteopen}}lookup\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ x\ {\isaliteral{3D}{\isacharequal}}\ None{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
+{\isaliteral{22}{\isachardoublequoteopen}}lookup\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{23}{\isacharhash}}\ ps{\isaliteral{29}{\isacharparenright}}\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ a\ {\isaliteral{3D}{\isacharequal}}\ x\ then\ Some\ b\ else\ lookup\ ps\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
\begin{isamarkuptext}%
Note that \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}} is the type of pairs, also written \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}.