**************************************************
Claim
{ termination = Standard
, system = (VAR x1)
(RULES 0 q0 0 -> 0 0 q0 ,
0 q0 h -> 0 0 q0 h ,
1 q1 0 -> 1 0 q1 ,
1 q1 h -> 1 0 q1 h ,
1 q1 1 -> 1 1 q1 ,
0 q1 0 -> 0 0 q2 ,
0 q1 h -> 0 0 q2 h ,
0 q1 1 -> 0 1 q2 ,
1 q2 0 -> 1 0 q2 ,
1 q2 h -> 1 0 q2 h ,
1 q2 1 -> 1 1 q2 ,
0 q2 -> q3 1 ,
1 q3 -> q3 1 ,
0 q3 -> q4 0 ,
1 q4 -> q4 1 ,
0 q4 0 -> 1 0 q5 ,
0 q4 1 -> 1 1 q5 ,
1 q5 0 -> 0 0 q1 ,
1 q5 h -> 0 0 q1 h ,
1 q5 1 -> 0 1 q1 ,
h q3 -> h 0 q3 ,
h q4 -> h 0 q4)
, deadline = Just
(Time
-2040393102)
}
is false because of
mirror image
R' = { reverse(l) -> reverse(r) | (l -> r) in R }
(VAR x1)
(RULES 0 q0 0 -> q0 0 0 ,
h q0 0 -> h q0 0 0 ,
0 q1 1 -> q1 0 1 ,
h q1 1 -> h q1 0 1 ,
1 q1 1 -> q1 1 1 ,
0 q1 0 -> q2 0 0 ,
h q1 0 -> h q2 0 0 ,
1 q1 0 -> q2 1 0 ,
0 q2 1 -> q2 0 1 ,
h q2 1 -> h q2 0 1 ,
1 q2 1 -> q2 1 1 ,
q2 0 -> 1 q3 ,
q3 1 -> 1 q3 ,
q3 0 -> 0 q4 ,
q4 1 -> 1 q4 ,
0 q4 0 -> q5 0 1 ,
1 q4 0 -> q5 1 1 ,
0 q5 1 -> q1 0 0 ,
h q5 1 -> h q1 0 0 ,
1 q5 1 -> q1 1 0 ,
q3 h -> q3 0 h ,
q4 h -> q4 0 h)
looping forward closure
of length 1
Derivation
{ lhs = [ h , q0 , 0 ] , rhs = [ h , q0 , 0 , 0 ]
, hash_value = -1037175702 , strict = True
, steps = [ Step
{ rule = 1 , position = 0 }
]
}
this is closure number 14
MAYBE
**************************************************
summary
satisfy: no strategy annotation
satisfy: no theory annotation
satisfy: no relative rules
linear weights (from simplex method)
direct (half-strict semi-ring) matrix method
domain: Matrix.MaxPlus.MaxPlus, dimension: 2, unknowns <= 7, intermediates <= 15
direct (half-strict semi-ring) matrix method
domain: Matrix.MaxPlus.MaxPlus, dimension: 2, unknowns <= 7, intermediates <= 15
direct (half-strict semi-ring) matrix method
domain: Matrix.MaxPlus.MaxPlus, dimension: 2, unknowns <= 7, intermediates <= 15
direct (half-strict semi-ring) matrix method
domain: Matrix.MaxPlus.MaxPlus, dimension: 2, unknowns <= 7, intermediates <= 15
direct (half-strict semi-ring) matrix method
domain: Matrix.MaxPlus.MaxPlus, dimension: 2, unknowns <= 7, intermediates <= 15
direct (half-strict semi-ring) matrix method
domain: Matrix.MaxPlus.MaxPlus, dimension: 2, unknowns <= 7, intermediates <= 15
open: Standard termination
**************************************************
detail
Claim
{ termination = Standard
, system = (VAR x1)
(RULES 0 q0 0 -> 0 0 q0 ,
0 q0 h -> 0 0 q0 h ,
0 q0 1 -> 0 1 q0 ,
1 q0 0 -> 0 0 q1 ,
1 q0 h -> 0 0 q1 h ,
1 q0 1 -> 0 1 q1 ,
1 q1 0 -> 1 0 q1 ,
1 q1 h -> 1 0 q1 h ,
1 q1 1 -> 1 1 q1 ,
0 q1 0 -> 0 0 q2 ,
0 q1 h -> 0 0 q2 h ,
0 q1 1 -> 0 1 q2 ,
1 q2 0 -> 1 0 q2 ,
1 q2 h -> 1 0 q2 h ,
1 q2 1 -> 1 1 q2 ,
0 q2 -> q3 1 ,
1 q3 -> q3 1 ,
0 q3 -> q4 0 ,
1 q4 -> q4 1 ,
0 q4 0 -> 1 0 q5 ,
0 q4 h -> 1 0 q5 h ,
0 q4 1 -> 1 1 q5 ,
1 q5 0 -> 0 0 q1 ,
1 q5 h -> 0 0 q1 h ,
1 q5 1 -> 0 1 q1 ,
h q0 -> h 0 q0 ,
h q1 -> h 0 q1 ,
h q2 -> h 0 q2 ,
h q3 -> h 0 q3 ,
h q4 -> h 0 q4 ,
h q5 -> h 0 q5)
, deadline = Just
(Time
-2040389993)
}
follows by
satisfy: no strategy annotation
from
Claim
{ termination = Standard
, system = (VAR x1)
(RULES 0 q0 0 -> 0 0 q0 ,
0 q0 h -> 0 0 q0 h ,
0 q0 1 -> 0 1 q0 ,
1 q0 0 -> 0 0 q1 ,
1 q0 h -> 0 0 q1 h ,
1 q0 1 -> 0 1 q1 ,
1 q1 0 -> 1 0 q1 ,
1 q1 h -> 1 0 q1 h ,
1 q1 1 -> 1 1 q1 ,
0 q1 0 -> 0 0 q2 ,
0 q1 h -> 0 0 q2 h ,
0 q1 1 -> 0 1 q2 ,
1 q2 0 -> 1 0 q2 ,
1 q2 h -> 1 0 q2 h ,
1 q2 1 -> 1 1 q2 ,
0 q2 -> q3 1 ,
1 q3 -> q3 1 ,
0 q3 -> q4 0 ,
1 q4 -> q4 1 ,
0 q4 0 -> 1 0 q5 ,
0 q4 h -> 1 0 q5 h ,
0 q4 1 -> 1 1 q5 ,
1 q5 0 -> 0 0 q1 ,
1 q5 h -> 0 0 q1 h ,
1 q5 1 -> 0 1 q1 ,
h q0 -> h 0 q0 ,
h q1 -> h 0 q1 ,
h q2 -> h 0 q2 ,
h q3 -> h 0 q3 ,
h q4 -> h 0 q4 ,
h q5 -> h 0 q5)
, deadline = Just
(Time
-2040389993)
}
follows by
satisfy: no theory annotation
from
Claim
{ termination = Standard
, system = (VAR x1)
(RULES 0 q0 0 -> 0 0 q0 ,
0 q0 h -> 0 0 q0 h ,
0 q0 1 -> 0 1 q0 ,
1 q0 0 -> 0 0 q1 ,
1 q0 h -> 0 0 q1 h ,
1 q0 1 -> 0 1 q1 ,
1 q1 0 -> 1 0 q1 ,
1 q1 h -> 1 0 q1 h ,
1 q1 1 -> 1 1 q1 ,
0 q1 0 -> 0 0 q2 ,
0 q1 h -> 0 0 q2 h ,
0 q1 1 -> 0 1 q2 ,
1 q2 0 -> 1 0 q2 ,
1 q2 h -> 1 0 q2 h ,
1 q2 1 -> 1 1 q2 ,
0 q2 -> q3 1 ,
1 q3 -> q3 1 ,
0 q3 -> q4 0 ,
1 q4 -> q4 1 ,
0 q4 0 -> 1 0 q5 ,
0 q4 h -> 1 0 q5 h ,
0 q4 1 -> 1 1 q5 ,
1 q5 0 -> 0 0 q1 ,
1 q5 h -> 0 0 q1 h ,
1 q5 1 -> 0 1 q1 ,
h q0 -> h 0 q0 ,
h q1 -> h 0 q1 ,
h q2 -> h 0 q2 ,
h q3 -> h 0 q3 ,
h q4 -> h 0 q4 ,
h q5 -> h 0 q5)
, deadline = Just
(Time
-2040389993)
}
follows by
satisfy: no relative rules
from
Claim
{ termination = Standard
, system = (VAR x1)
(RULES 0 q0 0 -> 0 0 q0 ,
0 q0 h -> 0 0 q0 h ,
0 q0 1 -> 0 1 q0 ,
1 q0 0 -> 0 0 q1 ,
1 q0 h -> 0 0 q1 h ,
1 q0 1 -> 0 1 q1 ,
1 q1 0 -> 1 0 q1 ,
1 q1 h -> 1 0 q1 h ,
1 q1 1 -> 1 1 q1 ,
0 q1 0 -> 0 0 q2 ,
0 q1 h -> 0 0 q2 h ,
0 q1 1 -> 0 1 q2 ,
1 q2 0 -> 1 0 q2 ,
1 q2 h -> 1 0 q2 h ,
1 q2 1 -> 1 1 q2 ,
0 q2 -> q3 1 ,
1 q3 -> q3 1 ,
0 q3 -> q4 0 ,
1 q4 -> q4 1 ,
0 q4 0 -> 1 0 q5 ,
0 q4 h -> 1 0 q5 h ,
0 q4 1 -> 1 1 q5 ,
1 q5 0 -> 0 0 q1 ,
1 q5 h -> 0 0 q1 h ,
1 q5 1 -> 0 1 q1 ,
h q0 -> h 0 q0 ,
h q1 -> h 0 q1 ,
h q2 -> h 0 q2 ,
h q3 -> h 0 q3 ,
h q4 -> h 0 q4 ,
h q5 -> h 0 q5)
, deadline = Just
(Time
-2040389993)
}
follows by
linear interpretation (weights, rational numbers):
listToFM
[ ( 0 , 0 / 1 ) , ( 1 , 0 / 1 ) , ( h , 0 / 1 ) , ( q0 , 1 / 1 ) , ( q1 , 0 / 1 )
, ( q2 , 0 / 1 ) , ( q3 , 0 / 1 ) , ( q4 , 0 / 1 ) , ( q5 , 0 / 1 )
]
from
Claim
{ termination = Standard
, system = (VAR x1)
(RULES 0 q0 0 -> 0 0 q0 ,
0 q0 h -> 0 0 q0 h ,
0 q0 1 -> 0 1 q0 ,
1 q1 0 -> 1 0 q1 ,
1 q1 h -> 1 0 q1 h ,
1 q1 1 -> 1 1 q1 ,
0 q1 0 -> 0 0 q2 ,
0 q1 h -> 0 0 q2 h ,
0 q1 1 -> 0 1 q2 ,
1 q2 0 -> 1 0 q2 ,
1 q2 h -> 1 0 q2 h ,
1 q2 1 -> 1 1 q2 ,
0 q2 -> q3 1 ,
1 q3 -> q3 1 ,
0 q3 -> q4 0 ,
1 q4 -> q4 1 ,
0 q4 0 -> 1 0 q5 ,
0 q4 h -> 1 0 q5 h ,
0 q4 1 -> 1 1 q5 ,
1 q5 0 -> 0 0 q1 ,
1 q5 h -> 0 0 q1 h ,
1 q5 1 -> 0 1 q1 ,
h q0 -> h 0 q0 ,
h q1 -> h 0 q1 ,
h q2 -> h 0 q2 ,
h q3 -> h 0 q3 ,
h q4 -> h 0 q4 ,
h q5 -> h 0 q5)
, deadline = Just
(Time
-2040394987)
}
follows by
Matrix_Interpretation
{ dimension = 2 , domain = "Matrix.MaxPlus.MaxPlus"
, method = Method
{ select = mkSet [ 1 , 2 ] , letter_form = DR
, difference_form = Positive_Or_Both_Zero
}
, mapping = listToFM
[ ( 0
, Matrix ( 2 , 2 )
[ [ 0 , 0 ] , [ -inf , 0 ] ]
)
, ( 1
, Matrix ( 2 , 2 )
[ [ -inf , 0 ] , [ -inf , 0 ] ]
)
, ( h
, Matrix ( 2 , 2 )
[ [ 0 , 1 ] , [ -inf , 0 ] ]
)
, ( q0
, Matrix ( 2 , 2 )
[ [ 0 , 2 ] , [ -inf , 0 ] ]
)
, ( q1
, Matrix ( 2 , 2 )
[ [ -inf , 0 ] , [ -inf , 0 ] ]
)
, ( q2
, Matrix ( 2 , 2 )
[ [ -inf , -inf ] , [ -inf , 0 ] ]
)
, ( q3
, Matrix ( 2 , 2 )
[ [ 0 , 0 ] , [ 0 , 0 ] ]
)
, ( q4
, Matrix ( 2 , 2 )
[ [ -inf , 0 ] , [ 0 , 0 ] ]
)
, ( q5
, Matrix ( 2 , 2 )
[ [ 0 , 0 ] , [ -inf , 0 ] ]
)
]
}
from
Claim
{ termination = Standard
, system = (VAR x1)
(RULES 0 q0 0 -> 0 0 q0 ,
0 q0 h -> 0 0 q0 h ,
0 q0 1 -> 0 1 q0 ,
1 q1 0 -> 1 0 q1 ,
1 q1 h -> 1 0 q1 h ,
1 q1 1 -> 1 1 q1 ,
0 q1 0 -> 0 0 q2 ,
0 q1 h -> 0 0 q2 h ,
0 q1 1 -> 0 1 q2 ,
1 q2 0 -> 1 0 q2 ,
1 q2 h -> 1 0 q2 h ,
1 q2 1 -> 1 1 q2 ,
0 q2 -> q3 1 ,
1 q3 -> q3 1 ,
0 q3 -> q4 0 ,
1 q4 -> q4 1 ,
0 q4 0 -> 1 0 q5 ,
0 q4 1 -> 1 1 q5 ,
1 q5 0 -> 0 0 q1 ,
1 q5 h -> 0 0 q1 h ,
1 q5 1 -> 0 1 q1 ,
h q0 -> h 0 q0 ,
h q1 -> h 0 q1 ,
h q2 -> h 0 q2 ,
h q3 -> h 0 q3 ,
h q4 -> h 0 q4 ,
h q5 -> h 0 q5)
, deadline = Just
(Time
-2040394553)
}
follows by
Matrix_Interpretation
{ dimension = 2 , domain = "Matrix.MaxPlus.MaxPlus"
, method = Method
{ select = mkSet [ 1 , 2 ] , letter_form = DR
, difference_form = Positive_Or_Both_Zero
}
, mapping = listToFM
[ ( 0
, Matrix ( 2 , 2 )
[ [ -inf , 4 ] , [ -inf , 0 ] ]
)
, ( 1
, Matrix ( 2 , 2 )
[ [ 0 , -inf ] , [ -inf , 0 ] ]
)
, ( h
, Matrix ( 2 , 2 )
[ [ -inf , -inf ] , [ 4 , 0 ] ]
)
, ( q0
, Matrix ( 2 , 2 )
[ [ 6 , 4 ] , [ -inf , 0 ] ]
)
, ( q1
, Matrix ( 2 , 2 )
[ [ 0 , 4 ] , [ -inf , 0 ] ]
)
, ( q2
, Matrix ( 2 , 2 )
[ [ 0 , 5 ] , [ -inf , 0 ] ]
)
, ( q3
, Matrix ( 2 , 2 )
[ [ -inf , 4 ] , [ -inf , 0 ] ]
)
, ( q4
, Matrix ( 2 , 2 )
[ [ -inf , 4 ] , [ -inf , 0 ] ]
)
, ( q5
, Matrix ( 2 , 2 )
[ [ -inf , 4 ] , [ -inf , 0 ] ]
)
]
}
from
Claim
{ termination = Standard
, system = (VAR x1)
(RULES 0 q0 0 -> 0 0 q0 ,
0 q0 h -> 0 0 q0 h ,
0 q0 1 -> 0 1 q0 ,
1 q1 0 -> 1 0 q1 ,
1 q1 h -> 1 0 q1 h ,
1 q1 1 -> 1 1 q1 ,
0 q1 0 -> 0 0 q2 ,
0 q1 h -> 0 0 q2 h ,
0 q1 1 -> 0 1 q2 ,
1 q2 0 -> 1 0 q2 ,
1 q2 h -> 1 0 q2 h ,
1 q2 1 -> 1 1 q2 ,
0 q2 -> q3 1 ,
1 q3 -> q3 1 ,
0 q3 -> q4 0 ,
1 q4 -> q4 1 ,
0 q4 0 -> 1 0 q5 ,
0 q4 1 -> 1 1 q5 ,
1 q5 0 -> 0 0 q1 ,
1 q5 h -> 0 0 q1 h ,
1 q5 1 -> 0 1 q1 ,
h q0 -> h 0 q0 ,
h q1 -> h 0 q1 ,
h q3 -> h 0 q3 ,
h q4 -> h 0 q4 ,
h q5 -> h 0 q5)
, deadline = Just
(Time
-2040394178)
}
follows by
Matrix_Interpretation
{ dimension = 2 , domain = "Matrix.MaxPlus.MaxPlus"
, method = Method
{ select = mkSet [ 1 , 2 ] , letter_form = DR
, difference_form = Positive_Or_Both_Zero
}
, mapping = listToFM
[ ( 0
, Matrix ( 2 , 2 )
[ [ -inf , -inf ] , [ -inf , 0 ] ]
)
, ( 1
, Matrix ( 2 , 2 )
[ [ 0 , -inf ] , [ -inf , 0 ] ]
)
, ( h
, Matrix ( 2 , 2 )
[ [ 5 , 1 ] , [ 1 , 0 ] ]
)
, ( q0
, Matrix ( 2 , 2 )
[ [ 0 , 3 ] , [ -inf , 0 ] ]
)
, ( q1
, Matrix ( 2 , 2 )
[ [ 1 , 0 ] , [ -inf , 4 ] ]
)
, ( q2
, Matrix ( 2 , 2 )
[ [ 3 , -inf ] , [ -inf , 4 ] ]
)
, ( q3
, Matrix ( 2 , 2 )
[ [ -inf , -inf ] , [ -inf , 4 ] ]
)
, ( q4
, Matrix ( 2 , 2 )
[ [ -inf , -inf ] , [ 4 , 4 ] ]
)
, ( q5
, Matrix ( 2 , 2 )
[ [ -inf , -inf ] , [ -inf , 4 ] ]
)
]
}
from
Claim
{ termination = Standard
, system = (VAR x1)
(RULES 0 q0 0 -> 0 0 q0 ,
0 q0 h -> 0 0 q0 h ,
0 q0 1 -> 0 1 q0 ,
1 q1 0 -> 1 0 q1 ,
1 q1 h -> 1 0 q1 h ,
1 q1 1 -> 1 1 q1 ,
0 q1 0 -> 0 0 q2 ,
0 q1 h -> 0 0 q2 h ,
0 q1 1 -> 0 1 q2 ,
1 q2 0 -> 1 0 q2 ,
1 q2 h -> 1 0 q2 h ,
1 q2 1 -> 1 1 q2 ,
0 q2 -> q3 1 ,
1 q3 -> q3 1 ,
0 q3 -> q4 0 ,
1 q4 -> q4 1 ,
0 q4 0 -> 1 0 q5 ,
0 q4 1 -> 1 1 q5 ,
1 q5 0 -> 0 0 q1 ,
1 q5 h -> 0 0 q1 h ,
1 q5 1 -> 0 1 q1 ,
h q1 -> h 0 q1 ,
h q3 -> h 0 q3 ,
h q4 -> h 0 q4 ,
h q5 -> h 0 q5)
, deadline = Just
(Time
-2040393807)
}
follows by
Matrix_Interpretation
{ dimension = 2 , domain = "Matrix.MaxPlus.MaxPlus"
, method = Method
{ select = mkSet [ 1 , 2 ] , letter_form = DR
, difference_form = Positive_Or_Both_Zero
}
, mapping = listToFM
[ ( 0
, Matrix ( 2 , 2 )
[ [ -inf , -inf ] , [ 0 , 0 ] ]
)
, ( 1
, Matrix ( 2 , 2 )
[ [ -inf , -inf ] , [ -inf , 0 ] ]
)
, ( h
, Matrix ( 2 , 2 )
[ [ 2 , 0 ] , [ 2 , 0 ] ]
)
, ( q0
, Matrix ( 2 , 2 )
[ [ -inf , 0 ] , [ -inf , 0 ] ]
)
, ( q1
, Matrix ( 2 , 2 )
[ [ -inf , 0 ] , [ -inf , 0 ] ]
)
, ( q2
, Matrix ( 2 , 2 )
[ [ -inf , 0 ] , [ -inf , 0 ] ]
)
, ( q3
, Matrix ( 2 , 2 )
[ [ 4 , -inf ] , [ 0 , 0 ] ]
)
, ( q4
, Matrix ( 2 , 2 )
[ [ 0 , -inf ] , [ 0 , 0 ] ]
)
, ( q5
, Matrix ( 2 , 2 )
[ [ -inf , -inf ] , [ -inf , 0 ] ]
)
]
}
from
Claim
{ termination = Standard
, system = (VAR x1)
(RULES 0 q0 0 -> 0 0 q0 ,
0 q0 h -> 0 0 q0 h ,
0 q0 1 -> 0 1 q0 ,
1 q1 0 -> 1 0 q1 ,
1 q1 h -> 1 0 q1 h ,
1 q1 1 -> 1 1 q1 ,
0 q1 0 -> 0 0 q2 ,
0 q1 h -> 0 0 q2 h ,
0 q1 1 -> 0 1 q2 ,
1 q2 0 -> 1 0 q2 ,
1 q2 h -> 1 0 q2 h ,
1 q2 1 -> 1 1 q2 ,
0 q2 -> q3 1 ,
1 q3 -> q3 1 ,
0 q3 -> q4 0 ,
1 q4 -> q4 1 ,
0 q4 0 -> 1 0 q5 ,
0 q4 1 -> 1 1 q5 ,
1 q5 0 -> 0 0 q1 ,
1 q5 h -> 0 0 q1 h ,
1 q5 1 -> 0 1 q1 ,
h q3 -> h 0 q3 ,
h q4 -> h 0 q4 ,
h q5 -> h 0 q5)
, deadline = Just
(Time
-2040393447)
}
follows by
Matrix_Interpretation
{ dimension = 2 , domain = "Matrix.MaxPlus.MaxPlus"
, method = Method
{ select = mkSet [ 1 , 2 ] , letter_form = DR
, difference_form = Positive_Or_Both_Zero
}
, mapping = listToFM
[ ( 0
, Matrix ( 2 , 2 )
[ [ -inf , -inf ] , [ -inf , 0 ] ]
)
, ( 1
, Matrix ( 2 , 2 )
[ [ -inf , -inf ] , [ -inf , 0 ] ]
)
, ( h
, Matrix ( 2 , 2 )
[ [ 0 , 0 ] , [ 4 , 0 ] ]
)
, ( q0
, Matrix ( 2 , 2 )
[ [ 0 , 0 ] , [ -inf , 0 ] ]
)
, ( q1
, Matrix ( 2 , 2 )
[ [ 0 , 0 ] , [ -inf , 0 ] ]
)
, ( q2
, Matrix ( 2 , 2 )
[ [ 0 , 0 ] , [ -inf , 0 ] ]
)
, ( q3
, Matrix ( 2 , 2 )
[ [ 0 , -inf ] , [ 0 , 0 ] ]
)
, ( q4
, Matrix ( 2 , 2 )
[ [ 0 , -inf ] , [ 4 , 0 ] ]
)
, ( q5
, Matrix ( 2 , 2 )
[ [ -inf , 4 ] , [ -inf , 0 ] ]
)
]
}
from
Claim
{ termination = Standard
, system = (VAR x1)
(RULES 0 q0 0 -> 0 0 q0 ,
0 q0 h -> 0 0 q0 h ,
0 q0 1 -> 0 1 q0 ,
1 q1 0 -> 1 0 q1 ,
1 q1 h -> 1 0 q1 h ,
1 q1 1 -> 1 1 q1 ,
0 q1 0 -> 0 0 q2 ,
0 q1 h -> 0 0 q2 h ,
0 q1 1 -> 0 1 q2 ,
1 q2 0 -> 1 0 q2 ,
1 q2 h -> 1 0 q2 h ,
1 q2 1 -> 1 1 q2 ,
0 q2 -> q3 1 ,
1 q3 -> q3 1 ,
0 q3 -> q4 0 ,
1 q4 -> q4 1 ,
0 q4 0 -> 1 0 q5 ,
0 q4 1 -> 1 1 q5 ,
1 q5 0 -> 0 0 q1 ,
1 q5 h -> 0 0 q1 h ,
1 q5 1 -> 0 1 q1 ,
h q3 -> h 0 q3 ,
h q4 -> h 0 q4)
, deadline = Just
(Time
-2040393102)
}
follows by
Matrix_Interpretation
{ dimension = 2 , domain = "Matrix.MaxPlus.MaxPlus"
, method = Method
{ select = mkSet [ 1 , 2 ] , letter_form = DR
, difference_form = Positive_Or_Both_Zero
}
, mapping = listToFM
[ ( 0
, Matrix ( 2 , 2 )
[ [ 0 , 0 ] , [ 0 , 0 ] ]
)
, ( 1
, Matrix ( 2 , 2 )
[ [ -inf , 0 ] , [ -inf , 0 ] ]
)
, ( h
, Matrix ( 2 , 2 )
[ [ -inf , -inf ] , [ 0 , 0 ] ]
)
, ( q0
, Matrix ( 2 , 2 )
[ [ 2 , 0 ] , [ -inf , 0 ] ]
)
, ( q1
, Matrix ( 2 , 2 )
[ [ 0 , -inf ] , [ -inf , 0 ] ]
)
, ( q2
, Matrix ( 2 , 2 )
[ [ -inf , -inf ] , [ -inf , 0 ] ]
)
, ( q3
, Matrix ( 2 , 2 )
[ [ -inf , -inf ] , [ 0 , 0 ] ]
)
, ( q4
, Matrix ( 2 , 2 )
[ [ -inf , -inf ] , [ 0 , 0 ] ]
)
, ( q5
, Matrix ( 2 , 2 )
[ [ 0 , 0 ] , [ -inf , 0 ] ]
)
]
}
from
Open
(Claim
{ termination = Standard
, system = (VAR x1)
(RULES 0 q0 0 -> 0 0 q0 ,
0 q0 h -> 0 0 q0 h ,
1 q1 0 -> 1 0 q1 ,
1 q1 h -> 1 0 q1 h ,
1 q1 1 -> 1 1 q1 ,
0 q1 0 -> 0 0 q2 ,
0 q1 h -> 0 0 q2 h ,
0 q1 1 -> 0 1 q2 ,
1 q2 0 -> 1 0 q2 ,
1 q2 h -> 1 0 q2 h ,
1 q2 1 -> 1 1 q2 ,
0 q2 -> q3 1 ,
1 q3 -> q3 1 ,
0 q3 -> q4 0 ,
1 q4 -> q4 1 ,
0 q4 0 -> 1 0 q5 ,
0 q4 1 -> 1 1 q5 ,
1 q5 0 -> 0 0 q1 ,
1 q5 h -> 0 0 q1 h ,
1 q5 1 -> 0 1 q1 ,
h q3 -> h 0 q3 ,
h q4 -> h 0 q4)
, deadline = Just
(Time
-2040393102)
})
**************************************************
MAYBE
**************************************************
summary
satisfy: no strategy annotation
satisfy: no theory annotation
satisfy: no relative rules
linear weights (from simplex method)
direct (half-strict semi-ring) matrix method
domain: Matrix.MaxPlus.MaxPlus, dimension: 2, unknowns <= 7, intermediates <= 15
direct (half-strict semi-ring) matrix method
domain: Matrix.MaxPlus.MaxPlus, dimension: 2, unknowns <= 7, intermediates <= 15
direct (half-strict semi-ring) matrix method
domain: Matrix.MaxPlus.MaxPlus, dimension: 2, unknowns <= 7, intermediates <= 15
direct (half-strict semi-ring) matrix method
domain: Matrix.MaxPlus.MaxPlus, dimension: 2, unknowns <= 7, intermediates <= 15
direct (half-strict semi-ring) matrix method
domain: Matrix.MaxPlus.MaxPlus, dimension: 2, unknowns <= 7, intermediates <= 15
direct (half-strict semi-ring) matrix method
domain: Matrix.MaxPlus.MaxPlus, dimension: 2, unknowns <= 7, intermediates <= 15
open: Standard termination
**************************************************
**************************************************
statistics:
total atomic proof attempts
number = 33, total = 49
maximal = [ Log
{ what = direct (half-strict semi-ring) matrix method
domain: Matrix.MaxPlus.MaxPlus, dimension: 2, unknowns <= 7, intermediates <= 15
, start = Time
-2040393505
, end = Time
-2040392547
, duration = 9 , success = False
}
]
successful atomic proof attempts
number = 14, total = 21
maximal = [ Log
{ what = direct (half-strict semi-ring) matrix method
domain: Matrix.MaxPlus.MaxPlus, dimension: 2, unknowns <= 7, intermediates <= 15
, start = Time
-2040394101
, end = Time
-2040393509
, duration = 5 , success = True
}
, Log
{ what = direct (half-strict semi-ring) matrix method
domain: Matrix.MaxPlus.MaxPlus, dimension: 2, unknowns <= 7, intermediates <= 15
, start = Time
-2040395987
, end = Time
-2040395554
, duration = 4 , success = True
}
, Log
{ what = direct (half-strict semi-ring) matrix method
domain: Matrix.MaxPlus.MaxPlus, dimension: 2, unknowns <= 7, intermediates <= 15
, start = Time
-2040394447
, end = Time
-2040394102
, duration = 3 , success = True
}
, Log
{ what = direct (half-strict semi-ring) matrix method
domain: Matrix.MaxPlus.MaxPlus, dimension: 2, unknowns <= 7, intermediates <= 15
, start = Time
-2040395178
, end = Time
-2040394812
, duration = 3 , success = True
}
, Log
{ what = direct (half-strict semi-ring) matrix method
domain: Matrix.MaxPlus.MaxPlus, dimension: 2, unknowns <= 7, intermediates <= 15
, start = Time
-2040394807
, end = Time
-2040394452
, duration = 3 , success = True
}
, Log
{ what = direct (half-strict semi-ring) matrix method
domain: Matrix.MaxPlus.MaxPlus, dimension: 2, unknowns <= 7, intermediates <= 15
, start = Time
-2040395553
, end = Time
-2040395180
, duration = 3 , success = True
}
, Log
{ what = simplex
, start = Time
-2040392502
, end = Time
-2040392494
, duration = 0 , success = True
}
, Log
{ what = simplex
, start = Time
-2040392539
, end = Time
-2040392530
, duration = 0 , success = True
}
, Log
{ what = simplex
, start = Time
-2040392532
, end = Time
-2040392516
, duration = 0 , success = True
}
, Log
{ what = simplex
, start = Time
-2040392541
, end = Time
-2040392540
, duration = 0 , success = True
}
, Log
{ what = simplex
, start = Time
-2040392514
, end = Time
-2040392503
, duration = 0 , success = True
}
, Log
{ what = simplex
, start = Time
-2040392544
, end = Time
-2040392534
, duration = 0 , success = True
}
, Log
{ what = simplex
, start = Time
-2040395991
, end = Time
-2040395991
, duration = 0 , success = True
}
, Log
{ what = simplex
, start = Time
-2040392529
, end = Time
-2040392519
, duration = 0 , success = True
}
]
failed atomic proof attempts
number = 19, total = 28
maximal = [ Log
{ what = direct (half-strict semi-ring) matrix method
domain: Matrix.MaxPlus.MaxPlus, dimension: 2, unknowns <= 7, intermediates <= 15
, start = Time
-2040393505
, end = Time
-2040392547
, duration = 9 , success = False
}
]
**************************************************
matchbox general information (including details on proof methods):
http://dfa.imn.htwk-leipzig.de/matchbox/
this matchbox implementation uses the SAT solver
MiniSat by Niklas Een and Niklas Sörensson
http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
matchbox process information
arguments : --solver=/tmp/tmpongfjx/matchbox-2007-06-01/minisat --timeout-command=/tmp/tmpongfjx/matchbox-2007-06-01/timeout --tmpdir=tmp --timeout=60 /tmp/tmp.Vg3YzfYs9B/a.srs
started : Thu Jan 26 12:27:57 CET 2012
finished : Thu Jan 26 12:28:37 CET 2012
run system : Linux uc01-11 2.6.32-5-amd64 #1 SMP Wed Jan 12 03:40:32 UTC 2011 x86_64
release date : Fri Jun 1 17:36:44 CEST 2007
build date : Fri Jun 1 17:36:44 CEST 2007
build system : Linux dfa 2.6.8-2-k7 #1 Tue Aug 16 14:00:15 UTC 2005 i686 GNU/Linux
used clock time: 40 secs