Lines Matching defs:proof
533 relations (proof by extensionality), and rules about the empty set and the
689 function, which is defined in terms of~\isa{cons}. The proof that
1864 the proof requires a quantified induction formula, but
1888 An alternative proof uses Isar's fancy \isa{induct} method, which
1901 the previous proof. As before, to conclude requires only \isa{auto}.
2022 \isa{rules} section of a theory, will be visible in proof scripts.
2025 leads to short proof scripts:
2151 (The proof uses depth-first search.)
2434 equivalence proof taken from Winskel~\cite{winskel93}. It formalises the
2457 proof that Ackermann's function is not primitive recursive.
2497 \section{A proof about powersets}\label{sec:ZF-pow-example}
2502 be instructive. This proof exploits the lattice properties of
2518 A shorter proof results from noting that intersection forms the greatest
2569 To conclude the proof, we clear up the trivial subgoals:
2575 We could have performed this proof instantly by calling
2581 Past researchers regarded this as a difficult proof, as indeed it is if all
2643 underlying representation, as in the following proof