Constant MATH_GODEL_LITERATE 

pub const MATH_GODEL_LITERATE: &str = r###"-- ============================================
-- GÖDEL SENTENCE CONSTRUCTION (Literate Mode)
-- ============================================
-- Building the self-referential sentence G that says "I am not provable"
--
-- This example demonstrates the fully Literate meta-logic syntax:
-- - "## To be Predicate" for predicate definitions
-- - "Let X be Y" for constant definitions
-- - "the Name X" for syntax names (maps to SName)
-- - "Variable N" for syntax variables (maps to SVar)
-- - "Apply(f, x)" for syntax application (maps to SApp)
-- - "the diagonalization of T" for diagonal lemma
-- - "there exists a d: T such that P" for existential quantification
-- - "X equals Y" for equality propositions

-- ============================================
-- 1. THE PROVABILITY PREDICATE
-- ============================================
-- "s is provable if there exists a derivation d that concludes s"

## To be Provable (s: Syntax) -> Prop:
    Yield there exists a d: Derivation such that (concludes(d) equals s).

-- ============================================
-- 2. THE TEMPLATE T
-- ============================================
-- T encodes "Not(Provable(x))" as syntax

Let Not_Name be the Name "Not".
Let Provable_Name be the Name "Provable".
Let T be Apply(Not_Name, Apply(Provable_Name, Variable 0)).

-- ============================================
-- 3. THE GÖDEL SENTENCE G
-- ============================================
-- G = T[code(T)/x] via the diagonal lemma
-- G says "I am not provable"

Let G be the diagonalization of T.

-- ============================================
-- VERIFICATION
-- ============================================

Check Provable.
Check T.
Check G.
Check Provable(G).
"###;