diff --git a/courseA/IM_Alloy.html b/courseA/IM_Alloy.html
index c39fa49..b26d31c 100644
--- a/courseA/IM_Alloy.html
+++ b/courseA/IM_Alloy.html
@@ -40,11 +40,13 @@
最初の述語として記述されている init は，Inventory の
インスタンスである its が初期化されていることを示しています．
次の itemRegistration は，itemId に対応する商品を登録する前の Inventory のインスタンス its と，
- 登録した後のインスタンス its' の関係を述語として定義しています．
- ここで quantity は初期数量，n は商品名を示しています．
+ 登録した後のインスタンス its' の関係を述語として定義しています．ここで quantity は初期数量，n は商品名を示しています．
+ また，述語定義中の some it: Item は，its のデータベースに登録されていない Item のインスタンス it が存在していることを示しており，
+ 直観的には Item のインスタンスの生成を示しています．
receivingOrShipping では itemId で登録されている商品に対して入荷か出荷を行った際の操作前の Inventory のインスタンス its と，
- 操作後のインスタンス its' の関係を述語として定義しています．
- ここで quantity が正の値のときは入荷，負の値のときは出荷を表しています．
+ 操作後のインスタンス its' の関係を述語として定義しています．ここで quantity が正の値のときは入荷，負の値のときは出荷を表しています．
+ また，述語定義中の some it': Item は，its のデータベースに登録されていない Item のインスタンス it' が存在していることを示しており，
+ 直観的には Item のインスタンスの生成を示しています．
最後の execute では，init ，itemRegistraction ，receivingOrShipping を
この順で呼び出す操作を定義しています．
run では，execute を呼び出して仮想実行を行います．
diff --git a/courseA/ST_Alloy.html b/courseA/ST_Alloy.html
index 3f2f446..118cb2a 100644
--- a/courseA/ST_Alloy.html
+++ b/courseA/ST_Alloy.html
@@ -29,7 +29,7 @@
Alloy では，アカウントidの集合を AccountId，アカウント名の集合を Name，
ツイートの集合を Tweet，アカウントデータベースの集合を Accounts，アカウントの集合を Account，ツイートリストの集合を List で表します．
以下のモデルでは sig を用いて，AccountId，Name，Tweet，Accounts，Account，List の順番にこれらの集合を宣言しています．
- Accounts には，AccountId から Account への対応関係がaccountDB フィールドとして定義されています．
+ Accounts には，AccountId から Account への対応関係が accountDB フィールドとして定義されています．
ここで，AccountId の右側の lone は１つの Account に対応する AccountId がたかだか１つしかないことを示しています．
Account の宣言では，アカウント名を表す name が Name のインスタンスとして，
ツイートリストを表す tweets が List のインスタンスとして定義されています．
@@ -42,12 +42,14 @@
最初の述語として記述されている init は，Accounts の
インスタンスである acs が初期化されていることを示しています．
次の signUp は，id に対応するアカウントを登録する前の Accounts のインスタンス acs と，
- 登録した後のインスタンス acs' の関係を述語として定義しています．
- ここで n はアカウント名を示しています．
+ 登録した後のインスタンス acs' の関係を述語として定義しています．ここで n はアカウント名を示しています．
+ また，述語定義中の some ac: Account は，acs のデータベースに登録されていない Account のインスタンス ac が存在していることを示しており，
+ 直観的には Account のインスタンスの生成を示しています．
tweet ではid で登録されているアカウントに対してツイートを行った際の操作前の Accounts のインスタンス acs と，
- 操作後のインスタンス acs' の関係を述語として定義しています．
- ここで contents はツイートの内容を表しています．
- また implies はその前に記述されている条件が成り立っているときは，その後に記述されている論理式または論理式の集合が成り立ち，条件が成り立っていないときは else の後ろに記述されている論理式または論理式の集合が成り立つことを示しています．
+ 操作後のインスタンス acs' の関係を述語として定義しています．ここで contents はツイートの内容を表しています．
+ 述語定義中の some ac': Account は，acs のデータベースに登録されていない Account のインスタンス ac' が存在していることを示しており，
+ 直観的には，Account のインスタンスが，ツイートを行うことによって複製されたことを示しています．
+ また implies は，その前に記述されている条件が成り立っているときは，その後に記述されている論理式または論理式の集合が成り立ち，条件が成り立っていないときは else の後ろに記述されている論理式または論理式の集合が成り立つことを示しています．
最後の execute では，init，signUp，tweet をこの順で呼び出す操作を定義しています．
run では，execute を呼び出して仮想実行を行います．
@@ -118,7 +120,7 @@
この図がモデルの実行に依らない，モデルそのものが持つ構造を表していることに注意して下さい．
Accounts が，AccountId のインスタンスを Account のインスタンスに対応させる accountDB というフィールドを持っており，
Account が Name のインスタンスを参照する name フィールドと，List のインスタンスを参照する tweets フィールドを，
- List が Int のインスタンスを参照する sizeフィールドと，
+ List が Int のインスタンスを参照する size フィールドと，
Int のインスタンスを Tweet のインスタンスに対応させる element フィールドをもっていることがわかります．