# Status of the IAU Meteor Data Center

Regina Rudawska1, Mária Hajduková2, Tadeusz J. Jopek3,
Luboš Neslušan4, Marián Jakubík4, Ján Svoreň4

(1RHEA group/ESA ESTEC, The Netherlands, 2Astronomical Institute of the Slovak
Academy of Sciences, Bratislava, Slovak Republic, 3Astronomical Observatory
Institute, Faculty of Physics, A.M. University, Poznań, Poland, 4Astronomical
Institute of the Slovak Academy of Sciences, Tatranská Lomnica, Slovak
Republic)

Accepted: Proceeding of IMC2021, to be published in WGN, the Journal of the
IMO.

### Abstract

Since 2007, the Meteor Data Center (MDC) has had two components: the ”Orbital
database” (OD) and the ”Shower database” (SD). The orbital part is in charge
of the eﬀicient collection, checking, and dissemination of geocentric
parameters and orbits of individual orbits. It also acts as a central
depository for meteoroid orbits obtained by different techniques:
photographic, television, video, CCD and radar.
The shower database collects the geocentric and orbital parameters of the
meteor showers and meteoroid streams. It is not an archive of all information
related to meteor showers, its primary task is to give unique names and codes
to new meteor showers (streams). The SD acts in conjunction with the Working
Group on Meteor Shower Nomenclature of International Astronomical Union (IAU)
Commission F1, ”Meteors, Meteorites, and Interplanetary Dust”.
In our paper, we give a concise description of the IAU MDC database, its
origin, structure and, in particular, the current requirements for the
introduction of new orbital and shower data.

##  1 Introduction

The Meteor Data Centre (MDC)111https://www.iaumeteordatacenter.org/ was
established at the General Assembly of the IAU held in 1982, in Patras, and at
that time compiled only orbital data. In 2006, in Prague, Commission 22 of the
IAU established a Task Group for Meteor Shower Nomenclature, (see [1]). 222In
2009 the Task Group was transformed into the Working Group on Meteor Shower
Nomenclature. In the following year, the meteor shower database was created as
part of the IAU MDC, and two years later, in 2009, in Rio de Janeiro, for the
first time in the history of meteor astronomy, $64$ meteor showers were
oﬀicially named by the GA IAU, (see [2, 3, 4]). The official names of the
subsequent 48 showers were approved at the GA IAU held in Beijing and Honolulu
(see [5, 6]).

Over the years, the structure of the MDC database and the rules of its
management have changed, see [7, 8, 9, 10, 11, 12].

Catalogue/Source | Number of orbits
---|---
Photographic/various data | 4 873
Video/CAMS | 110 521
Video/SonotaCo | 353 231
Radar/Hissar | 8 916
Table 1: IAU MDC orbital data status October 2021.

In this work, the words meteoroid stream and meteor shower can be understood
as synonyms. Their current definition adopted by the IAU is available in the
work of [13].

In the current OD, each new sample of the orbits submitted is saved separately
(though in a consistent form) and can also be downloaded separately. This rule
has already been applied to all of the video orbits in the database. The
orbital database consists of more than 450 000 orbits, see Table 1. The
magnitude distributions of the meteors caused by the meteoroids with known
orbital data are shown in Figure 1, separately for the meteors detected by
photographic (a) and video (b) techniques (photographic meteors and video
meteors, hereafter). In Figure 2, there are, furthermore, the orbital elements
of the meteoroids observed by video technique. Only the Cameras for Allsky
Meteor Surveillance (CAMS, [14, 15, 16, 17]) video meteors were included in
the database at the time of plotting the graphs.

Type of list | Number of showers
---|---
List of All Showers | 917
List of Established Showers | 112
Working List | 781
List of Shower Groups | 24
List of Removed Showers | 44
Table 2: IAU MDC shower lists in October 2021.

Currently, the SD component contains over 900 meteor showers; their names are
grouped in the form of five lists, see Table 2. The first list consists of the
names of all unique showers actually registered in the database. 450 of them
are represented by more than one set of parameters (so called solutions). The
names of the showers already approved by the IAU are also listed separately in
the List of Established Showers. The Working List constitutes showers that
have yet to be confirmed (by other authors or other data). The List of Meteor
Shower Groups consists of groups/complexes that have been suggested in a
scientific publication. In Figure 3 we plotted the radiants of the meteor
showers from the Working and Established lists on the whole celestial sphere.
As one can see, in the northern sphere of the ecliptic system, we have
slightly more meteor radiants.

Removed showers remain in the MDC in a separate list. The list contains the
names of showers that were previously on the Working List and were excluded
from it for various, very individual reasons. The problem of removing
unnecessary data from the Working List was discussed during the Meteoroids
2019 conference, ([12]). The Working List may include duplicates and data of
very low statistical significance; for example, a shower (steam) identified by
means of two orbits only. It was decided that any shower (stream) would be
removed from the Working List if a work recommending such a decision was
published. After a recommendation for removal, the MDC will move the shower to
the List of Removed Showers and add a note giving the reason for the removal
on the MDC Web site. Any removed shower can eventually return to the Working
List after such a recommendation has been published. However, it should be
noted that an incomplete record (e.g. no orbital data) is not a reason for
removal, as long as the proposed shower is uniquely identified by the
geocentric parameters.

##  2 How to submit new data

The current requirements for submission and the points of contact are on the
website, listed separately for orbital and shower data.

###  2.1 New orbits of meteoroids

A new set of orbital data sent to the MDC has to be accompanied by a paper or
papers, which should have been published in a peer reviewed journal before
submission to the MDC. The paper(s) should provide a description of the
observational facility used to detect the meteors and a description of the
method of processing the observations, as well as the way of calculating the
parameters presented. References to this paper(s) must be sent to the IAU MDC
together with the data (it is assumed that the papers will be cited by users).
If the authors send another set of data gained using the same observational
equipment and the same method of data processing, the accompanying paper is
not required.

For each meteor, the complete set of compulsory parameters must be given. The
compulsory parameters are:

  1. 1.

date of the meteor detection (in the form: year, month, day and fraction of
day, giving the time of meteor detection in U.T.),

  2. 2.

right ascension and declination of the geocentric radiant (in degrees),

  3. 3.

geocentric and heliocentric velocities (in km s-1),

  4. 4.

perihelion distance of meteor orbit (in AU),

  5. 5.

its numerical eccentricity,

  6. 6.

argument of perihelion (in degrees),

  7. 7.

longitude of ascending node (in degrees), and

  8. 8.

inclination (in degrees).

The angular parameters should be referred to the actual equinox of J2000.0.
Ideally, at least some of these parameters should be given with their error
limits.

Besides the compulsory parameters, the authors of new data on the meteors can
also supply some of 22 additional parameters for every meteor. The list of 21
of those parameters currently accepted by the IAU MDC was published in a paper
by [18], Table 1. The 22nd parameter, duration of meteor, was added recently,
in the process of incorporating the SonotaCo data ([19, 20, 21]).

Before the proper sending of new orbital data, the authors are requested to
communicate the way of sending and format of the data with the MDC-OD
team333mdc<EMAIL_ADDRESS>
Figure 1: The magnitude distribution of all photographic (panel a) and CAMS
video (b) meteors. Eleven video meteors brighter than $-6^{m}$ are out of the
shown range.

Figure 2: The distributions of perihelion distance (panel a), reciprocal semi-
major axis (b), eccentricity (c), argument of perihelion (d), longitude of
ascending node (e), and inclination (f) of the video meteors in the CAMS MDC
database.

Figure 3: Ecliptical coordinates of the mean radiants of the meteor showers in
Aitoff-Hammer’s projection. $781$ radiants from the MDC working list are
marked with red squares. $112$ shower radiants from the Established list are
marked with blue triangles.

###  2.2 Delivery of meteor showers

Observers may send data for both unknown and well-known meteoroid streams to
the SD. Data provided of a stream which already exist in the MDC will be used
to confirm its real existence. Modern methods of identifying meteoroid streams
do not guarantee that the results obtained were not obtained by chance.

The shower database is not an archive of all meteoroid information. It only
stores those parameters that are necessary to determine whether we are dealing
with a new stream or with a well-known stream. Hence the geocentric longitude
of the Sun, the radiant coordinates, and geocentric velocity are required, as
well as the heliocentric elements of the orbit. However, only the geocentric
parameters are obligatory, while the orbital elements are very much
appreciated. The basic planes of the reference system used in the MDC are the
mean equator and the mean ecliptic of the epoch J2000. The moment of time of
the shower activity is represented by the ecliptic longitude of the Sun. In
brief, the data sent to the MDC may include:

  1. 1.

Activity – the year of observed shower activity. If observed regularly - the
word annual should be given.

  2. 2.

S. Lon – the mean solar ecliptic longitude at the moment of observation of the
members of the shower. (degrees, epoch J2000).

  3. 3.

RA – mean geocentric right ascension of the shower radiant (degrees, epoch
J2000).

  4. 4.

DE – mean geocentric declination of the shower radiant (degrees, epoch J2000).

  5. 5.

dRA – radiant drift in right ascension (not obligatory, degrees RA per degree
of solar longitude, epoch J2000).

  6. 6.

dDE – radiant drift in declination (not obligatory, degrees DE per degree of
solar longitude, epoch J2000).

  7. 7.

VG – mean geocentric speed (km s-1).

  8. 8.

a – mean semi-major axis (AU).

  9. 9.

q – mean perihelion distance (AU).

  10. 10.

e – mean eccentricity.

  11. 11.

Peri – mean argument of perihelion (degrees, epoch J2000).

  12. 12.

Node – mean longitude of ascending node (degrees, epoch J2000).

  13. 13.

Incl – mean inclination of the orbital plane (degrees, epoch J2000).

  14. 14.

N – number of meteors used to determine the mean radiant and orbit.

  15. 15.

OT – code of the technique used for the meteor shower observation: P – photo,
R – radar, T – TV, video, C- CCD, V – visual.

  16. 16.

Information where the submitted meteor data will be published.

  17. 17.

Also, the author may propose unique name of the submitted shower, as well as
its unique 3-letter code.

All meteoroid data should be sent to the MDC as an ASCII file, according to
the template available on the MDC website. Next, the MDC verifies the
correctness of the proposed stream name and 3 letter code. If necessary, the
MDC determines the correct name and code. From this moment, within 6 months,
using the obtained shower name and code, the author should publish a paper
describing his/her submission. Publications in any peer-reviewed scientific
journal are accepted, but also in amateur journals such as WGN or MeteorNews.

As the mean values of the meteoroid parameters, most authors give the
arithmetic means of the corresponding parameters of the stream members. Other
authors provide median values of the individual parameters. However, both such
approaches do not guarantee consistency between the given parameters, e.g. the
mean value of the semi-major axis is usually not equal to the semi-axis
calculated using arithmetic means or medians of eccentricity and perihelion
distance. This means that the mean values of the orbital elements reported in
the MDC do not represent the orbit of a meteoroid stream in terms of celestial
mechanics.

On the MDC website, there are templates of two files: the shower mean data
444https://www.ta3.sk/IAUC22DB/MDC2007/Etc/streamMDC-Template.txt and the
Look-up table 555https://www.ta3.sk/IAUC22DB/MDC2007/Etc/streamLT-
Template.csv, which the user must complete and submit to the MDC. The first
file contains mean parameters describing the submitted shower and which are
included in the kernel of the shower database. The second file, the so-called
’Look-up table’, contains the data of individual meteoroids, the members of a
given stream. These are members of the stream, the data of which were used to
determine the average values of the stream parameters. The content of the
Look-up table was established at the Meteoroids 2019 conference, (see [12])
during the business meeting of the Working Group on Meteor Shower Nomenclature
(IAU Commission F1: Meteors, Meteorites, and Interplanetary Dust).

Each Look-up table must contain the following information for each meteor on
which the new identification is based:

  1. 1.

CurNum – current number of the meteor in the Look-up table.

  2. 2.

SolLon – ecliptic longitude of Sun at the meteor instant (degrees, J2000).

  3. 3.

SCELoG – Sun centered ecliptic longitude of the geocentric radiant (degrees).

  4. 4.

ELaG – ecliptic latitude of the geocentric radiant (degrees, J2000).

  5. 5.

VG – geocentric velocity [km s-1].

  6. 6.

IAUNo – IAU numerical code of the shower.

  7. 7.

IAUCod – IAU 3 letter code of the shower, (not obligatory).

  8. 8.

CatCod – code of the source catalogue of the meteor, (not obligatory).

  9. 9.

MetCod – meteor code given in the source catalogue, (not obligatory).

More details on the required data format of the Look-up table records are
given in the template on the MDC website.

The Look-up tables provided to the MDC will allow a more complete insight into
the meteoroid streams submitted to the database. They contain information
about shower duration, as well as radiant and speed dispersion. The MDC user,
by comparing the contents of the tables, will therefore be able to assess
whether an identified ’new’ stream is already in the MDC.

##  3 Conclusions

As a result of the changes in the mode of operation of the MDC shower base,
more than 40 streams were moved to the List of Removed Showers or added as
another solution of a previously known stream. These were mostly duplicates.
We are convinced that the introduced changes, a critical assessment of the
database content and the way it functions, have led to an improvement in the
quality of data contained in the SD, and make the lists more valuable for
users.

It will be recalled that before publishing, each new meteoroids stream must
receive a unique name, the IAU numeric and 3-letter code from the MDC.
Moreover, each new entry to the MDC must be published in a scientific journal
or meteor amateur journal like WGN (the Journal of the IMO) or MeteorNews. In
order to avoid permanent deletion from the MDC, the published manuscript
describing the study must be sent to the MDC within half a year of requesting
the shower names and codes. Each new submission to the MDC should be
accompanied by the corresponding ”Lookup table” that gives the shower members’
parameters.

Concerning the OD component of the MDC database, its video part will be
upgraded in a near future; specifically, version 2 of the CAMS data will be
replaced by version 3. Altogether, the new version of the CAMS data contains
471577 video meteors.

The MDC database is not perfect. It still contains incorrect data: mistakes
and errors, inconsistent values of the parameters, missing information about
the data source etc. Furthermore, the functionality of the database could be
improved. Hence, we appreciate every critical remark related to the content
and the operation of the MDC.

## Acknowledgments

The authors like to acknowledge: Reiner Arlt, David Asher, Rhiannon Blaauw,
Steve Hutcheon, Sirko Molau, Ned Smith, Francisco Ocaña, Željko Andreić, Damir
Šegon, Denis Vida, Allan Mulof, Paul Roggemans, Galina Ryabova, Masahiro
Koseki, Alfredo Dal’Ava Júnior, Mikiya Sato, Diego Janches, Jiří Borovička,
Zuzana Kaňuchová, Ivan Sergey and Peter Jenniskens who in recent years helped
improve the IAU MDC contents.

This research has made use of NASA’s Astrophysics Data System Bibliographic
Services.

## References

  * [1] Pavel Spurný, Junichi Watanabe, Ingrid Mann, William J. Baggaley, Jiří Borovička, Peter G. Brown, Guy J. Consolmagno, Peter Jenniskens, Asta K. Pellinen-Wannberg, Vladimír Porubčan, Iwan P. Williams, and Hajime Yano.  Commission 22: Meteors, Meteorites and Interplanetary Dust.  Transactions of the International Astronomical Union, Series B, 3(26B):140–141, December 2007.
  * [2] Edward L. G. Bowell, Karen J. Meech, Iwan P. Williams, Alan Boss, Régis Courtin, Bo Å. S. Gustafson, Anny-Chantal Levasseur-Regourd, Michel Mayor, Pavel Spurný, Junichi Watanabe, Guy J. Consolmagno, Julio A. Fernández, Walter F. Huebner, Mikhail Ya. Marov, Rita M. Schulz, Giovanni B. Valsecchi, and Adolf N. Witt.  Division III: Planetary Systems Science.  Transactions of the International Astronomical Union, Series B, 6(T27):158–167, May 2010.
  * [3] Junichi Watanabe, Peter Jenniskens, Pavel Spurný, Jiří Borovička, Margaret Campbell-Brown, Guy Consolmagno, Tadeusz Jopek, Jeremie Vaubaillon, Iwan P. Williams, and Jin Zhu.  Commission 22: Meters, Meteorites and Interplanetary Dust.  Transactions of the International Astronomical Union, Series B, 6(T27):177–179, May 2010.
  * [4] T. J. Jopek and P. M. Jenniskens.  The Working Group on Meteor Showers Nomenclature: A History, Current Status and a Call for Contributions.  In W. J. Cooke, D. E. Moser, B. F. Hardin, and D. Janches, editors, Meteoroids: The Smallest Solar System Bodies, pages 7–13, July 2011.
  * [5] T. J. Jopek and Z. Kaňuchová.  Current status of the IAU MDC Meteor Showers Database.  In T. J. Jopek, F. J. M. Rietmeijer, J. Watanabe, and I. P. Williams, editors, Meteoroids 2013, pages 353–364, July 2014.
  * [6] T. J. Jopek and Z. Kaňuchová.  IAU Meteor Data Center-the shower database: A status report.  Planetary Space Science, 143:3–6, September 2017.
  * [7] B. A. Lindblad.  The IAU Meteor Data Center in Lund.  Publications of the Astronomical Institute of the Czechoslovak Academy of Sciences, 67:201–204, January 1987.
  * [8] B. A. Lindblad and D. I. Steel.  Meteoroid Orbits Available from the IAU Meteor Data Center.  In Andrea Milani, Michel di Martino, and A. Cellino, editors, Asteroids, Comets, Meteors 1993, volume 160, page 497, January 1994.
  * [9] B. A. Lindblad, L. Neslušan, V. Porubčan, and J. Svoreň.  IAU Meteor Database of photographic orbits version 2003.  Earth Moon and Planets, 93(4):249–260, December 2003.
  * [10] V. Porubčan, J. Svoreň, L. Neslušan, and E. Schunová.  The Updated IAU MDC Catalogue of Photographic Meteor Orbits.  In W. J. Cooke, D. E. Moser, B. F. Hardin, and D. Janches, editors, Meteoroids: The Smallest Solar System Bodies, page 338, July 2011\.
  * [11] L. Neslušan, V. Porubčan, and J. Svoreň.  IAU MDC Photographic Meteor Orbits Database: Version 2013.  Earth Moon and Planets, 111(3-4):105–114, May 2014.
  * [12] Peter Jenniskens, Tadeusz J. Jopek, Diego Janches, Maria Hajduková, Gulchehra I. Kokhirova, and Regina Rudawska.  On removing showers from the IAU Working List of Meteor Showers.  Planetary Space Science, 182:104821, March 2020.
  * [13] Detlef Koschny and Jiri Borovicka.  Definitions of terms in meteor astronomy.  WGN, Journal of the International Meteor Organization, 45(5):91–92, October 2017.
  * [14] P. Jenniskens, P. S. Gural, L. Dynneson, B. J. Grigsby, K. E. Newman, M. Borden, M. Koop, and D. Holman.  CAMS: Cameras for Allsky Meteor Surveillance to establish minor meteor showers.  Icarus, 216:40–61, November 2011.
  * [15] P. Jenniskens, Q. Nénon, P. S. Gural, J. Albers, B. Haberman, B. Johnson, D. Holman, R. Morales, B. J. Grigsby, D. Samuels, and C. Johannink.  CAMS confirmation of previously reported meteor showers.  Icarus, 266:355–370, March 2016.
  * [16] P. Jenniskens, Q. Nénon, P. S. Gural, J. Albers, B. Haberman, B. Johnson, R. Morales, B. J. Grigsby, D. Samuels, and C. Johannink.  CAMS newly detected meteor showers and the sporadic background.  Icarus, 266:384–409, March 2016.
  * [17] Peter Jenniskens and Quentin Nénon.  CAMS verification of single-linked high-threshold D-criterion detected meteor showers.  Icarus, 266:371–383, March 2016.
  * [18] M. Narziev, R. P. Chebotarev, T. J. Jopek, L. Neslušan, V. Porubčan, J. Svoreň, H. F. Khujanazarov, R. Sh Bibarsov, Sh N. Irkaeva, Sh O. Isomutdinov, V. N. Kolmakov, G. A. Polushkin, and V. N. Sidorin.  IAU MDC meteor orbits database - A sample of radio-meteor data from the Hissar Observatory.  Planetary and Space Science, 192:105008, November 2020.
  * [19] SonotaCo.  A meteor shower catalog based on video observations in 2007-2008.  WGN, Journal of the International Meteor Organization, 37:55–62, April 2009.
  * [20] SonotaCo.  Observation error propagation on video meteor orbit determination.  WGN, Journal of the International Meteor Organization, 44:42–45, April 2016.
  * [21] SonotaCo, T. Masuzawa, T. Sekiguchi, T. Miyoshi, Y. Fujiwara, K. Maeda, and S. Uehara.  Ongoing Meteor Work. SNMv3: A Meteor Data Set for Meteor Shower Analysis.  WGN, Journal of the International Meteor Organization, 49:64–70, 2021.


35.94196pt\hbox{$\displaystyle\Gamma_{\mathtt{TT}}\wedge\Gamma_{u}\vdash\mathtt{TT}{[}\\!{[}u{]}\\!{]}[x/u]:\mathcal{A}\mid\Delta_{\mathtt{TT}}\vee\Delta_{u}$}}}}$

where $x\in\mathtt{fv}(\mathtt{TT}{[}\\!{[}u{]}\\!{]})$ implies
$\mathcal{I}\neq[\,]$ by Lemma 22, so that $\mathcal{I}^{*}=\mathcal{I}$.

By Lemma 29 applied to $\Phi_{\mathtt{TT}{[}\\!{[}u{]}\\!{]}}$, we have
$\Gamma^{\prime}_{0},\,\Delta_{0},\,\mathcal{I}_{0}\neq[\,],\,\Gamma_{u}^{\prime},\,\Delta_{u}^{\prime}$
such that

    * –

$\Gamma_{\mathtt{TT}};x:\mathcal{I}=\Gamma^{\prime}_{0}\wedge\Gamma_{u}^{\prime}$,

    * –

$\Delta_{\mathtt{TT}}=\Delta_{0}\vee\Delta_{u}^{\prime}$,

    * –

$\Phi_{\mathtt{TT}{[}\\!{[}x{]}\\!{]}}\triangleright\Gamma^{\prime}_{0}\wedge
x:\mathcal{I}_{0}\vdash\mathtt{TT}{[}\\!{[}x{]}\\!{]}:\mathcal{A}\mid\Delta_{0}$

    * –

$\triangleright\Gamma_{u}^{\prime}\Vdash
u:\mathcal{I}_{0}\mid\Delta_{u}^{\prime}$.

We set
$\mathcal{I}^{{}^{\prime\prime}}=\mathcal{I}\wedge\mathcal{I}_{0},\,\Gamma_{u}^{{}^{\prime\prime}}=\Gamma_{u}\wedge\Gamma_{u}^{\prime},\,\Delta_{u}^{{}^{\prime\prime}}=\Delta_{u}\vee\Delta_{u}^{\prime}$.
Thus, in particular,
$({\mathcal{I}^{{}^{\prime\prime}}})^{*}=\mathcal{I}^{{}^{\prime\prime}}$. By
Lemma 22, $x\notin\mathtt{dom}(\Gamma_{u}^{\prime})$, so that
$\Gamma_{0}^{\prime}=\Gamma_{0};x:\mathcal{I}$ for some $\Gamma_{0}$ and thus
$\Gamma_{0}^{\prime}\wedge
x:\mathcal{I}_{0}=\Gamma_{0};x:\mathcal{I}^{{}^{\prime\prime}}$. By Lemma 11,
there is a derivation
$\Theta_{u}^{{}^{\prime\prime}}\triangleright\Gamma_{u}^{{}^{\prime\prime}}\Vdash
u:\mathcal{I}^{{}^{\prime\prime}}\mid\Delta_{u}^{{}^{\prime\prime}}$. We then
construct the following derivation $\Phi$ :

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 12.88762pt\hbox{$\displaystyle\penalty
1\Phi_{\mathtt{TT}{[}\\!{[}x{]}\\!{]}}\hskip
19.91684pt\Theta_{u}^{{}^{\prime\prime}}\triangleright\Gamma_{u}^{{}^{\prime\prime}}\vdash
u:\mathcal{I}^{{}^{\prime\prime}}\mid\Delta_{u}^{{}^{\prime\prime}}$}}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern
0.0pt$$}\vrule height=0.25002pt,depth=0.25002pt,width=136.94441pt\hbox{\kern
3.00003pt$(\mathtt{s})$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle\Gamma_{0}\wedge\Gamma_{u}^{{}^{\prime\prime}}\vdash\mathtt{TT}{[}\\!{[}x{]}\\!{]}[x/u]:\mathcal{A}\mid\Delta_{0}\vee\Delta_{u}^{{}^{\prime\prime}}$}}}}$

We conclude since
$\Gamma_{0}\wedge\Gamma_{u}^{{}^{\prime\prime}}=\Gamma_{0}\wedge\Gamma_{u}^{\prime}\wedge\Gamma_{u}=\Gamma_{\mathtt{TT}}\wedge\Gamma_{u}=\Gamma$
and
$\Delta_{0}\vee\Delta_{u}^{{}^{\prime\prime}}=\Delta_{0}\vee\Delta_{u}^{\prime}\vee\Delta_{u}=\Delta_{\mathtt{TT}}\vee\Delta_{u}=\Delta$.

  * •

If
$o=\mathtt{TT}{[}\\!{[}x{]}\\!{]}[x/u]\rightarrow\mathtt{TT}{[}\\!{[}u{]}\\!{]}=o^{\prime}$,
with $|\mathtt{TT}{[}\\!{[}x{]}\\!{]}|_{x}=1$. The derivation $\Phi^{\prime}$
ends with $\Gamma\vdash\mathtt{TT}{[}\\!{[}u{]}\\!{]}:\mathcal{A}\mid\Delta$
where $x\notin\mathtt{dom}(\Gamma)$ by Lemma 22. By Lemma 29 applied to
$\Phi^{\prime}$, we have
$\Gamma_{0},\,\Delta_{0},\,\mathcal{I}_{0}\neq[\,],\,\Gamma_{u},\,\Delta_{u}$
such that

    * –

$\Gamma=\Gamma_{0}\wedge\Gamma_{u}$,

    * –

$\Delta=\Delta_{0}\vee\Delta_{u}$,

    * –

$\Phi_{\mathtt{TT}{[}\\!{[}x{]}\\!{]}}\triangleright\Gamma_{0}\wedge
x:\mathcal{I}_{0}\vdash\mathtt{TT}{[}\\!{[}x{]}\\!{]}:\mathcal{A}\mid\Delta_{0}$

    * –

$\triangleright\Gamma_{u}\Vdash u:\mathcal{I}_{0}\mid\Delta_{u}$.

Thus in particular $\mathcal{I}_{0}^{*}=\mathcal{I}_{0}$. Since
$x\notin\mathtt{dom}(\Gamma)$, $x\notin\mathtt{dom}(\Gamma_{0})$, so that
$\Gamma_{0}\wedge x:\mathcal{I}_{0}=\Gamma_{0};x:\mathcal{I}_{0}$. We then
construct the following derivation $\Phi$ :

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 38.2959pt\hbox{$\displaystyle\penalty
1\Phi_{\mathtt{TT}{[}\\!{[}x{]}\\!{]}}\\\ \triangleright\Gamma_{u}\Vdash
u:\mathcal{I}_{0}\mid\Delta_{u}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=136.94441pt\hbox{\kern
3.00003pt$(\mathtt{s})$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle\Gamma_{0}\wedge\Gamma_{u}\vdash\mathtt{TT}{[}\\!{[}x{]}\\!{]}[x/u]:\mathcal{U}\mid\Delta_{0}\vee\Delta_{u}$}}}}$

We conclude since $\Gamma=\Gamma_{0}\wedge\Gamma_{u}$ and
$\Delta=\Delta_{0}\vee\Delta_{u}$.

  * •

If
$o=\mathtt{CC}{[}\\!{[}[\alpha]t{]}\\!{]}\langle\alpha/\\!\\!/\alpha^{\prime}.u\rangle\rightarrow\mathtt{CC}{[}\\!{[}[\alpha^{\prime}]tu{]}\\!{]}\langle\alpha/\\!\\!/\alpha^{\prime}.u\rangle=o^{\prime}$,
with $|\mathtt{CC}{[}\\!{[}[\alpha]t{]}\\!{]}_{\alpha}>1$. Then
$\Phi^{\prime}$ has the following form :

${{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1\Phi_{0}^{\prime}\triangleright\Gamma_{\mathtt{CC}}\vdash\mathtt{CC}{[}\\!{[}[\alpha^{\prime}]tu{]}\\!{]}:\mathcal{A}\mid\Delta_{\mathtt{CC}};\alpha^{\prime}:\mathcal{V}_{\alpha^{\prime}};\alpha:\mathcal{V}_{\alpha}\hskip
28.45274pt\Theta_{u}\triangleright\Gamma_{u}\Vdash
u:\mathcal{I}_{u}\mid\Delta_{u}$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=268.68501pt\hbox{\kern
3.00003pt$(\mathtt{r})$}}}\hbox{\kern 0.0pt\kern
10.60292pt\hbox{$\displaystyle\Gamma_{\mathtt{CC}}\wedge\Gamma_{u}\vdash\mathtt{CC}{[}\\!{[}[\alpha^{\prime}]tu{]}\\!{]}\langle\alpha/\\!\\!/\alpha^{\prime}.u\rangle:\mathcal{A}\mid(\Delta_{\mathtt{CC}};\alpha^{\prime}:\mathcal{V}_{\alpha^{\prime}})\vee\Delta_{u}\vee\alpha^{\prime}:\mathcal{V}$}}}}}$

where
$\mathcal{V}_{\alpha}=\langle\mathcal{I}_{\ell}\rightarrow{\mathcal{V}}_{\ell}\rangle_{{\ell\in
L}}$, $\mathcal{I}_{u}=(\wedge_{{\ell\in L}}\mathcal{I}_{\ell}^{*})^{*}$,
$\mathcal{V}=\vee_{{\ell\in L}}{\mathcal{V}}_{\ell}$,
$\Gamma=\Gamma_{\mathtt{CC}}\wedge\Gamma_{u}$ and
$\Delta=(\Delta_{\mathtt{CC}};\alpha^{\prime}:\mathcal{V}_{\alpha^{\prime}})\vee\Delta_{u}\vee\alpha^{\prime}:\mathcal{V}=(\Delta_{\mathtt{CC}}\vee\Delta_{u};\alpha^{\prime}:\mathcal{V}_{\alpha^{\prime}}\vee\mathcal{V})$
since $\alpha^{\prime}\notin\mathtt{fn}(u)$ implies
$\alpha^{\prime}\notin\mathtt{dom}(\Delta_{u})$. Since
$\alpha\in\mathtt{fn}(\mathtt{CC}{[}\\!{[}[\alpha^{\prime}]tu{]}\\!{]})$, then
$L\neq\emptyset$ by Lemma 22, so that $\mathcal{I}_{u}=\wedge_{{\ell\in
L}}\mathcal{I}_{\ell}^{*}$.

By Lemma 30 applied to $\Phi_{0}^{\prime}$, we have
$\Gamma_{0},\,\Delta_{0}^{\prime}$,$\,\Phi_{0},\,\mathcal{V}_{0},\,K\neq\emptyset,\,(\mathcal{I}_{k})_{{k\in
K}},\,(\mathcal{V}_{k})_{{k\in K}},\,\Gamma_{u}^{\prime},\Delta_{u}^{\prime}$,
and $\Theta_{u}^{\prime}$ such that

    * –

$\Gamma_{\mathtt{CC}}=\Gamma_{0}\wedge\Gamma_{u}^{\prime}$,

    * –

$\Delta_{\mathtt{CC}};\alpha:\mathcal{V}_{\alpha}=\Delta_{0}^{\prime}\vee\Delta_{u}^{\prime}$,

    * –

$\mathcal{V}_{\alpha^{\prime}}=\mathcal{V}_{0}\vee_{{k\in K}}\mathcal{V}_{k}$,

    * –

$\Phi_{0}\triangleright\Gamma_{0}\vdash\mathtt{CC}{[}\\!{[}[\alpha]t{]}\\!{]}:\mathcal{A}\mid\alpha^{\prime}:\mathcal{V}_{0};\alpha:\langle\mathcal{I}_{k}\rightarrow\mathcal{V}_{k}\rangle_{{k\in
K}}\vee\Delta_{0}^{\prime}$ and

    * –

$\triangleright\Gamma_{u}^{\prime}\Vdash u:\wedge_{{k\in
K}}\mathcal{I}_{k}^{*}\mid\Delta_{u}^{\prime}$

We set $L^{{}^{\prime\prime}}=L\uplus
K,\,\Gamma_{u}^{{}^{\prime\prime}}=\Gamma_{u}\wedge\Gamma_{u}^{\prime},\,\Delta_{u}^{{}^{\prime\prime}}=\Delta_{u}\vee\Delta_{u}^{\prime}$
and
$(\mathcal{I}_{u}^{{}^{\prime\prime}})^{*}=\mathcal{I}_{u}^{{}^{\prime\prime}}=\wedge_{{\ell\in
L}^{{}^{\prime\prime}}}\mathcal{I}_{\ell}^{*}$ (indeed,
$L^{{}^{\prime\prime}}\supseteq K\neq\emptyset$). By Lemma 22,
$\alpha\notin\mathtt{dom}(\Delta_{u}^{\prime})$, so that
$\Delta_{0}^{\prime}=\Delta_{0};\alpha:\mathcal{V}_{\alpha}$ for some
$\Delta_{0}$ and
$\alpha^{\prime}:\mathcal{V}_{0};\alpha:\langle\mathcal{I}_{k}\rightarrow\mathcal{V}_{k}\rangle_{{k\in
K}}\vee\Delta_{0}^{\prime}=\alpha^{\prime}:\mathcal{V}_{0};\alpha:\langle\mathcal{I}_{\ell}\rightarrow{\mathcal{V}}_{\ell}\rangle_{{\ell\in
L}^{{}^{\prime\prime}}};\Delta_{0}$ since
$\alpha^{\prime}\notin\mathtt{dom}(\Delta_{0}^{\prime})$. By Lemma 11, there
is
$\Theta_{u}^{{}^{\prime\prime}}\triangleright\Gamma_{u}^{{}^{\prime\prime}}\Vdash
u:\mathcal{I}_{u}^{{}^{\prime\prime}}\mid\Delta_{u}^{{}^{\prime\prime}}$. We
then construct the following derivation $\Phi$:

${{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1\Phi_{0}\triangleright\Gamma_{0}\vdash\mathtt{CC}{[}\\!{[}[\alpha]t{]}\\!{]}:\mathcal{A}\mid\alpha^{\prime}:\mathcal{V}_{0};\alpha:\langle\mathcal{I}_{k}\rightarrow\mathcal{V}_{k}\rangle_{{k\in
K}}\vee\Delta_{0}^{\prime}\quad\Theta_{u}^{{}^{\prime\prime}}\triangleright\Gamma_{u}^{{}^{\prime\prime}}\Vdash
u:\mathcal{I}_{u}^{{}^{\prime\prime}}\mid\Delta_{u}^{{}^{\prime\prime}}$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\hbox{\kern
0.0pt$$}\vrule height=0.25002pt,depth=0.25002pt,width=266.14365pt\hbox{\kern
3.00003pt$(\mathtt{r})$}}}\hbox{\kern 0.0pt\kern
23.74347pt\hbox{$\displaystyle\Gamma_{0}\wedge\Gamma_{u}^{{}^{\prime\prime}}\vdash\mathtt{CC}{[}\\!{[}[\alpha]t{]}\\!{]}\langle\alpha/\\!\\!/\alpha^{\prime}.u\rangle:\mathcal{A}\mid\alpha^{\prime}:\mathcal{V}_{0}\vee_{{\ell\in
L}^{{}^{\prime\prime}}}{\mathcal{V}}_{\ell};\Delta_{0}\vee\Delta_{u}^{{}^{\prime\prime}}$}}}}}$

We conclude since
$\Gamma_{0}\wedge\Gamma_{u}^{{}^{\prime\prime}}=\Gamma_{0}\wedge\Gamma_{u}^{\prime}\wedge\Gamma_{u}=\Gamma_{\mathtt{CC}}\wedge\Gamma_{u}=\Gamma$,
$\Delta_{0}\vee\Delta_{u}^{{}^{\prime\prime}}=\Delta_{0}\vee\Delta_{u}^{\prime}\vee\Delta_{u}=\Delta_{\mathtt{CC}}\vee\Delta_{u}$
and $\mathcal{V}_{0}\vee_{{\ell\in
L}^{{}^{\prime\prime}}}{\mathcal{V}}_{\ell}=\mathcal{V}_{0}\vee_{{k\in
K}}\mathcal{V}_{k}\vee_{{\ell\in
L}}{\mathcal{V}}_{\ell}=\mathcal{V}_{\alpha^{\prime}}\vee_{{\ell\in
L}}{\mathcal{V}}_{\ell}=\mathcal{V}_{\alpha^{\prime}}\vee\mathcal{V}$.

  * •

If
$o=\mathtt{CC}{[}\\!{[}[\alpha]t{]}\\!{]}\langle\alpha/\\!\\!/\alpha^{\prime}.u\rangle\rightarrow\mathtt{CC}{[}\\!{[}[\alpha^{\prime}]tu{]}\\!{]}=o^{\prime}$,
with $|\mathtt{CC}{[}\\!{[}[\alpha]t{]}\\!{]}|_{\alpha}=1$, then the
derivation $\Phi^{\prime}$ necessarily ends with the judgment
$\Gamma\vdash\mathtt{CC}{[}\\!{[}[\alpha^{\prime}]tu{]}\\!{]}:\mathcal{A}\mid\Delta_{\mathtt{CC}};\alpha^{\prime}:\mathcal{V}$,
where $\Delta=\Delta_{\mathtt{CC}};\alpha^{\prime}:\mathcal{V}$.

By Lemma 30 applied to $\Phi^{\prime}$, we have
$\Gamma_{0},\,\Delta_{0},\,\mathcal{V}_{0},\,K\neq\emptyset,\,(\mathcal{I}_{k})_{{k\in
K}},\,(\mathcal{V}_{k})_{{k\in K}},\,\Gamma_{u},\,\Delta_{u}$, and
$\Theta_{u}$ such that

    * –

$\Gamma=\Gamma_{0}\wedge\Gamma_{u}$,

    * –

$\Delta_{\mathtt{CC}}=\Delta_{0}\vee\Delta_{u}$,

    * –

$\mathcal{V}=\mathcal{V}_{0}\vee_{{k\in K}}\mathcal{V}_{k}$,

    * –

$\Phi_{0}\triangleright\Gamma_{0}\vdash\mathtt{CC}{[}\\!{[}[\alpha]t{]}\\!{]}:\mathcal{A}\mid\alpha^{\prime}:\mathcal{V}_{0};\alpha:\langle\mathcal{I}_{k}\rightarrow\mathcal{V}_{k}\rangle_{{k\in
K}}\vee\Delta_{0}$ and

    * –

$\Theta_{u}\triangleright\Gamma_{u}\Vdash u:\wedge_{{k\in
K}}\mathcal{I}_{k}^{*}\mid\Delta_{u}$

Notice that $K\neq\emptyset$ implies $(\wedge_{{k\in
K}}\mathcal{I}_{k}^{*})^{*}=\wedge_{{k\in K}}\mathcal{I}_{k}^{*}$. Moreover,
by Lemma 22, since
$\alpha\notin\mathtt{fn}(\mathtt{CC}{[}\\!{[}[\alpha^{\prime}]tu{]}\\!{]})$,
then $\alpha\notin\mathtt{dom}(\Delta)$, thus
$\alpha\notin\mathtt{dom}(\Delta_{0})$ and
$\alpha:\langle\mathcal{I}_{k}\rightarrow\mathcal{V}_{k}\rangle_{{k\in
K}}\vee\Delta_{0}=\alpha:\langle\mathcal{I}_{k}\rightarrow\mathcal{V}_{k}\rangle_{{k\in
K}};\Delta_{0}$. We then construct $\Phi$ :

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1\Phi_{0}\triangleright\Gamma_{0}\vdash\mathtt{CC}{[}\\!{[}[\alpha]t{]}\\!{]}:\mathcal{A}\mid\alpha^{\prime}:\mathcal{V}_{0};\alpha:\langle\mathcal{I}_{k}\rightarrow\mathcal{V}_{k}\rangle_{{k\in
K}}\vee\Delta_{0}\quad\Theta_{u}\triangleright\Gamma_{u}\Vdash u:\wedge_{{k\in
K}}\mathcal{I}_{k}^{*}\mid\Delta_{u}$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\hbox{\kern 0.0pt$$}\vrule
height=0.25002pt,depth=0.25002pt,width=284.67789pt\hbox{\kern
3.00003pt$(\mathtt{r})$}}}\hbox{\kern 0.0pt\kern
26.66516pt\hbox{$\displaystyle\Gamma\vdash\mathtt{CC}{[}\\!{[}[\alpha]t{]}\\!{]}\langle\alpha/\\!\\!/\alpha^{\prime}.u\rangle:\mathcal{A}\mid(\Delta_{0};\alpha^{\prime}:\mathcal{V}_{0})\vee\Delta_{u}\vee\alpha^{\prime}:\vee_{{k\in
K}}\mathcal{V}_{k}$}}}}$

We conclude since $\alpha^{\prime}\notin\mathtt{fn}(u)$ implies
$\alpha^{\prime}\notin\mathtt{dom}(\Delta_{u})$ by Lemma 22 so that
$(\Delta_{0};\alpha^{\prime}:\mathcal{V}_{0})\vee\Delta_{u}\vee\alpha^{\prime}:\vee_{{k\in
K}}\mathcal{V}_{k}=\Delta_{0}\vee\Delta_{u};\alpha^{\prime}:\mathcal{V}_{0}\vee_{{k\in
K}}\mathcal{V}_{k}=\Delta_{\mathtt{CC}};\alpha^{\prime}:\mathcal{V}=\Delta$ as
desired.