spec.het revision b3bacd257ffcdd346b70ab690f03b28ad5f33fdc
7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maederlogic LF
7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maederspec SP1 =
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder o : type.
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder ded : o -> type.
7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maeder i : type.
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill Mossakowski p : o.
7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maeder q : o = p.
a0e24c863b78669b05797ff8ce635995a9bede44Christian Maeder f : i -> o.
08faa81d4dd8409cd923b334064f64f802ecc33dChristian Maeder
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder . ded q
08faa81d4dd8409cd923b334064f64f802ecc33dChristian Maederend
08faa81d4dd8409cd923b334064f64f802ecc33dChristian Maeder
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederspec SP2 =
08faa81d4dd8409cd923b334064f64f802ecc33dChristian Maeder o : type.
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder p : o.
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder a : o = p.
23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maeder q = p.
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederend
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder
f71a8dcf94fd9eb3c9800e16dcdc5e5ff74e5c22Christian Maederspec SP = SP1 and SP2
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederspec SP' = SP then
23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maeder b : o.
7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maeder
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder .ded b
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maederend
a0e24c863b78669b05797ff8ce635995a9bede44Christian Maeder
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederspec SP3 =
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maedernat : type.
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maedert : nat.
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederl : nat.
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederend
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder
a0e24c863b78669b05797ff8ce635995a9bede44Christian Maederspec SP4 =
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maedernat : type.
81946e2b3f6dde6167f48769bd02c7a634736856Christian MaederNat : type.
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maederp : nat.
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maederplus : nat -> nat -> nat.
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maederend
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder%view V1 : SP3 to SP4 = t |-> plus p p
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maederspec SP5 = SP hide p
a0e24c863b78669b05797ff8ce635995a9bede44Christian Maeder
a0e24c863b78669b05797ff8ce635995a9bede44Christian Maeder%spec SP6 = SP reveal i
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder