Hierarchy

Cumulative hierarchy example

Open in Workbench View on GitHub

1-- Cumulative hierarchy example2-- Part of the Grace17 proof assistant for mathematics based on set theory.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module HierarchyDemo8import Grace.Cumulus.Set910-- Evaluates to four nested powersets over the empty set.11eval finite(4)1213theorem naturals_are_ordinals (n : Nat)14  shows n in Ordinal15proof16  simp [Ordinal.natural]1718theorem V_three_membership (x : Set)19  shows x in finite(3) <-> Subset(x, finite(2))20proof21  simp [finite, set.powerset, Subset]22