# Open Induction

 Title: Open Induction Authors: Mizuhito Ogawa and Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com) Submission date: 2012-11-02 Abstract: A proof of the open induction schema based on J.-C. Raoult, Proving open properties by induction, Information Processing Letters 29, 1988, pp.19-23. This research was supported by the Austrian Science Fund (FWF): J3202. BibTeX: @article{Open_Induction-AFP, author = {Mizuhito Ogawa and Christian Sternagel}, title = {Open Induction}, journal = {Archive of Formal Proofs}, month = nov, year = 2012, note = {\url{https://isa-afp.org/entries/Open_Induction.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Used by: Decreasing-Diagrams-II, Functional_Ordered_Resolution_Prover, Myhill-Nerode, Well_Quasi_Orders Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.