Case Analysis in CCRW, 2
Case Analysis in Circular Coinductive Rewriting, 2
Here we apply BOBJ's circular coinductive rewriting algorithm, with its new
feature for case analysis, to a real time asynchronous data transmission
protocol. The spec and the proof are both due to Profs. Futatsugi and Ogata
of JAIST (see Rewriting can verify distributed real-time systems - how to
verify in CafeOBJ, in Proc. Int. Workshop on Rewriting in Proof and
Computation, pp. 60-79, 2001). However the presentation of this proof is
much simplified by using BOBJ's case analysis features, including named case
declarations (so that they are first class citizens, that can be reused),
"multiplying" cases to form compound cases (the cartesian product of the cases
of the components), and excluding cases from a product (e.g., because they
cannot occur). These features were developed jointly by Joseph Goguen and Kai
Lin, and were implemented by Kai Lin.
1. BOBJ Source Code
<![CDATA[
dth BASIC-INT is
sorts Zero NzNat Nat NgInt NpInt Int .
subsort Zero NzNat < Nat .
subsort NgInt Zero < NpInt .
subsort NgInt Zero NpInt NzNat Nat < Int .
op 0 : -> Zero .
op s_ : Nat -> NzNat .
op p_ : NpInt -> NgInt .
op s_ : Int -> Int .
op p_ : Int -> Int .
var I : Int .
eq s p I = I .
eq p s I = I .
end
dth INT* is pr BASIC-INT .
op _+_ : Int Int -> Int [assoc comm].
vars I J : Int . var N : NzNat .
eq I + 0 = I .
eq I + s J = s(I + J) .
eq I + p J = p(I + J) .
op -_ : Int -> Int .
eq - 0 = 0 .
eq - (s I) = p (- I) .
eq - (p I) = s (- I) .
op _*_ : Int Int -> Int .
eq 0 * J = 0 .
eq (s I) * J = J + (I * J) .
eq (p I) * J = (- J) + (I * J) .
ops inc dec : Int -> Int .
eq inc(I) = s I .
eq dec(I) = p I .
op _<_ : Int Int -> Bool .
eq I < I + N = true .
end
dth LIST [X :: TRIV]is sort List .
op nil : -> List .
op _$_ : Elt List -> List .
op car_ : List -> Elt .
op cdr_ : List -> List .
var E : Elt . var L : List .
eq car (E $ L) = E .
eq cdr (E $ L) = L .
end
dth ILIST is pr LIST[INT*].
op 0 upto _ : Int -> List .
var N : NgInt . var M : Nat .
var I : Int . var L : List .
eq 0 upto N = nil .
eq 0 upto 0 = nil .
eq 0 upto (s M) = (M $ (0 upto M)) .
eq cdr (0 upto I) = 0 upto (p I) .
eq (s I) $ (0 upto I) = 0 upto (s I) .
eq I $ (0 upto p I) = 0 upto I .
op put : List Int -> List .
eq put(L, I) = I $ L .
end
th REAL+ is
sorts Real+ Timeval Timeval0 .
subsort Real+ Timeval < Timeval0 .
op 0 : -> Real+ .
op oo : -> Timeval .
op _+_ : Timeval0 Timeval0 -> Timeval0 [comm].
op _+_ : Real+ Real+ -> Real+ [comm].
op _+_ : Timeval Timeval -> Timeval [comm].
op _<=_ : Timeval0 Timeval0 -> Bool .
op _<_ : Timeval0 Timeval0 -> Bool .
vars T1 T2 T3 : Timeval0 .
eq T1 + T2 <= T1 + T3 = T2 <= T3 .
eq T1 + T2 < T1 + T3 = T2 < T3 .
end
***> distributed real-time asynchoronous data transmission protocol
bth ASEND is sort Sys .
protecting INT* + ILIST + REAL+ .
op init : -> Sys .
op empty : Sys -> Bool .
ops content data : Sys -> Nat .
op list : Sys -> List .
ops now l : Sys -> Real+ .
op u : Sys -> Timeval .
ops send rec : Sys -> Sys .
op tick : Sys Real+ -> Sys .
op d1 : -> Real+ . *** minimum delay for send
op d2 : -> Real+ . *** maximum delay for rec
eq d2 < d1 = true .
var T : Timeval0 . var S : Sys . var D : Real+ .
eq T < T + d1 = true .
eq empty(init) = true .
eq data(init) = 0 .
eq list(init) = nil .
eq now(init) = 0 .
eq l(init) = d1 .
eq u(init) = oo .
ceq empty(send(S)) = false if l(S) <= now(S) .
ceq empty(send(S)) = empty(S) if now(S) < l(S) .
ceq content(send(S)) = data(S) if l(S) <= now(S) .
ceq content(send(S)) = content(S) if now(S) < l(S) .
ceq data(send(S)) = inc(data(S)) if l(S) <= now(S) .
ceq data(send(S)) = data(S) if now(S) < l(S) .
eq list(send(S)) = list(S) .
eq now(send(S)) = now(S) .
ceq l(send(S)) = now(S) + d1 if l(S) <= now(S) .
ceq l(send(S)) = l(S) if now(S) < l(S) .
ceq u(send(S)) = now(S) + d2 if l(S) <= now(S) .
ceq u(send(S)) = u(S) if now(S) < l(S) .
ceq empty(rec(S)) = true if empty(S) == false .
ceq empty(rec(S)) = empty(S) if empty(S) == true .
eq content(rec(S)) = content(S) .
eq data(rec(S)) = data(S) .
ceq list(rec(S)) = put(list(S),content(S)) if empty(S) == false .
ceq list(rec(S)) = list(S) if empty(S) == true .
eq now(rec(S)) = now(S) .
eq l(rec(S)) = l(S) .
ceq u(rec(S)) = oo if empty(S) == false .
ceq u(rec(S)) = u(S) if empty(S) == true .
eq empty(tick(S,D)) = empty(S) .
eq content(tick(S,D)) = content(S) .
eq data(tick(S,D)) = data(S) .
eq list(tick(S,D)) = list(S) .
ceq now(tick(S,D)) = now(S) + D if now(S) + D <= u(S) .
ceq now(tick(S,D)) = now(S) if u(S) < now(S) + D .
eq l(tick(S,D)) = l(S) .
eq u(tick(S,D)) = u(S) .
end
dth INV is protecting ASEND .
*** inv1 is the property we want to prove about the spec ASEND
op inv1 : Sys -> Bool .
var S : Sys .
eq inv1(S) =
(empty(S) implies (list(S) == 0 upto dec(data(S)))) and
(not(empty(S)) implies (list(S) == 0 upto dec(dec(data(S))))) .
op inv2 : Sys -> Bool .
eq inv2(S) = empty(S) or (now(S) < l(S)) .
op inv3 : Sys -> Bool .
eq inv3(S) = (u(S) < l(S)) or empty(S) .
op inv4 : Sys -> Bool .
eq inv4(S) = (content(S) == dec(data(S))) or empty(S) .
end
***> induction base:
***> inv1(init), inv2(init), inv3(init), inv4(init) hold
open INV .
red inv1(init) .
red inv2(init) .
red inv3(init) .
red inv4(init) .
close
dth BASE is protecting INV .
op s : -> Sys .
var D : Real+ .
end
cases C1 for BASE is context s .
case eq empty(s) = true .
case eq empty(s) = false .
end
cases C2 for BASE is context s .
case eq now(s) < l(s) = true .
case eq l(s) <= now(s) = true .
end
cases C3 for BASE is
var D : Real+ .
context tick(s, D) .
case eq now(s) + D <= u(s) = true .
case eq u(s) < now(s) + D = true .
end
***> ==== proof score for inv3 and inv4 =======
*** module for induction BASE for inv3 and inv4
dth BASE3and4 is protecting BASE .
*** inv3
ceq u(s) < l(s) = true if not(empty(s)) .
*** inv4
ceq content(s) = dec(data(s)) if not(empty(s)) .
end
open BASE3and4 .
use C1 * C2 .
cred inv3(send(s)) == true .
cred inv4(send(s)) == true .
cred inv3(rec(s)) == true .
cred inv4(rec(s)) == true .
op d : -> Real+ .
cred inv3(tick(s,d)) == true .
cred inv4(tick(s,d)) == true .
close
***> ==== proof score for inv2 =======
dth BASE2 is protecting BASE .
*** lemmata inv3 and inv4 are already proved
var S : Sys . var D : Timeval0 .
ceq (u(S) < l(S)) = true if not(empty(S)) .
ceq content(S) = dec(data(S)) if not(empty(S)) .
*** necessary proposition: validity is trivial
ceq ((now(S) + D) < l(S)) = true if
((now(S) + D) <= u(S)) and (u(S) < l(S)) .
*** inv2
ceq (now(s) < l(s)) = true if not(empty(s)) .
end
open BASE2 .
use C1 * C2 .
cred inv2(send(s)) == true .
cred inv2(rec(s)) == true .
op d : -> Real+ .
cred with C3 * C1 * C2 inv2(tick(s,d)) == true .
close
***> ==== proof score for inv1 =======
dth BASE1 is protecting BASE .
var S : Sys .
ceq (now(S) < l(S)) = true if not(empty(S)) .
ceq (u(S) < l(S)) = true if not(empty(S)) .
ceq content(S) = dec(data(S)) if not(empty(S)) .
*** inv1: the property to be proved
ceq list(s) = (0 upto dec(data(s))) if empty(s) .
ceq list(s) = (0 upto dec(dec(data(s)))) if not(empty(s)) .
end
open BASE1 .
cred with C1 * C2 exclude (2,2) inv1(send(s)) == true .
cred with C1 inv1(rec(s)) == true .
op d : -> Real+ .
cred with C1 inv1(tick(s, d)) == true .
close
]]>
2. BOBJ Output with Full Trace Off
We first give the output with full trace off, which is much more compact,
though less informative, than the output with full trace on, as shown in the
next section below.
<![CDATA[
awk% bobj
\|||||||||||||||||/
--- Welcome to BOBJ ---
/|||||||||||||||||\
BOBJ version 0.9.146 built: Mon Jan 7 18:30:55 PST 2002
University of California, San Diego
Tue Jan 08 13:14:43 PST 2002
BOBJ> in realcase
==========================================
dth BASIC-INT
==========================================
dth INT*
==========================================
dth LIST
==========================================
dth ILIST
==========================================
th REAL+
==========================================
***> distributed real-time asynchoronous data transmission protocol
==========================================
bth ASEND
==========================================
dth INV
==========================================
***> induction base:
==========================================
***> inv1(init), inv2(init), inv3(init), inv4(init) hold
==========================================
open INV
==========================================
reduce in INV : inv1(init)
result Bool: true
rewrite time: 144ms parse time: 1ms
==========================================
reduce in INV : inv2(init)
result Bool: true
rewrite time: 2ms parse time: 2ms
==========================================
reduce in INV : inv3(init)
result Bool: true
rewrite time: 22ms parse time: 1ms
==========================================
reduce in INV : inv4(init)
result Bool: true
rewrite time: 3ms parse time: 1ms
==========================================
close
==========================================
dth BASE
==========================================
cases C1
==========================================
cases C2
==========================================
cases C3
==========================================
***> ==== proof score for inv3 and inv4 =======
==========================================
dth BASE3and4
==========================================
open BASE3and4
==========================================
use C1 * C2
==========================================
c-reduce in BASE3and4 : inv3(send(s)) == true
result: true
c-rewrite time: 85ms parse time: 11ms
==========================================
c-reduce in BASE3and4 : inv4(send(s)) == true
result: true
c-rewrite time: 57ms parse time: 3ms
==========================================
c-reduce in BASE3and4 : inv3(rec(s)) == true
result: true
c-rewrite time: 46ms parse time: 4ms
==========================================
c-reduce in BASE3and4 : inv4(rec(s)) == true
result: true
c-rewrite time: 42ms parse time: 3ms
==========================================
op d : -> Real+
==========================================
c-reduce in BASE3and4 : inv3(tick(s, d)) == true
result: true
c-rewrite time: 44ms parse time: 4ms
==========================================
c-reduce in BASE3and4 : inv4(tick(s, d)) == true
result: true
c-rewrite time: 39ms parse time: 4ms
==========================================
close
==========================================
***> ==== proof score for inv2 =======
==========================================
dth BASE2
==========================================
open BASE2
==========================================
use C1 * C2
==========================================
c-reduce in BASE2 : inv2(send(s)) == true
result: true
c-rewrite time: 46ms parse time: 3ms
==========================================
c-reduce in BASE2 : inv2(rec(s)) == true
result: true
c-rewrite time: 32ms parse time: 3ms
==========================================
op d : -> Real+
==========================================
c-reduce in BASE2 : inv2(tick(s, d)) == true
use: C3 * C1 * C2
result: true
c-rewrite time: 87ms parse time: 4ms
==========================================
close
==========================================
***> ==== proof score for inv1 =======
==========================================
dth BASE1
==========================================
open BASE1
==========================================
c-reduce in BASE1 : inv1(send(s)) == true
use: C1 * C2 exclude (2,2)
result: true
c-rewrite time: 99ms parse time: 3ms
==========================================
c-reduce in BASE1 : inv1(rec(s)) == true
use: C1
result: true
c-rewrite time: 81ms parse time: 4ms
==========================================
op d : -> Real+
==========================================
c-reduce in BASE1 : inv1(tick(s, d)) == true
use: C1
result: true
c-rewrite time: 69ms parse time: 4ms
==========================================
close
BOBJ> q
Bye.
]]>
3. BOBJ Output with Full Trace On
We next give the output with full trace on, which shows many more details
about the computations that are performed.
<![CDATA[
awk% bobj
\|||||||||||||||||/
--- Welcome to BOBJ ---
/|||||||||||||||||\
BOBJ version 0.9.146 built: Mon Jan 7 18:30:55 PST 2002
University of California, San Diego
Tue Jan 08 13:14:56 PST 2002
BOBJ> set full trace on .
BOBJ> in realcase
==========================================
dth BASIC-INT
==========================================
dth INT*
==========================================
dth LIST
==========================================
dth ILIST
==========================================
th REAL+
==========================================
***> distributed real-time asynchoronous data transmission protocol
==========================================
bth ASEND
==========================================
dth INV
==========================================
***> induction base:
==========================================
***> inv1(init), inv2(init), inv3(init), inv4(init) hold
==========================================
open INV
==========================================
reduce in INV : inv1(init)
result Bool: true
rewrite time: 158ms parse time: 1ms
==========================================
reduce in INV : inv2(init)
result Bool: true
rewrite time: 2ms parse time: 2ms
==========================================
reduce in INV : inv3(init)
result Bool: true
rewrite time: 22ms parse time: 1ms
==========================================
reduce in INV : inv4(init)
result Bool: true
rewrite time: 4ms parse time: 2ms
==========================================
close
==========================================
dth BASE
==========================================
cases C1
==========================================
cases C2
==========================================
cases C3
==========================================
***> ==== proof score for inv3 and inv4 =======
==========================================
dth BASE3and4
==========================================
open BASE3and4
==========================================
use C1 * C2
==========================================
c-reduce in BASE3and4 : inv3(send(s)) == true
-------------------------------------------
case analyse by C1 * C2
-------------------------------------------
case (1,1) :
assume: empty(s) = true
now(s) < l(s) = true
reduce: inv3(send(s)) == true
nf: true
-------------------------------
case (1,2) :
assume: empty(s) = true
l(s) <= now(s) = true
reduce: inv3(send(s)) == true
nf: true
-------------------------------
case (2,1) :
assume: empty(s) = false
now(s) < l(s) = true
reduce: inv3(send(s)) == true
nf: true
-------------------------------
case (2,2) :
assume: empty(s) = false
l(s) <= now(s) = true
reduce: inv3(send(s)) == true
nf: true
-------------------------------
result: true
c-rewrite time: 101ms parse time: 11ms
==========================================
c-reduce in BASE3and4 : inv4(send(s)) == true
-------------------------------------------
case analyse by C1 * C2
-------------------------------------------
case (1,1) :
assume: empty(s) = true
now(s) < l(s) = true
reduce: inv4(send(s)) == true
nf: true
-------------------------------
case (1,2) :
assume: empty(s) = true
l(s) <= now(s) = true
reduce: inv4(send(s)) == true
nf: true
-------------------------------
case (2,1) :
assume: empty(s) = false
now(s) < l(s) = true
reduce: inv4(send(s)) == true
nf: true
-------------------------------
case (2,2) :
assume: empty(s) = false
l(s) <= now(s) = true
reduce: inv4(send(s)) == true
nf: true
-------------------------------
result: true
c-rewrite time: 63ms parse time: 3ms
==========================================
c-reduce in BASE3and4 : inv3(rec(s)) == true
-------------------------------------------
case analyse by C1 * C2
-------------------------------------------
case (1,1) :
assume: empty(s) = true
now(s) < l(s) = true
reduce: inv3(rec(s)) == true
nf: true
-------------------------------
case (1,2) :
assume: empty(s) = true
l(s) <= now(s) = true
reduce: inv3(rec(s)) == true
nf: true
-------------------------------
case (2,1) :
assume: empty(s) = false
now(s) < l(s) = true
reduce: inv3(rec(s)) == true
nf: true
-------------------------------
case (2,2) :
assume: empty(s) = false
l(s) <= now(s) = true
reduce: inv3(rec(s)) == true
nf: true
-------------------------------
result: true
c-rewrite time: 59ms parse time: 3ms
==========================================
c-reduce in BASE3and4 : inv4(rec(s)) == true
-------------------------------------------
case analyse by C1 * C2
-------------------------------------------
case (1,1) :
assume: empty(s) = true
now(s) < l(s) = true
reduce: inv4(rec(s)) == true
nf: true
-------------------------------
case (1,2) :
assume: empty(s) = true
l(s) <= now(s) = true
reduce: inv4(rec(s)) == true
nf: true
-------------------------------
case (2,1) :
assume: empty(s) = false
now(s) < l(s) = true
reduce: inv4(rec(s)) == true
nf: true
-------------------------------
case (2,2) :
assume: empty(s) = false
l(s) <= now(s) = true
reduce: inv4(rec(s)) == true
nf: true
-------------------------------
result: true
c-rewrite time: 54ms parse time: 3ms
==========================================
op d : -> Real+
==========================================
c-reduce in BASE3and4 : inv3(tick(s, d)) == true
-------------------------------------------
case analyse by C1 * C2
-------------------------------------------
case (1,1) :
assume: empty(s) = true
now(s) < l(s) = true
reduce: inv3(tick(s, d)) == true
nf: true
-------------------------------
case (1,2) :
assume: empty(s) = true
l(s) <= now(s) = true
reduce: inv3(tick(s, d)) == true
nf: true
-------------------------------
case (2,1) :
assume: empty(s) = false
now(s) < l(s) = true
reduce: inv3(tick(s, d)) == true
nf: true
-------------------------------
case (2,2) :
assume: empty(s) = false
l(s) <= now(s) = true
reduce: inv3(tick(s, d)) == true
nf: true
-------------------------------
result: true
c-rewrite time: 58ms parse time: 3ms
==========================================
c-reduce in BASE3and4 : inv4(tick(s, d)) == true
-------------------------------------------
case analyse by C1 * C2
-------------------------------------------
case (1,1) :
assume: empty(s) = true
now(s) < l(s) = true
reduce: inv4(tick(s, d)) == true
nf: true
-------------------------------
case (1,2) :
assume: empty(s) = true
l(s) <= now(s) = true
reduce: inv4(tick(s, d)) == true
nf: true
-------------------------------
case (2,1) :
assume: empty(s) = false
now(s) < l(s) = true
reduce: inv4(tick(s, d)) == true
nf: true
-------------------------------
case (2,2) :
assume: empty(s) = false
l(s) <= now(s) = true
reduce: inv4(tick(s, d)) == true
nf: true
-------------------------------
result: true
c-rewrite time: 53ms parse time: 4ms
==========================================
close
==========================================
***> ==== proof score for inv2 =======
==========================================
dth BASE2
==========================================
open BASE2
==========================================
use C1 * C2
==========================================
c-reduce in BASE2 : inv2(send(s)) == true
-------------------------------------------
case analyse by C1 * C2
-------------------------------------------
case (1,1) :
assume: empty(s) = true
now(s) < l(s) = true
reduce: inv2(send(s)) == true
nf: true
-------------------------------
case (1,2) :
assume: empty(s) = true
l(s) <= now(s) = true
reduce: inv2(send(s)) == true
nf: true
-------------------------------
case (2,1) :
assume: empty(s) = false
now(s) < l(s) = true
reduce: inv2(send(s)) == true
nf: true
-------------------------------
case (2,2) :
assume: empty(s) = false
l(s) <= now(s) = true
reduce: inv2(send(s)) == true
nf: true
-------------------------------
result: true
c-rewrite time: 64ms parse time: 3ms
==========================================
c-reduce in BASE2 : inv2(rec(s)) == true
-------------------------------------------
case analyse by C1 * C2
-------------------------------------------
case (1,1) :
assume: empty(s) = true
now(s) < l(s) = true
reduce: inv2(rec(s)) == true
nf: true
-------------------------------
case (1,2) :
assume: empty(s) = true
l(s) <= now(s) = true
reduce: inv2(rec(s)) == true
nf: true
-------------------------------
case (2,1) :
assume: empty(s) = false
now(s) < l(s) = true
reduce: inv2(rec(s)) == true
nf: true
-------------------------------
case (2,2) :
assume: empty(s) = false
l(s) <= now(s) = true
reduce: inv2(rec(s)) == true
nf: true
-------------------------------
result: true
c-rewrite time: 45ms parse time: 3ms
==========================================
op d : -> Real+
==========================================
c-reduce in BASE2 : inv2(tick(s, d)) == true
use: C3 * C1 * C2
-------------------------------------------
case analyse by C3 * C1 * C2
-------------------------------------------
case (1,1,1) :
assume: (now(s) + d) <= u(s) = true
empty(s) = true
now(s) < l(s) = true
reduce: inv2(tick(s, d)) == true
nf: true
-------------------------------
case (1,1,2) :
assume: (now(s) + d) <= u(s) = true
empty(s) = true
l(s) <= now(s) = true
reduce: inv2(tick(s, d)) == true
nf: true
-------------------------------
case (1,2,1) :
assume: (now(s) + d) <= u(s) = true
empty(s) = false
now(s) < l(s) = true
reduce: inv2(tick(s, d)) == true
nf: true
-------------------------------
case (1,2,2) :
assume: (now(s) + d) <= u(s) = true
empty(s) = false
l(s) <= now(s) = true
reduce: inv2(tick(s, d)) == true
nf: true
-------------------------------
case (2,1,1) :
assume: u(s) < (now(s) + d) = true
empty(s) = true
now(s) < l(s) = true
reduce: inv2(tick(s, d)) == true
nf: true
-------------------------------
case (2,1,2) :
assume: u(s) < (now(s) + d) = true
empty(s) = true
l(s) <= now(s) = true
reduce: inv2(tick(s, d)) == true
nf: true
-------------------------------
case (2,2,1) :
assume: u(s) < (now(s) + d) = true
empty(s) = false
now(s) < l(s) = true
reduce: inv2(tick(s, d)) == true
nf: true
-------------------------------
case (2,2,2) :
assume: u(s) < (now(s) + d) = true
empty(s) = false
l(s) <= now(s) = true
reduce: inv2(tick(s, d)) == true
nf: true
-------------------------------
result: true
c-rewrite time: 104ms parse time: 4ms
==========================================
close
==========================================
***> ==== proof score for inv1 =======
==========================================
dth BASE1
==========================================
open BASE1
==========================================
c-reduce in BASE1 : inv1(send(s)) == true
use: C1 * C2 exclude (2,2)
-------------------------------------------
case analyse by C1 * C2 exclude (2,2)
-------------------------------------------
case (1,1) :
assume: empty(s) = true
now(s) < l(s) = true
reduce: inv1(send(s)) == true
nf: true
-------------------------------
case (1,2) :
assume: empty(s) = true
l(s) <= now(s) = true
reduce: inv1(send(s)) == true
nf: true
-------------------------------
case (2,1) :
assume: empty(s) = false
now(s) < l(s) = true
reduce: inv1(send(s)) == true
nf: true
-------------------------------
result: true
c-rewrite time: 117ms parse time: 3ms
==========================================
c-reduce in BASE1 : inv1(rec(s)) == true
use: C1
-------------------------------------------
case analyse by C1
-------------------------------------------
case 1 :
assume: empty(s) = true
reduce: inv1(rec(s)) == true
nf: true
-------------------------------
case 2 :
assume: empty(s) = false
reduce: inv1(rec(s)) == true
nf: true
-------------------------------
result: true
c-rewrite time: 74ms parse time: 3ms
==========================================
op d : -> Real+
==========================================
c-reduce in BASE1 : inv1(tick(s, d)) == true
use: C1
-------------------------------------------
case analyse by C1
-------------------------------------------
case 1 :
assume: empty(s) = true
reduce: inv1(tick(s, d)) == true
nf: true
-------------------------------
case 2 :
assume: empty(s) = false
reduce: inv1(tick(s, d)) == true
nf: true
-------------------------------
result: true
c-rewrite time: 82ms parse time: 4ms
==========================================
close
BOBJ> q
Bye.
awk%
]]>
To the BOBJ Examples homepage
To the Tatami project homepage
Maintained by Joseph Goguen
Last modified: Fri Jan 10 12:59:03 PST 2003