Checksum: e0f5eb1625a6b9fc38dbbdd6b4659de6124ac162bf82029284fccb3a53000173 (page 1)

• acl2/6.5-2/books/models/jvm/m1/m1-half-via-inductive-assertions.acl2
• acl2/6.5-2~bpo70+1/books/models/jvm/m1/m1-half-via-inductive-assertions.acl2
• acl2/7.2dfsg-3/books/models/jvm/m1/m1-half-via-inductive-assertions.acl2
• acl2/8.0dfsg-1/books/models/jvm/m1/m1-half-via-inductive-assertions.acl2
• acl2/8.3dfsg-2/books/models/jvm/m1/m1-half-via-inductive-assertions.acl2
• acl2/8.5dfsg-5/books/models/jvm/m1/m1-half-via-inductive-assertions.acl2
• acl2/8.6+dfsg-2/books/models/jvm/m1/m1-half-via-inductive-assertions.acl2
• acl2/8.6+dfsg-3/books/models/jvm/m1/m1-half-via-inductive-assertions.acl2