changeset 1673 | d22110ddd0af |
parent 1669 | e56cdf711729 |
child 1678 | 8aff580dce44 |
1672:2c109cd2fdd0 | 1673:d22110ddd0af |
---|---|
1 open I; |
1 open I; |
2 |
|
3 Unify.trace_bound := 45; |
|
4 Unify.search_bound := 50; |
|
2 |
5 |
3 goal thy |
6 goal thy |
4 "! a m s s' t n. \ |
7 "! a m s s' t n. \ |
5 \ (new_tv m a & new_tv m s) --> I e a m s = Ok(s',t,n) --> \ |
8 \ (new_tv m a & new_tv m s) --> I e a m s = Ok(s',t,n) --> \ |
6 \ ( ? r. W e ($ s a) m = Ok(r, $ s' t, n) & s' = ($ r o s) )"; |
9 \ ( ? r. W e ($ s a) m = Ok(r, $ s' t, n) & s' = ($ r o s) )"; |