{"issue":{"pull_request":{"diff_url":null,"html_url":null,"patch_url":null},"state":"open","user":{"avatar_url":"https://secure.gravatar.com/avatar/4d5ed0e3301f94353dd52b228752f601?d=https://a248.e.akamai.net/assets.github.com%2Fimages%2Fgravatars%2Fgravatar-140.png","gravatar_id":"4d5ed0e3301f94353dd52b228752f601","url":"https://api.github.com/users/yav","login":"yav","id":12394},"milestone":null,"assignee":null,"updated_at":"2011-11-11T06:56:26Z","labels":[],"comments":0,"closed_at":null,"url":"https://api.github.com/repos/yav/tc-solver/issues/2","body":"We need backward rules of the form:\r\n\r\n(x <= 5) => (x <= 7)\r\n\r\nThey are derived by specializing transitivity of <= on the axioms.  It is easy to generate the correct rules\r\n(they got removed accidentally) but first I'll have to update the generator so that it can deal with brule with parameters.\r\n\r\nI never updated that part when adding proof objects because I though (incorrectly) that all BRules will be simple.","html_url":"https://github.com/yav/tc-solver/issues/2","title":"Backward reasoning for <=","number":2,"id":2206840,"created_at":"2011-11-11T06:56:26Z"},"action":"opened"}