Check-in [95a716e7e5]

Not logged in

 ```9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 ``` ```spec([ % Due to an oversight on my part, the way we handle inductive proofs, % although correct, will not work with the kind of incremental proofs % construction we are aiming to do. More permanent solutions will have to % come later, but for now we hard-code the IH into the specification. % (Which, yes, means that you can only prove one thing by induction!) ih('IH', add(' x', z, ' x'), 'nat|sml'(' x')), % Nat formation rules rule('Nat-z', nat(z), and([true])), rule('Nat-succ', nat(s(' n')), and([nat(' n')])), % Addition rules rule('Add-z', add(z,' x', ' x'), and([true])), ``` ``` | ``` ```9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 ``` ```spec([ % Due to an oversight on my part, the way we handle inductive proofs, % although correct, will not work with the kind of incremental proofs % construction we are aiming to do. More permanent solutions will have to % come later, but for now we hard-code the IH into the specification. % (Which, yes, means that you can only prove one thing by induction!) ih('IH', add(' x', z, ' x'), and(['nat|sml'(' x')])), % Nat formation rules rule('Nat-z', nat(z), and([true])), rule('Nat-succ', nat(s(' n')), and([nat(' n')])), % Addition rules rule('Add-z', add(z,' x', ' x'), and([true])), ```