224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichlibrary IndexingExample
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichspec A =
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich sorts A,B,C < T
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich preds R1 : A * B;
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich R2 : B * C;
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich R3 : C * T
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichend
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichspec B =
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich sorts A,B,F,G < T
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich preds R1 : A * B;
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich R2 : B * G;
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich R3 : F * T
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichend
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichspec Combination =
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich A
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich with A |-> A[A]
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich and
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich B with A |-> A[B]
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichend