*Hyp with extensionality resume by contradiction set name lemma critical-pairs *Hyp with extensionality qed % Three theorems about subset set proof-methods =>, normalization prove e \in x /\ x \subseteq y => e \in y by induction on x resume by case ec = e1c set name lemma complete qed prove x \subseteq y /\ y \subseteq x => x = y set name lemma prove e \in xc <=> e \in yc by <=> complete complete instantiate x by xc, y by yc in extensionality qed prove (x \union y) \subseteq z <=> x \subseteq z /\ y \subseteq z by induction on x qed % An alternate induction rule prove sort S generated by {}, {__}, \union set name lemma resume by induction critical-pairs *GenHyp with *GenHyp critical-pairs *InductHyp with lemma qed Bibliography Pascal André, Annya Romanczuk, Jean-Claude Royer, and Aline Vasconcelos, "Checking the consistency of UML class diagrams using Larch Prover", Proceedings of the 2000 International Conference on Rigorous Object-Oriented Methods, page 1, York, UK, BCS Learning & Development Ltd., Swindon, GBR, January 2000. Boutheina Chetali, "Formal verification of concurrent programs using the Larch Prover", IEEE Transactions on Software Engineering 24:1, pages 46–62, January 1998. doi: 10.1109/32.663997. Manfred Broy, "Experiences with software specification and verification using LP, the Larch proof assistant", Formal Methods in System Design 8:3, pages 221–272, 1996. Urban Engberg, Peter Grønning, and Leslie Lamport, "Mechanical Verification of Concurrent Systems with TLA", Computer-Aided Verification, G. v. Bochmann and D. K. Probst editors, Proceedings of the Fourth International Conference CAV'92), Lecture Notes in Computer Science 663, Springer-Verlag, June 1992, pages 44–55. Urban Engberg, Reasoning in the Temporal Logic of Actions, BRICS Dissertation Series DS 96–1, Department of Computer Science, University of Aarhus, Denmark, August 1996. ISSN 1396-7002. Stephen J. Garland and John V. Guttag, "Inductive methods for reasoning about abstract data types," Fifteenth Annual ACM Symposium on Principles of Programming Languages, pages 219–228, San Diego, CA, January 1988. Stephen J. Garland and John V. Guttag, "LP: The Larch Prover," Ninth International Conference on Automated Deduction Lecture Notes in Computer Science 310, pages 748–749, Argonne, Illinois, May 1988. Springer-Verlag. Stephen J. Garland, John V. Guttag, and Jørgen Staunstrup, "Verification of VLSI circuits using LP," The Fusion of Hardware Design and Verification, pages 329–345, Glasgow, Scotland, July 4–6, 1988. IFIP WG 10.2, North Holland. Stephen J. Garland and John V. Guttag, "An overview of LP, the Larch Prover,"