start(i) → busy(F, closed, stop, false, false, false, i)
busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrect
busy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correct
busy(S, closed, stop, false, false, false, empty) → correct
busy(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(B, open, stop, false, b2, b3, i) → idle(B, closed, stop, false, b2, b3, i)
busy(F, open, stop, b1, false, b3, i) → idle(F, closed, stop, b1, false, b3, i)
busy(S, open, stop, b1, b2, false, i) → idle(S, closed, stop, b1, b2, false, i)
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
or(true, b) → true
or(false, b) → b
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
start'(i) → busy'(F', closed', stop', false', false', false', i)
busy'(BF', d, stop', b1, b2, b3, i) → incorrect'
busy'(FS', d, stop', b1, b2, b3, i) → incorrect'
busy'(fl, open', up', b1, b2, b3, i) → incorrect'
busy'(fl, open', down', b1, b2, b3, i) → incorrect'
busy'(B', closed', stop', false', false', false', empty') → correct'
busy'(F', closed', stop', false', false', false', empty') → correct'
busy'(S', closed', stop', false', false', false', empty') → correct'
busy'(B', closed', stop', false', false', false', newbuttons'(i1, i2, i3, i)) → idle'(B', closed', stop', false', false', false', newbuttons'(i1, i2, i3, i))
busy'(F', closed', stop', false', false', false', newbuttons'(i1, i2, i3, i)) → idle'(F', closed', stop', false', false', false', newbuttons'(i1, i2, i3, i))
busy'(S', closed', stop', false', false', false', newbuttons'(i1, i2, i3, i)) → idle'(S', closed', stop', false', false', false', newbuttons'(i1, i2, i3, i))
busy'(B', open', stop', false', b2, b3, i) → idle'(B', closed', stop', false', b2, b3, i)
busy'(F', open', stop', b1, false', b3, i) → idle'(F', closed', stop', b1, false', b3, i)
busy'(S', open', stop', b1, b2, false', i) → idle'(S', closed', stop', b1, b2, false', i)
busy'(B', d, stop', true', b2, b3, i) → idle'(B', open', stop', false', b2, b3, i)
busy'(F', d, stop', b1, true', b3, i) → idle'(F', open', stop', b1, false', b3, i)
busy'(S', d, stop', b1, b2, true', i) → idle'(S', open', stop', b1, b2, false', i)
busy'(B', closed', down', b1, b2, b3, i) → idle'(B', closed', stop', b1, b2, b3, i)
busy'(S', closed', up', b1, b2, b3, i) → idle'(S', closed', stop', b1, b2, b3, i)
busy'(B', closed', up', true', b2, b3, i) → idle'(B', closed', stop', true', b2, b3, i)
busy'(F', closed', up', b1, true', b3, i) → idle'(F', closed', stop', b1, true', b3, i)
busy'(F', closed', down', b1, true', b3, i) → idle'(F', closed', stop', b1, true', b3, i)
busy'(S', closed', down', b1, b2, true', i) → idle'(S', closed', stop', b1, b2, true', i)
busy'(B', closed', up', false', b2, b3, i) → idle'(BF', closed', up', false', b2, b3, i)
busy'(F', closed', up', b1, false', b3, i) → idle'(FS', closed', up', b1, false', b3, i)
busy'(F', closed', down', b1, false', b3, i) → idle'(BF', closed', down', b1, false', b3, i)
busy'(S', closed', down', b1, b2, false', i) → idle'(FS', closed', down', b1, b2, false', i)
busy'(BF', closed', up', b1, b2, b3, i) → idle'(F', closed', up', b1, b2, b3, i)
busy'(BF', closed', down', b1, b2, b3, i) → idle'(B', closed', down', b1, b2, b3, i)
busy'(FS', closed', up', b1, b2, b3, i) → idle'(S', closed', up', b1, b2, b3, i)
busy'(FS', closed', down', b1, b2, b3, i) → idle'(F', closed', down', b1, b2, b3, i)
busy'(B', closed', stop', false', true', b3, i) → idle'(B', closed', up', false', true', b3, i)
busy'(B', closed', stop', false', false', true', i) → idle'(B', closed', up', false', false', true', i)
busy'(F', closed', stop', true', false', b3, i) → idle'(F', closed', down', true', false', b3, i)
busy'(F', closed', stop', false', false', true', i) → idle'(F', closed', up', false', false', true', i)
busy'(S', closed', stop', b1, true', false', i) → idle'(S', closed', down', b1, true', false', i)
busy'(S', closed', stop', true', false', false', i) → idle'(S', closed', down', true', false', false', i)
idle'(fl, d, m, b1, b2, b3, empty') → busy'(fl, d, m, b1, b2, b3, empty')
idle'(fl, d, m, b1, b2, b3, newbuttons'(i1, i2, i3, i)) → busy'(fl, d, m, or'(b1, i1), or'(b2, i2), or'(b3, i3), i)
or'(true', b) → true'
or'(false', b) → b
Infered types.
Rules:
start'(i) → busy'(F', closed', stop', false', false', false', i)
busy'(BF', d, stop', b1, b2, b3, i) → incorrect'
busy'(FS', d, stop', b1, b2, b3, i) → incorrect'
busy'(fl, open', up', b1, b2, b3, i) → incorrect'
busy'(fl, open', down', b1, b2, b3, i) → incorrect'
busy'(B', closed', stop', false', false', false', empty') → correct'
busy'(F', closed', stop', false', false', false', empty') → correct'
busy'(S', closed', stop', false', false', false', empty') → correct'
busy'(B', closed', stop', false', false', false', newbuttons'(i1, i2, i3, i)) → idle'(B', closed', stop', false', false', false', newbuttons'(i1, i2, i3, i))
busy'(F', closed', stop', false', false', false', newbuttons'(i1, i2, i3, i)) → idle'(F', closed', stop', false', false', false', newbuttons'(i1, i2, i3, i))
busy'(S', closed', stop', false', false', false', newbuttons'(i1, i2, i3, i)) → idle'(S', closed', stop', false', false', false', newbuttons'(i1, i2, i3, i))
busy'(B', open', stop', false', b2, b3, i) → idle'(B', closed', stop', false', b2, b3, i)
busy'(F', open', stop', b1, false', b3, i) → idle'(F', closed', stop', b1, false', b3, i)
busy'(S', open', stop', b1, b2, false', i) → idle'(S', closed', stop', b1, b2, false', i)
busy'(B', d, stop', true', b2, b3, i) → idle'(B', open', stop', false', b2, b3, i)
busy'(F', d, stop', b1, true', b3, i) → idle'(F', open', stop', b1, false', b3, i)
busy'(S', d, stop', b1, b2, true', i) → idle'(S', open', stop', b1, b2, false', i)
busy'(B', closed', down', b1, b2, b3, i) → idle'(B', closed', stop', b1, b2, b3, i)
busy'(S', closed', up', b1, b2, b3, i) → idle'(S', closed', stop', b1, b2, b3, i)
busy'(B', closed', up', true', b2, b3, i) → idle'(B', closed', stop', true', b2, b3, i)
busy'(F', closed', up', b1, true', b3, i) → idle'(F', closed', stop', b1, true', b3, i)
busy'(F', closed', down', b1, true', b3, i) → idle'(F', closed', stop', b1, true', b3, i)
busy'(S', closed', down', b1, b2, true', i) → idle'(S', closed', stop', b1, b2, true', i)
busy'(B', closed', up', false', b2, b3, i) → idle'(BF', closed', up', false', b2, b3, i)
busy'(F', closed', up', b1, false', b3, i) → idle'(FS', closed', up', b1, false', b3, i)
busy'(F', closed', down', b1, false', b3, i) → idle'(BF', closed', down', b1, false', b3, i)
busy'(S', closed', down', b1, b2, false', i) → idle'(FS', closed', down', b1, b2, false', i)
busy'(BF', closed', up', b1, b2, b3, i) → idle'(F', closed', up', b1, b2, b3, i)
busy'(BF', closed', down', b1, b2, b3, i) → idle'(B', closed', down', b1, b2, b3, i)
busy'(FS', closed', up', b1, b2, b3, i) → idle'(S', closed', up', b1, b2, b3, i)
busy'(FS', closed', down', b1, b2, b3, i) → idle'(F', closed', down', b1, b2, b3, i)
busy'(B', closed', stop', false', true', b3, i) → idle'(B', closed', up', false', true', b3, i)
busy'(B', closed', stop', false', false', true', i) → idle'(B', closed', up', false', false', true', i)
busy'(F', closed', stop', true', false', b3, i) → idle'(F', closed', down', true', false', b3, i)
busy'(F', closed', stop', false', false', true', i) → idle'(F', closed', up', false', false', true', i)
busy'(S', closed', stop', b1, true', false', i) → idle'(S', closed', down', b1, true', false', i)
busy'(S', closed', stop', true', false', false', i) → idle'(S', closed', down', true', false', false', i)
idle'(fl, d, m, b1, b2, b3, empty') → busy'(fl, d, m, b1, b2, b3, empty')
idle'(fl, d, m, b1, b2, b3, newbuttons'(i1, i2, i3, i)) → busy'(fl, d, m, or'(b1, i1), or'(b2, i2), or'(b3, i3), i)
or'(true', b) → true'
or'(false', b) → b
Types:
start' :: empty':newbuttons' → incorrect':correct'
busy' :: F':BF':FS':B':S' → closed':open' → stop':up':down' → false':true' → false':true' → false':true' → empty':newbuttons' → incorrect':correct'
F' :: F':BF':FS':B':S'
closed' :: closed':open'
stop' :: stop':up':down'
false' :: false':true'
BF' :: F':BF':FS':B':S'
incorrect' :: incorrect':correct'
FS' :: F':BF':FS':B':S'
open' :: closed':open'
up' :: stop':up':down'
down' :: stop':up':down'
B' :: F':BF':FS':B':S'
empty' :: empty':newbuttons'
correct' :: incorrect':correct'
S' :: F':BF':FS':B':S'
newbuttons' :: false':true' → false':true' → false':true' → empty':newbuttons' → empty':newbuttons'
idle' :: F':BF':FS':B':S' → closed':open' → stop':up':down' → false':true' → false':true' → false':true' → empty':newbuttons' → incorrect':correct'
true' :: false':true'
or' :: false':true' → false':true' → false':true'
_hole_incorrect':correct'1 :: incorrect':correct'
_hole_empty':newbuttons'2 :: empty':newbuttons'
_hole_F':BF':FS':B':S'3 :: F':BF':FS':B':S'
_hole_closed':open'4 :: closed':open'
_hole_stop':up':down'5 :: stop':up':down'
_hole_false':true'6 :: false':true'
_gen_empty':newbuttons'7 :: Nat → empty':newbuttons'
Heuristically decided to analyse the following defined symbols:
busy', idle'
They will be analysed ascendingly in the following order:
busy' = idle'
Rules:
start'(i) → busy'(F', closed', stop', false', false', false', i)
busy'(BF', d, stop', b1, b2, b3, i) → incorrect'
busy'(FS', d, stop', b1, b2, b3, i) → incorrect'
busy'(fl, open', up', b1, b2, b3, i) → incorrect'
busy'(fl, open', down', b1, b2, b3, i) → incorrect'
busy'(B', closed', stop', false', false', false', empty') → correct'
busy'(F', closed', stop', false', false', false', empty') → correct'
busy'(S', closed', stop', false', false', false', empty') → correct'
busy'(B', closed', stop', false', false', false', newbuttons'(i1, i2, i3, i)) → idle'(B', closed', stop', false', false', false', newbuttons'(i1, i2, i3, i))
busy'(F', closed', stop', false', false', false', newbuttons'(i1, i2, i3, i)) → idle'(F', closed', stop', false', false', false', newbuttons'(i1, i2, i3, i))
busy'(S', closed', stop', false', false', false', newbuttons'(i1, i2, i3, i)) → idle'(S', closed', stop', false', false', false', newbuttons'(i1, i2, i3, i))
busy'(B', open', stop', false', b2, b3, i) → idle'(B', closed', stop', false', b2, b3, i)
busy'(F', open', stop', b1, false', b3, i) → idle'(F', closed', stop', b1, false', b3, i)
busy'(S', open', stop', b1, b2, false', i) → idle'(S', closed', stop', b1, b2, false', i)
busy'(B', d, stop', true', b2, b3, i) → idle'(B', open', stop', false', b2, b3, i)
busy'(F', d, stop', b1, true', b3, i) → idle'(F', open', stop', b1, false', b3, i)
busy'(S', d, stop', b1, b2, true', i) → idle'(S', open', stop', b1, b2, false', i)
busy'(B', closed', down', b1, b2, b3, i) → idle'(B', closed', stop', b1, b2, b3, i)
busy'(S', closed', up', b1, b2, b3, i) → idle'(S', closed', stop', b1, b2, b3, i)
busy'(B', closed', up', true', b2, b3, i) → idle'(B', closed', stop', true', b2, b3, i)
busy'(F', closed', up', b1, true', b3, i) → idle'(F', closed', stop', b1, true', b3, i)
busy'(F', closed', down', b1, true', b3, i) → idle'(F', closed', stop', b1, true', b3, i)
busy'(S', closed', down', b1, b2, true', i) → idle'(S', closed', stop', b1, b2, true', i)
busy'(B', closed', up', false', b2, b3, i) → idle'(BF', closed', up', false', b2, b3, i)
busy'(F', closed', up', b1, false', b3, i) → idle'(FS', closed', up', b1, false', b3, i)
busy'(F', closed', down', b1, false', b3, i) → idle'(BF', closed', down', b1, false', b3, i)
busy'(S', closed', down', b1, b2, false', i) → idle'(FS', closed', down', b1, b2, false', i)
busy'(BF', closed', up', b1, b2, b3, i) → idle'(F', closed', up', b1, b2, b3, i)
busy'(BF', closed', down', b1, b2, b3, i) → idle'(B', closed', down', b1, b2, b3, i)
busy'(FS', closed', up', b1, b2, b3, i) → idle'(S', closed', up', b1, b2, b3, i)
busy'(FS', closed', down', b1, b2, b3, i) → idle'(F', closed', down', b1, b2, b3, i)
busy'(B', closed', stop', false', true', b3, i) → idle'(B', closed', up', false', true', b3, i)
busy'(B', closed', stop', false', false', true', i) → idle'(B', closed', up', false', false', true', i)
busy'(F', closed', stop', true', false', b3, i) → idle'(F', closed', down', true', false', b3, i)
busy'(F', closed', stop', false', false', true', i) → idle'(F', closed', up', false', false', true', i)
busy'(S', closed', stop', b1, true', false', i) → idle'(S', closed', down', b1, true', false', i)
busy'(S', closed', stop', true', false', false', i) → idle'(S', closed', down', true', false', false', i)
idle'(fl, d, m, b1, b2, b3, empty') → busy'(fl, d, m, b1, b2, b3, empty')
idle'(fl, d, m, b1, b2, b3, newbuttons'(i1, i2, i3, i)) → busy'(fl, d, m, or'(b1, i1), or'(b2, i2), or'(b3, i3), i)
or'(true', b) → true'
or'(false', b) → b
Types:
start' :: empty':newbuttons' → incorrect':correct'
busy' :: F':BF':FS':B':S' → closed':open' → stop':up':down' → false':true' → false':true' → false':true' → empty':newbuttons' → incorrect':correct'
F' :: F':BF':FS':B':S'
closed' :: closed':open'
stop' :: stop':up':down'
false' :: false':true'
BF' :: F':BF':FS':B':S'
incorrect' :: incorrect':correct'
FS' :: F':BF':FS':B':S'
open' :: closed':open'
up' :: stop':up':down'
down' :: stop':up':down'
B' :: F':BF':FS':B':S'
empty' :: empty':newbuttons'
correct' :: incorrect':correct'
S' :: F':BF':FS':B':S'
newbuttons' :: false':true' → false':true' → false':true' → empty':newbuttons' → empty':newbuttons'
idle' :: F':BF':FS':B':S' → closed':open' → stop':up':down' → false':true' → false':true' → false':true' → empty':newbuttons' → incorrect':correct'
true' :: false':true'
or' :: false':true' → false':true' → false':true'
_hole_incorrect':correct'1 :: incorrect':correct'
_hole_empty':newbuttons'2 :: empty':newbuttons'
_hole_F':BF':FS':B':S'3 :: F':BF':FS':B':S'
_hole_closed':open'4 :: closed':open'
_hole_stop':up':down'5 :: stop':up':down'
_hole_false':true'6 :: false':true'
_gen_empty':newbuttons'7 :: Nat → empty':newbuttons'
Generator Equations:
_gen_empty':newbuttons'7(0) ⇔ empty'
_gen_empty':newbuttons'7(+(x, 1)) ⇔ newbuttons'(false', false', false', _gen_empty':newbuttons'7(x))
The following defined symbols remain to be analysed:
idle', busy'
They will be analysed ascendingly in the following order:
busy' = idle'