相対性理論その1 - Maximaでこうぞうりきがく

CERNの長基線ニュートリノ振動実験でなにかと話題の相対性理論のお話です
内山龍雄訳・解説「相対性理論」（岩波文庫）117頁の解説をフォローします
内容はアインシュタインの最初の論文"Zur Elektrodynamik bewegter Körper"の運動学の部§2."長さと時間の相対性"になります
原論文の英訳がfourmilabにありますので参考まで
(入力行頭の式番号はテキストに合わせています)
special relativity1.wxm

c : 真空中の光の速度
v : K系とK'系との相対速度
%o1にて特定の'及び.を文字列として宣言します
%o2では数式内でのcとvの表記順序を指定します
K系の時計と時計Aのテンポを比較するためaという量を考えます(%o3)
K系の時刻が0のとき，Aの針も0となるので%o4式が成り立ちます
K'系から見たとき光がBに達した瞬間，時計AはA0A2の真ん中の点Mにいたので%o5式が成り立ちます
時計Aが点A1において示す時刻t'1と，Mにおける時刻(t'2)/2の間には%o6式が成り立ちます
ここで%o5式をt'2について解いた解を用いて%o6式を書き換えたものを%o7式として示します

K系の時間がt1だけ進む間に，光はc*t1進む（図4のA0Dに相当）ことから%o8式が成り立ちます
Bで反射された光については%o9式が成り立ちます
%o8，%o9式から%o10，%o11式が成り立ちます
%o10，%o11式それぞれの左辺・右辺同士を足し合わせると%o12式を得ます
これを書き直したものを%o13式として示します

A1における時計Aの示す時刻t'1は%o4式より%o14式で表されます
これを%o10式で書き直したものを%o15式として示します
同様に，Mにおける時計Aの時刻(t'2)/2は%o4式より%o16式で表されます
これを%o13式で書き直したものを%o17式として示します
既に%o5式で示したように，%o17式はB1において時計Bの示す時刻t'Bにも等しい
そこでA1Mの長さ（t'1-t'B）を%o5式で書き直したものを%o18式として示します
これに%o15，%o17式を代入すると%o19式を得ます