シグネチャのフィールドにある関係の多重度 続き

昨日の日記 の続き。 id:koji8y さんから、トラックバックで

じゃあ，昨日のスタート Alloy の演習中に僕らが表現したかったこと，

sig A {
	r: B -> C
}

で，各 A の各 r が one to one の関係 (functional かつ injective な関係) となること*1を表現するにはどう記述したらいいでしょうね?
（略）

sig A {
	r: B -> C
}{
	// functional (left-unique)
	all b: B, c1, c2: C {
		(b->c1 in r and b->c2 in r) => c1 = c2
	}
	// injective (right-unique)
	all b1, b2: B, c: C {
		(b1->c in r and b2->c in r) => b1 = b2
	}
}

とすると，表示したインスタンスは求めている形になっていそう．

でももっと簡単に記述できるるのではないかと...

と追加質問いただいたんですが…これって

  sig A {
    r: B lone -> lone C
  }

では？シグネチャファクト中の

  all b: B, c1, c2: C {
    (b->c1 in r and b->c2 in r) => c1 = c2
  }

って制約は

  all b: B {
    lone b.r
  }

と同じ意味に読めます。

実際、下記のように書いたアサーションで反例は（スコープをいくつにしても）出ないです。
（アサーションを記述するため、シグネチャファクトや宣言制約を述語内に書き下しています）

sig A {
	r: B -> C
}
sig B, C {}

pred p1 {
  all a: A {
	// functional (left-unique)
	all b: B, c1, c2: C {
		(b->c1 in a.r and b->c2 in a.r) => c1 = c2
	}
	// injective (right-unique)
	all b1, b2: B, c: C {
		(b1->c in a.r and b2->c in a.r) => b1 = b2
	}
  }
}

pred p2 {
  all a: A | a.r in B lone -> lone C
}

assert equivalence {
  p1 <=> p2
} 

check equivalence for 6