Blueprint Summary🔗

Overview

Total entries107completed: 103; deps incomplete: 0; sorries: 1; no proof: 0

Ready now4Entries with an actionable next formalization step.

Fully closed103Local code and prerequisite closure are both complete.

Actionable priorities0Entries ready now and already unlocking downstream work.

Current blockers1Missing external or incomplete Lean declarations.

Missing informal coverage9Entries with Lean code but missing an informal statement or proof block.

Current blockers (1)

collatz_conjecture(Theorem)

Declaration with sorry: collatz_conjecture [theorem/lemma; contains sorry; in proof; refs: 1]

Missing informal coverage (9)

Entry index (107)

Definitions44completed: 41; deps incomplete: 0; sorries: 0; no proof: 0

Theorems63completed: 62; deps incomplete: 0; sorries: 1; no proof: 0

Informal-only entries3

Definition Index (44)

Theorem / Proposition / Lemma / Corollary Index (63)

By parent groups (9)

Data structures as they appear in LaPToP: lists/strings, functions as data, and related theories used when specifying programs that manipulate structure. The string and list material is Hehner's Sections 2.2 and 2.3; the formal counterparts are the Lean modules LaPToP.DataStructures.Strings and LaPToP.DataStructures.Lists . (8)

Notational conventions and elementary Boolean / predicate scaffolding used throughout Hehner's A Practical Theory of Programming . The book's Section 1.0 calls this Binary Theory ; its laws (reference §11.3.1) are formalized in the Lean module LaPToP.BasicTheories.Binary . (5)

A small exploratory demo chapter about the Collatz iteration. It is not part of Hehner's book; it exists so the Blueprint graph has an intentionally unfinished node from day one. (1)

collatz_conjecture(Theorem)
Associated lean decls (1)
- collatz_conjecture

Functions with an explicit domain, selective union, predicates and relations, and the quantifiers built on them: Hehner's Chapter 3, the prerequisite for the specifications and refinements of Program Theory. The formal counterparts are the Lean modules LaPToP.FunctionTheory.Functions , LaPToP.FunctionTheory.Quantifiers and LaPToP.FunctionTheory.FinePoints . (8)

Hehner's Chapter 5: the programming notations of "several languages" — control structures, scope, data structures, subprograms — explained as refinement notations or as specifications in the theory of Chapter 4. The while-loop of Section 5.2.0 is formalized in LaPToP.ProgramTheory.WhileLoop the for-loop of Section 5.2.3 in LaPToP.ProgramTheory.ForLoop , and variable declaration and suspension (Section 5.0) in LaPToP.ProgramTheory.Scope , assertions and backtracking (Section 5.4) in LaPToP.ProgramTheory.Assertions . (6)

Hehner's Chapter 7: "the stack, the queue, and the tree ... are presented here as case studies in theory design and implementation", a theory being "a contract between two parties, an implementer and a user". The data theories of Section 7.0 are formalized in LaPToP.TheoryDesign.Stack , SimpleStack , Queue and Tree ; program-stack theory (Section 7.1) in LaPToP.TheoryDesign.ProgramStack . (3)

Basic theories: numbers, bunches, sets, and the calculation style that underpins later program reasoning in LaPToP. The bunch and set material is Hehner's Sections 2.0 and 2.1; the formal counterpart lives in the Lean module LaPToP.BasicTheories.Bunch (axioms and laws) and LaPToP.BasicTheories.Numbers (named bunches, the interval, distribution). The number laws of Section 1.1 (reference §11.3.2) are in LaPToP.BasicTheories.NumberLaws . (15)

Recursive programs, time bounds, and concurrent composition as developed in later chapters of A Practical Theory of Programming . Recursive data definition (Section 6.0) is formalized in LaPToP.RecursiveDefinition.Nat and LaPToP.RecursiveDefinition.DataConstruction , and recursive program definition (Section 6.1) in LaPToP.RecursiveDefinition.Programs . (7)

Programs as predicates on pre- and post-states; refinement as implication; sequential composition, conditionals, and assignment in Hehner's theory. Sections 4.0–4.2 of the book are formalized in the Lean modules LaPToP.ProgramTheory.Specifications , LaPToP.ProgramTheory.Programs and LaPToP.ProgramTheory.Time . (10)

Dependency insights

Statement-used entries65Entries reused in statement dependencies.

Tracked parent groups9Grouped health rollups for parents with more than one child entry.

Most used in statements (65)

specification_notations(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 10proof uses: 0direct uses: 10downstream unlocks: 38
Associated lean decls (12)
bunch_vs_set(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 9proof uses: 0direct uses: 9downstream unlocks: 88
Associated lean decls (2)
- LaPToP.BasicTheories.Bunch
- LaPToP.BasicTheories.HSet
substitution_law(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 9proof uses: 0direct uses: 9downstream unlocks: 27
Associated lean decls (4)
time_variable(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 8proof uses: 0direct uses: 8downstream unlocks: 19
Associated lean decls (15)
bunch_primitives(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 74
Associated lean decls (3)
boolean_domain(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 63
Associated lean decls (5)
bunch_named_bunches(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 68
Associated lean decls (7)
solution_quantifier(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 53
Associated lean decls (6)
list_packaging(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 46
Associated lean decls (9)
quantifier_numeric(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 22
Associated lean decls (7)
Show all 55 more statement-used entries
- nat_induction_predicate(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 20
  Associated lean decls (14)
- list_as_string(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 55
  Associated lean decls (4)
- program_as_predicate(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 41
  Associated lean decls (13)
- quantifier_forall_exists(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 26
  Associated lean decls (8)
- refinement_by_steps_parts_cases(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 25
  Associated lean decls (13)
- string_syntax(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 50
  Associated lean decls (6)
- function_notation(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 34
  Associated lean decls (7)
- number_domain(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 26
  Associated lean decls (4)
- specification_implementability(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 25
  Associated lean decls (8)
- bunch_operator_distribution(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 24
  Associated lean decls (6)
- bunch_interval(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 13
  Associated lean decls (1)
  - LaPToP.BasicTheories.Bunch.interval
- recursive_program(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 11
  Associated lean decls (3)
- data_stack_theory(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 8
  Associated lean decls (10)
- list_axioms(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 8
  Associated lean decls (21)
- while_loop(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 8
  Associated lean decls (5)
- for_loop(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 4
  Associated lean decls (8)
- predicates_relations(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 57
  Associated lean decls (8)
- bunch_axioms_size(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 44
  Associated lean decls (4)
- assignment_spec(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 35
  Associated lean decls (3)
- refinement_laws(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 28
  Associated lean decls (8)
- list_summation(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 16
  Associated lean decls (19)
- least_fixed_points(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 11
  Associated lean decls (8)
- recursive_program_zap(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 11
  Associated lean decls (50)
- bunch_axioms_inclusion(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 3
  Associated lean decls (8)
- recursive_data_construction(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 3
  Associated lean decls (8)
- state_as_variables(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 42
  Associated lean decls (1)
  - LaPToP.ProgramTheory.Spec.State
- sequential_composition(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 34
  Associated lean decls (2)
  - LaPToP.ProgramTheory.Spec.seq
  - LaPToP.ProgramTheory.Spec.implementable_seq
- bunch_axioms_algebra(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 26
  Associated lean decls (12)
- bunch_nat_axioms(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 22
  Associated lean decls (2)
  - LaPToP.BasicTheories.Bunch.nat_construction
  - LaPToP.BasicTheories.Bunch.nat_induction
- function_axioms(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 21
  Associated lean decls (7)
- selective_union(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 19
  Associated lean decls (5)
- program_definition(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 17
  Associated lean decls (4)
- string_axioms_indexing(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 9
  Associated lean decls (5)
- data_stack_implementation(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 5
  Associated lean decls (11)
- assertions(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (13)
- program_stack_theory(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (9)
- skip_refines_true(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 29
  Associated lean decls (2)
  - LaPToP.ProgramTheory.Spec.top_refines_ok
  - skip_refines_true
- binary_laws_case(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 27
  Associated lean decls (22)
- specification_laws(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 26
  Associated lean decls (15)
- bunch_axioms_membership(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 20
  Associated lean decls (5)
- list_as_function(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 17
  Associated lean decls (12)
- recursive_time(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 11
  Associated lean decls (7)
- simple_data_stack_theory(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (5)
- variable_declaration(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (18)
- boolean_excluded_middle(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (2)
  - LaPToP.BasicTheories.Binary.excluded_middle
  - boolean_excluded_middle
- function_on_bunches(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (11)
- variable_suspension(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (12)
- binary_laws_algebra(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (38)
- binary_laws_basic(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (22)
- collatz_step(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (2)
  - collatzStep
  - collatzTerminatesAtOne
- function_totality(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (14)
- list_append_nil(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (2)
  - LaPToP.DataStructures.Str.append_nil
  - list_append_nil
- number_laws_order(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (9)
- program_stack_implementation(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (7)
- set_packaging(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (4)

Group health (9)

Basic theories: numbers, bunches, sets, and the calculation style that underpins later program reasoning in LaPToP. The bunch and set material is Hehner's Sections 2.0 and 2.1; the formal counterpart lives in the Lean module LaPToP.BasicTheories.Bunch (axioms and laws) and LaPToP.BasicTheories.Numbers (named bunches, the interval, distribution). The number laws of Section 1.1 (reference §11.3.2) are in LaPToP.BasicTheories.NumberLaws .basic_theories_core

Grouped view over entries sharing the same parent.

total: 22closed: 21local-only: 0ready: 1blocked: 0incomplete Lean: 0unlock score: 410

Next: calculation_style stage: statementdownstream unlocks: 0
Data structures as they appear in LaPToP: lists/strings, functions as data, and related theories used when specifying programs that manipulate structure. The string and list material is Hehner's Sections 2.2 and 2.3; the formal counterparts are the Lean modules LaPToP.DataStructures.Strings and LaPToP.DataStructures.Lists .data_structures_core

Grouped view over entries sharing the same parent.

total: 12closed: 11local-only: 0ready: 1blocked: 0incomplete Lean: 0unlock score: 169

Next: function_as_data stage: statementdownstream unlocks: 0
Recursive programs, time bounds, and concurrent composition as developed in later chapters of A Practical Theory of Programming . Recursive data definition (Section 6.0) is formalized in LaPToP.RecursiveDefinition.Nat and LaPToP.RecursiveDefinition.DataConstruction , and recursive program definition (Section 6.1) in LaPToP.RecursiveDefinition.Programs .recursion_concurrency_core

Grouped view over entries sharing the same parent.

total: 12closed: 11local-only: 0ready: 1blocked: 0incomplete Lean: 0unlock score: 56

Next: concurrent_composition stage: statementdownstream unlocks: 0
A small exploratory demo chapter about the Collatz iteration. It is not part of Hehner's book; it exists so the Blueprint graph has an intentionally unfinished node from day one.collatz_core

Grouped view over entries sharing the same parent.

total: 2closed: 1local-only: 0ready: 1blocked: 0incomplete Lean: 1unlock score: 1

Next: collatz_conjecture stage: proofdownstream unlocks: 0
Programs as predicates on pre- and post-states; refinement as implication; sequential composition, conditionals, and assignment in Hehner's theory. Sections 4.0–4.2 of the book are formalized in the Lean modules LaPToP.ProgramTheory.Specifications , LaPToP.ProgramTheory.Programs and LaPToP.ProgramTheory.Time .program_theory_core

Grouped view over entries sharing the same parent.

total: 16closed: 16local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 371

Next: no ready child currently unlocks downstream work.
Functions with an explicit domain, selective union, predicates and relations, and the quantifiers built on them: Hehner's Chapter 3, the prerequisite for the specifications and refinements of Program Theory. The formal counterparts are the Lean modules LaPToP.FunctionTheory.Functions , LaPToP.FunctionTheory.Quantifiers and LaPToP.FunctionTheory.FinePoints .function_theory_core

Grouped view over entries sharing the same parent.

total: 16closed: 16local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 252

Next: no ready child currently unlocks downstream work.
Notational conventions and elementary Boolean / predicate scaffolding used throughout Hehner's A Practical Theory of Programming . The book's Section 1.0 calls this Binary Theory ; its laws (reference §11.3.1) are formalized in the Lean module LaPToP.BasicTheories.Binary .prelude_core

Grouped view over entries sharing the same parent.

total: 7closed: 7local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 136

Next: no ready child currently unlocks downstream work.
Hehner's Chapter 5: the programming notations of "several languages" — control structures, scope, data structures, subprograms — explained as refinement notations or as specifications in the theory of Chapter 4. The while-loop of Section 5.2.0 is formalized in LaPToP.ProgramTheory.WhileLoop the for-loop of Section 5.2.3 in LaPToP.ProgramTheory.ForLoop , and variable declaration and suspension (Section 5.0) in LaPToP.ProgramTheory.Scope , assertions and backtracking (Section 5.4) in LaPToP.ProgramTheory.Assertions .programming_language_core

Grouped view over entries sharing the same parent.

total: 11closed: 11local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 19

Next: no ready child currently unlocks downstream work.
Hehner's Chapter 7: "the stack, the queue, and the tree ... are presented here as case studies in theory design and implementation", a theory being "a contract between two parties, an implementer and a user". The data theories of Section 7.0 are formalized in LaPToP.TheoryDesign.Stack , SimpleStack , Queue and Tree ; program-stack theory (Section 7.1) in LaPToP.TheoryDesign.ProgramStack .theory_design_core

Grouped view over entries sharing the same parent.

total: 9closed: 9local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 19

Next: no ready child currently unlocks downstream work.

Metadata

Owners in use1Distinct owners referenced by the current blueprint entries.

Tags in use55Distinct tags currently attached to blueprint entries.

Owner rollups (1)

Eric Hehnerhehner

entries: 5actionable: 0quick wins: 0linked PRs: 0

Tag rollups (55)

tag: famous

entries: 1actionable: 1quick wins: 0linked PRs: 0
tag: incomplete

entries: 1actionable: 1quick wins: 0linked PRs: 0
tag: playful

entries: 1actionable: 1quick wins: 0linked PRs: 0
tag: programs

entries: 18actionable: 0quick wins: 0linked PRs: 0
tag: basic

entries: 15actionable: 0quick wins: 0linked PRs: 0
tag: bunch

entries: 10actionable: 0quick wins: 0linked PRs: 0
tag: data

entries: 10actionable: 0quick wins: 0linked PRs: 0
tag: hehner-2.0

entries: 10actionable: 0quick wins: 0linked PRs: 0
tag: function

entries: 8actionable: 0quick wins: 0linked PRs: 0
tag: recursion

entries: 7actionable: 0quick wins: 0linked PRs: 0
Show all 45 more tags
- tag: hehner-2.2
  
  entries: 5actionable: 0quick wins: 0linked PRs: 0
- tag: loops
  
  entries: 5actionable: 0quick wins: 0linked PRs: 0
- tag: prelude
  
  entries: 5actionable: 0quick wins: 0linked PRs: 0
- tag: quantifier
  
  entries: 5actionable: 0quick wins: 0linked PRs: 0
- tag: strings
  
  entries: 5actionable: 0quick wins: 0linked PRs: 0
- tag: binary
  
  entries: 4actionable: 0quick wins: 0linked PRs: 0
- tag: hehner-11.3.1
  
  entries: 4actionable: 0quick wins: 0linked PRs: 0
- tag: lists
  
  entries: 4actionable: 0quick wins: 0linked PRs: 0
- tag: refinement
  
  entries: 4actionable: 0quick wins: 0linked PRs: 0
- tag: time
  
  entries: 4actionable: 0quick wins: 0linked PRs: 0
- tag: hehner-11.3.2
  
  entries: 3actionable: 0quick wins: 0linked PRs: 0
- tag: hehner-11.3.8
  
  entries: 3actionable: 0quick wins: 0linked PRs: 0
- tag: hehner-5.2.3
  
  entries: 3actionable: 0quick wins: 0linked PRs: 0
- tag: nat
  
  entries: 3actionable: 0quick wins: 0linked PRs: 0
- tag: number
  
  entries: 3actionable: 0quick wins: 0linked PRs: 0
- tag: stacks
  
  entries: 3actionable: 0quick wins: 0linked PRs: 0
- tag: theory design
  
  entries: 3actionable: 0quick wins: 0linked PRs: 0
- tag: hehner-2.3
  
  entries: 2actionable: 0quick wins: 0linked PRs: 0
- tag: hehner-3.1
  
  entries: 2actionable: 0quick wins: 0linked PRs: 0
- tag: hehner-4.0
  
  entries: 2actionable: 0quick wins: 0linked PRs: 0
- tag: hehner-4.0.1
  
  entries: 2actionable: 0quick wins: 0linked PRs: 0
- tag: hehner-5.2.0
  
  entries: 2actionable: 0quick wins: 0linked PRs: 0
- tag: hehner-6.0.0
  
  entries: 2actionable: 0quick wins: 0linked PRs: 0
- tag: hehner-6.0.2
  
  entries: 2actionable: 0quick wins: 0linked PRs: 0
- tag: hehner-7.0.1
  
  entries: 2actionable: 0quick wins: 0linked PRs: 0
- tag: laws
  
  entries: 2actionable: 0quick wins: 0linked PRs: 0
- tag: arithmetic
  
  entries: 1actionable: 0quick wins: 0linked PRs: 0
- tag: backtracking
  
  entries: 1actionable: 0quick wins: 0linked PRs: 0
- tag: boolean
  
  entries: 1actionable: 0quick wins: 0linked PRs: 0
- tag: development
  
  entries: 1actionable: 0quick wins: 0linked PRs: 0
- tag: hehner-2.1
  
  entries: 1actionable: 0quick wins: 0linked PRs: 0
- tag: hehner-3.0
  
  entries: 1actionable: 0quick wins: 0linked PRs: 0
- tag: hehner-3.2
  
  entries: 1actionable: 0quick wins: 0linked PRs: 0
- tag: hehner-3.3
  
  entries: 1actionable: 0quick wins: 0linked PRs: 0
- tag: hehner-4.0.2
  
  entries: 1actionable: 0quick wins: 0linked PRs: 0
- tag: hehner-4.1.0
  
  entries: 1actionable: 0quick wins: 0linked PRs: 0
- tag: hehner-4.1.1
  
  entries: 1actionable: 0quick wins: 0linked PRs: 0
- tag: hehner-4.2
  
  entries: 1actionable: 0quick wins: 0linked PRs: 0
- tag: hehner-4.2.2
  
  entries: 1actionable: 0quick wins: 0linked PRs: 0
- tag: hehner-5.4.0
  
  entries: 1actionable: 0quick wins: 0linked PRs: 0
- tag: hehner-6.1
  
  entries: 1actionable: 0quick wins: 0linked PRs: 0
- tag: hehner-6.1.0
  
  entries: 1actionable: 0quick wins: 0linked PRs: 0
- tag: hehner-7.1.1
  
  entries: 1actionable: 0quick wins: 0linked PRs: 0
- tag: list
  
  entries: 1actionable: 0quick wins: 0linked PRs: 0
- tag: set
  
  entries: 1actionable: 0quick wins: 0linked PRs: 0

Metadata audit

Missing owner102

Missing effort44

Untagged44

Missing owner (102)

add_one_to_each(Theorem)

Missing owner metadata.

effort: mediumtag: programstag: loopstag: liststag: hehner-5.2.3
Associated lean decls (10)
assertions(Definition)

Missing owner metadata.
Associated lean decls (13)
assignment_spec(Definition)

Missing owner metadata.
Associated lean decls (3)
backtracking(Theorem)

Missing owner metadata.

effort: smalltag: programstag: backtrackingtag: hehner-5.4.0
Associated lean decls (12)
binary_exponentiation(Theorem)

Missing owner metadata.

effort: smalltag: programstag: loopstag: hehner-5.2.3
Associated lean decls (7)
boolean_domain(Definition)

Missing owner metadata.
Associated lean decls (5)
bunch_axioms_algebra(Theorem)

Missing owner metadata.

effort: smalltag: basictag: bunchtag: hehner-2.0
Associated lean decls (12)
bunch_axioms_inclusion(Theorem)

Missing owner metadata.

effort: smalltag: basictag: bunchtag: hehner-2.0
Associated lean decls (8)
bunch_axioms_membership(Theorem)

Missing owner metadata.

effort: smalltag: basictag: bunchtag: hehner-2.0
Associated lean decls (5)
bunch_axioms_size(Theorem)

Missing owner metadata.

effort: smalltag: basictag: bunchtag: hehner-2.0
Associated lean decls (4)
Show all 92 more entries missing owner
- bunch_derived_laws(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: basictag: bunchtag: hehner-2.0
  Associated lean decls (10)
- bunch_interval(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LaPToP.BasicTheories.Bunch.interval
- bunch_interval_laws(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: basictag: bunchtag: hehner-2.0
  Associated lean decls (8)
- bunch_named_bunch_laws(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: basictag: bunchtag: hehner-2.0
  Associated lean decls (4)
- bunch_named_bunches(Definition)
  
  Missing owner metadata.
  Associated lean decls (7)
- bunch_nat_axioms(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: basictag: bunchtag: hehner-2.0
  Associated lean decls (2)
  - LaPToP.BasicTheories.Bunch.nat_construction
  - LaPToP.BasicTheories.Bunch.nat_induction
- bunch_null_laws(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: basictag: bunchtag: hehner-2.0
  Associated lean decls (5)
- bunch_operator_distribution(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: basictag: bunchtag: hehner-2.0
  Associated lean decls (6)
- bunch_primitives(Definition)
  
  Missing owner metadata.
  Associated lean decls (3)
- bunch_vs_set(Definition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LaPToP.BasicTheories.Bunch
  - LaPToP.BasicTheories.HSet
- calculation_style(Definition)
  
  Missing owner metadata.
- collatz_conjecture(Theorem)
  
  Missing owner metadata.
  
  effort: mediumtag: playfultag: famoustag: incomplete
  Associated lean decls (1)
  - collatz_conjecture
- collatz_step(Definition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - collatzStep
  - collatzTerminatesAtOne
- concurrent_composition(Definition)
  
  Missing owner metadata.
- data_queue_theory(Definition)
  
  Missing owner metadata.
  Associated lean decls (10)
- data_stack_implementation(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: theory designtag: stackstag: hehner-7.0.1
  Associated lean decls (11)
- data_stack_theory(Definition)
  
  Missing owner metadata.
  Associated lean decls (10)
- data_tree_theory(Definition)
  
  Missing owner metadata.
  Associated lean decls (12)
- fancy_and_weak_program_stack(Definition)
  
  Missing owner metadata.
  Associated lean decls (10)
- for_loop(Definition)
  
  Missing owner metadata.
  Associated lean decls (8)
- for_loop_timing(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: programstag: loopstag: timetag: hehner-5.2.3
  Associated lean decls (7)
- function_as_data(Definition)
  
  Missing owner metadata.
- function_axioms(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: functiontag: hehner-3.0
  Associated lean decls (7)
- function_inclusion(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: functiontag: hehner-3.2
  Associated lean decls (20)
- function_notation(Definition)
  
  Missing owner metadata.
  Associated lean decls (7)
- function_on_bunches(Definition)
  
  Missing owner metadata.
  Associated lean decls (11)
- function_totality(Definition)
  
  Missing owner metadata.
  Associated lean decls (14)
- inconsistent_axiom_bad(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: recursiontag: datatag: hehner-6.0.2
  Associated lean decls (10)
- least_fixed_points(Definition)
  
  Missing owner metadata.
  Associated lean decls (8)
- list_append_nil(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: datatag: lists
  Associated lean decls (2)
  - LaPToP.DataStructures.Str.append_nil
  - list_append_nil
- list_as_function(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: functiontag: listtag: hehner-3.3
  Associated lean decls (12)
- list_as_string(Definition)
  
  Missing owner metadata.
  Associated lean decls (4)
- list_axioms(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: datatag: liststag: hehner-2.3
  Associated lean decls (21)
- list_derived_laws(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: datatag: liststag: hehner-2.3
  Associated lean decls (3)
- list_packaging(Definition)
  
  Missing owner metadata.
  Associated lean decls (9)
- list_summation(Theorem)
  
  Missing owner metadata.
  
  effort: mediumtag: programstag: developmenttag: hehner-4.1.1
  Associated lean decls (19)
- loop_definition(Definition)
  
  Missing owner metadata.
  Associated lean decls (12)
- nat_add_zero(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: basictag: arithmetic
  Associated lean decls (2)
  - LaPToP.BasicTheories.Number.add_zero
  - nat_add_zero
- nat_induction_predicate(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: recursiontag: nattag: hehner-6.0.0
  Associated lean decls (14)
- nat_induction_versions(Theorem)
  
  Missing owner metadata.
  
  effort: mediumtag: recursiontag: nattag: hehner-6.0.0
  Associated lean decls (18)
- nat_repeat_zero(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: recursiontag: nat
  Associated lean decls (1)
  - nat_repeat_zero
- number_domain(Definition)
  
  Missing owner metadata.
  Associated lean decls (4)
- number_laws_additive(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: basictag: numbertag: hehner-11.3.2
  Associated lean decls (22)
- number_laws_multiplicative(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: basictag: numbertag: hehner-11.3.2
  Associated lean decls (20)
- number_laws_order(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: basictag: numbertag: hehner-11.3.2
  Associated lean decls (9)
- pow_least_fixed_point(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: recursiontag: datatag: hehner-6.0.2
  Associated lean decls (15)
- predicates_relations(Definition)
  
  Missing owner metadata.
  Associated lean decls (8)
- program_as_predicate(Definition)
  
  Missing owner metadata.
  Associated lean decls (13)
- program_definition(Definition)
  
  Missing owner metadata.
  Associated lean decls (4)
- program_stack_implementation(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: theory designtag: stackstag: hehner-7.1.1
  Associated lean decls (7)
- program_stack_theory(Definition)
  
  Missing owner metadata.
  Associated lean decls (9)
- quantifier_forall_exists(Definition)
  
  Missing owner metadata.
  Associated lean decls (8)
- quantifier_laws_basic(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: functiontag: quantifiertag: hehner-3.1
  Associated lean decls (5)
- quantifier_laws_logical(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: functiontag: quantifiertag: hehner-11.3.8
  Associated lean decls (34)
- quantifier_laws_numeric(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: functiontag: quantifiertag: hehner-11.3.8
  Associated lean decls (21)
- quantifier_laws_solution(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: functiontag: quantifiertag: hehner-11.3.8
  Associated lean decls (19)
- quantifier_numeric(Definition)
  
  Missing owner metadata.
  Associated lean decls (7)
- quantifier_numeric_axioms(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: functiontag: quantifiertag: hehner-3.1
  Associated lean decls (17)
- recursive_data_construction(Definition)
  
  Missing owner metadata.
  Associated lean decls (8)
- recursive_program(Definition)
  
  Missing owner metadata.
  Associated lean decls (3)
- recursive_program_construction(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: recursiontag: programstag: hehner-6.1.0
  Associated lean decls (5)
- recursive_program_zap(Theorem)
  
  Missing owner metadata.
  
  effort: mediumtag: recursiontag: programstag: hehner-6.1
  Associated lean decls (50)
- recursive_time(Theorem)
  
  Missing owner metadata.
  
  effort: mediumtag: programstag: timetag: hehner-4.2
  Associated lean decls (7)
- refinement_by_steps_parts_cases(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: programstag: refinementtag: hehner-4.1.0
  Associated lean decls (13)
- refinement_examples(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: programstag: refinementtag: hehner-4.0
  Associated lean decls (14)
- refinement_laws(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: programstag: refinementtag: hehner-4.0.2
  Associated lean decls (8)
- selective_union(Definition)
  
  Missing owner metadata.
  Associated lean decls (5)
- sequential_composition(Definition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LaPToP.ProgramTheory.Spec.seq
  - LaPToP.ProgramTheory.Spec.implementable_seq
- set_axioms(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: basictag: settag: hehner-2.1
  Associated lean decls (9)
- set_packaging(Definition)
  
  Missing owner metadata.
  Associated lean decls (4)
- simple_data_stack_theory(Definition)
  
  Missing owner metadata.
  Associated lean decls (5)
- skip_refines_true(Theorem)
  
  Missing owner metadata.
  
  effort: smallpriority: hightag: programstag: refinement
  Associated lean decls (2)
  - LaPToP.ProgramTheory.Spec.top_refines_ok
  - skip_refines_true
- solution_quantifier(Definition)
  
  Missing owner metadata.
  Associated lean decls (6)
- specification_implementability(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: programstag: hehner-4.0
  Associated lean decls (8)
- specification_laws(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: programstag: lawstag: hehner-4.0.1
  Associated lean decls (15)
- specification_notations(Definition)
  
  Missing owner metadata.
  Associated lean decls (12)
- stack_theory_incomplete(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: theory designtag: stackstag: hehner-7.0.1
  Associated lean decls (9)
- state_as_variables(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LaPToP.ProgramTheory.Spec.State
- string_axioms_copies_update(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: datatag: stringstag: hehner-2.2
  Associated lean decls (6)
- string_axioms_indexing(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: datatag: stringstag: hehner-2.2
  Associated lean decls (5)
- string_axioms_join_length(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: datatag: stringstag: hehner-2.2
  Associated lean decls (7)
- string_axioms_order(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: datatag: stringstag: hehner-2.2
  Associated lean decls (3)
- string_interval_laws(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: datatag: stringstag: hehner-2.2
  Associated lean decls (5)
- string_syntax(Definition)
  
  Missing owner metadata.
  Associated lean decls (6)
- substitution_law(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: programstag: lawstag: hehner-4.0.1
  Associated lean decls (4)
- termination(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: programstag: timetag: hehner-4.2.2
  Associated lean decls (12)
- time_variable(Definition)
  
  Missing owner metadata.
  Associated lean decls (15)
- unbounded_bound(Theorem)
  
  Missing owner metadata.
  
  effort: mediumtag: programstag: loopstag: timetag: hehner-5.2.0
  Associated lean decls (13)
- variable_declaration(Definition)
  
  Missing owner metadata.
  Associated lean decls (18)
- variable_suspension(Definition)
  
  Missing owner metadata.
  Associated lean decls (12)
- while_list_summation(Theorem)
  
  Missing owner metadata.
  
  effort: smalltag: programstag: loopstag: hehner-5.2.0
  Associated lean decls (10)
- while_loop(Definition)
  
  Missing owner metadata.
  Associated lean decls (5)

Missing effort (44)

assertions(Definition)

Missing effort metadata.
Associated lean decls (13)
assignment_spec(Definition)

Missing effort metadata.
Associated lean decls (3)
boolean_domain(Definition)

Missing effort metadata.
Associated lean decls (5)
bunch_interval(Definition)

Missing effort metadata.
Associated lean decls (1)
- LaPToP.BasicTheories.Bunch.interval
bunch_named_bunches(Definition)

Missing effort metadata.
Associated lean decls (7)
bunch_primitives(Definition)

Missing effort metadata.
Associated lean decls (3)
bunch_vs_set(Definition)

Missing effort metadata.
Associated lean decls (2)
- LaPToP.BasicTheories.Bunch
- LaPToP.BasicTheories.HSet
calculation_style(Definition)

Missing effort metadata.
collatz_step(Definition)

Missing effort metadata.
Associated lean decls (2)
- collatzStep
- collatzTerminatesAtOne
concurrent_composition(Definition)

Missing effort metadata.
Show all 34 more entries missing effort
- data_queue_theory(Definition)
  
  Missing effort metadata.
  Associated lean decls (10)
- data_stack_theory(Definition)
  
  Missing effort metadata.
  Associated lean decls (10)
- data_tree_theory(Definition)
  
  Missing effort metadata.
  Associated lean decls (12)
- fancy_and_weak_program_stack(Definition)
  
  Missing effort metadata.
  Associated lean decls (10)
- for_loop(Definition)
  
  Missing effort metadata.
  Associated lean decls (8)
- function_as_data(Definition)
  
  Missing effort metadata.
- function_notation(Definition)
  
  Missing effort metadata.
  Associated lean decls (7)
- function_on_bunches(Definition)
  
  Missing effort metadata.
  Associated lean decls (11)
- function_totality(Definition)
  
  Missing effort metadata.
  Associated lean decls (14)
- least_fixed_points(Definition)
  
  Missing effort metadata.
  Associated lean decls (8)
- list_as_string(Definition)
  
  Missing effort metadata.
  Associated lean decls (4)
- list_packaging(Definition)
  
  Missing effort metadata.
  Associated lean decls (9)
- loop_definition(Definition)
  
  Missing effort metadata.
  Associated lean decls (12)
- number_domain(Definition)
  
  Missing effort metadata.
  Associated lean decls (4)
- predicates_relations(Definition)
  
  Missing effort metadata.
  Associated lean decls (8)
- program_as_predicate(Definition)
  
  Missing effort metadata.
  Associated lean decls (13)
- program_definition(Definition)
  
  Missing effort metadata.
  Associated lean decls (4)
- program_stack_theory(Definition)
  
  Missing effort metadata.
  Associated lean decls (9)
- quantifier_forall_exists(Definition)
  
  Missing effort metadata.
  Associated lean decls (8)
- quantifier_numeric(Definition)
  
  Missing effort metadata.
  Associated lean decls (7)
- recursive_data_construction(Definition)
  
  Missing effort metadata.
  Associated lean decls (8)
- recursive_program(Definition)
  
  Missing effort metadata.
  Associated lean decls (3)
- selective_union(Definition)
  
  Missing effort metadata.
  Associated lean decls (5)
- sequential_composition(Definition)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LaPToP.ProgramTheory.Spec.seq
  - LaPToP.ProgramTheory.Spec.implementable_seq
- set_packaging(Definition)
  
  Missing effort metadata.
  Associated lean decls (4)
- simple_data_stack_theory(Definition)
  
  Missing effort metadata.
  Associated lean decls (5)
- solution_quantifier(Definition)
  
  Missing effort metadata.
  Associated lean decls (6)
- specification_notations(Definition)
  
  Missing effort metadata.
  Associated lean decls (12)
- state_as_variables(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LaPToP.ProgramTheory.Spec.State
- string_syntax(Definition)
  
  Missing effort metadata.
  Associated lean decls (6)
- time_variable(Definition)
  
  Missing effort metadata.
  Associated lean decls (15)
- variable_declaration(Definition)
  
  Missing effort metadata.
  Associated lean decls (18)
- variable_suspension(Definition)
  
  Missing effort metadata.
  Associated lean decls (12)
- while_loop(Definition)
  
  Missing effort metadata.
  Associated lean decls (5)

Untagged (44)

assertions(Definition)

Missing tag metadata.
Associated lean decls (13)
assignment_spec(Definition)

Missing tag metadata.
Associated lean decls (3)
boolean_domain(Definition)

Missing tag metadata.
Associated lean decls (5)
bunch_interval(Definition)

Missing tag metadata.
Associated lean decls (1)
- LaPToP.BasicTheories.Bunch.interval
bunch_named_bunches(Definition)

Missing tag metadata.
Associated lean decls (7)
bunch_primitives(Definition)

Missing tag metadata.
Associated lean decls (3)
bunch_vs_set(Definition)

Missing tag metadata.
Associated lean decls (2)
- LaPToP.BasicTheories.Bunch
- LaPToP.BasicTheories.HSet
calculation_style(Definition)

Missing tag metadata.
collatz_step(Definition)

Missing tag metadata.
Associated lean decls (2)
- collatzStep
- collatzTerminatesAtOne
concurrent_composition(Definition)

Missing tag metadata.
Show all 34 more untagged entries
- data_queue_theory(Definition)
  
  Missing tag metadata.
  Associated lean decls (10)
- data_stack_theory(Definition)
  
  Missing tag metadata.
  Associated lean decls (10)
- data_tree_theory(Definition)
  
  Missing tag metadata.
  Associated lean decls (12)
- fancy_and_weak_program_stack(Definition)
  
  Missing tag metadata.
  Associated lean decls (10)
- for_loop(Definition)
  
  Missing tag metadata.
  Associated lean decls (8)
- function_as_data(Definition)
  
  Missing tag metadata.
- function_notation(Definition)
  
  Missing tag metadata.
  Associated lean decls (7)
- function_on_bunches(Definition)
  
  Missing tag metadata.
  Associated lean decls (11)
- function_totality(Definition)
  
  Missing tag metadata.
  Associated lean decls (14)
- least_fixed_points(Definition)
  
  Missing tag metadata.
  Associated lean decls (8)
- list_as_string(Definition)
  
  Missing tag metadata.
  Associated lean decls (4)
- list_packaging(Definition)
  
  Missing tag metadata.
  Associated lean decls (9)
- loop_definition(Definition)
  
  Missing tag metadata.
  Associated lean decls (12)
- number_domain(Definition)
  
  Missing tag metadata.
  Associated lean decls (4)
- predicates_relations(Definition)
  
  Missing tag metadata.
  Associated lean decls (8)
- program_as_predicate(Definition)
  
  Missing tag metadata.
  Associated lean decls (13)
- program_definition(Definition)
  
  Missing tag metadata.
  Associated lean decls (4)
- program_stack_theory(Definition)
  
  Missing tag metadata.
  Associated lean decls (9)
- quantifier_forall_exists(Definition)
  
  Missing tag metadata.
  Associated lean decls (8)
- quantifier_numeric(Definition)
  
  Missing tag metadata.
  Associated lean decls (7)
- recursive_data_construction(Definition)
  
  Missing tag metadata.
  Associated lean decls (8)
- recursive_program(Definition)
  
  Missing tag metadata.
  Associated lean decls (3)
- selective_union(Definition)
  
  Missing tag metadata.
  Associated lean decls (5)
- sequential_composition(Definition)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LaPToP.ProgramTheory.Spec.seq
  - LaPToP.ProgramTheory.Spec.implementable_seq
- set_packaging(Definition)
  
  Missing tag metadata.
  Associated lean decls (4)
- simple_data_stack_theory(Definition)
  
  Missing tag metadata.
  Associated lean decls (5)
- solution_quantifier(Definition)
  
  Missing tag metadata.
  Associated lean decls (6)
- specification_notations(Definition)
  
  Missing tag metadata.
  Associated lean decls (12)
- state_as_variables(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LaPToP.ProgramTheory.Spec.State
- string_syntax(Definition)
  
  Missing tag metadata.
  Associated lean decls (6)
- time_variable(Definition)
  
  Missing tag metadata.
  Associated lean decls (15)
- variable_declaration(Definition)
  
  Missing tag metadata.
  Associated lean decls (18)
- variable_suspension(Definition)
  
  Missing tag metadata.
  Associated lean decls (12)
- while_loop(Definition)
  
  Missing tag metadata.
  Associated lean decls (5)

Structure and coverage

Informal-only3Statements with no associated Lean code yet.

Ready to formalize4Entries with an actionable next formalization step.

Fully closed103Local code and ancestor closure are both complete.

Heaviest prerequisites (101)

list_summation(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 5statement deps: 5proof deps: 0direct uses: 3downstream unlocks: 16
Associated lean decls (19)
function_inclusion(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (20)
list_as_function(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 4statement deps: 4proof deps: 0direct uses: 1downstream unlocks: 17
Associated lean decls (12)
loop_definition(Definition)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (12)
program_as_predicate(Definition)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 4statement deps: 4proof deps: 0direct uses: 5downstream unlocks: 41
Associated lean decls (13)
recursive_program_zap(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 4statement deps: 4proof deps: 0direct uses: 3downstream unlocks: 11
Associated lean decls (50)
recursive_time(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 4statement deps: 4proof deps: 0direct uses: 1downstream unlocks: 11
Associated lean decls (7)
time_variable(Definition)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 4statement deps: 4proof deps: 0direct uses: 8downstream unlocks: 19
Associated lean decls (15)
unbounded_bound(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (13)
variable_suspension(Definition)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 4statement deps: 4proof deps: 0direct uses: 1downstream unlocks: 2
Associated lean decls (12)
Show all 91 more heaviest-prerequisite entries
- while_list_summation(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (10)
- add_one_to_each(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (10)
- backtracking(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (12)
- bunch_interval_laws(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (8)
- data_stack_implementation(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 2downstream unlocks: 5
  Associated lean decls (11)
- data_stack_theory(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 4downstream unlocks: 8
  Associated lean decls (10)
- data_tree_theory(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (12)
- fancy_and_weak_program_stack(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (10)
- for_loop_timing(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (7)
- least_fixed_points(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 3downstream unlocks: 11
  Associated lean decls (8)
- list_axioms(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 4downstream unlocks: 8
  Associated lean decls (21)
- nat_induction_predicate(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 6downstream unlocks: 20
  Associated lean decls (14)
- pow_least_fixed_point(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (15)
- program_stack_implementation(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (7)
- program_stack_theory(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (9)
- quantifier_laws_solution(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (19)
- quantifier_numeric_axioms(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (17)
- refinement_examples(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (14)
- sequential_composition(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 2downstream unlocks: 34
  Associated lean decls (2)
  - LaPToP.ProgramTheory.Spec.seq
  - LaPToP.ProgramTheory.Spec.implementable_seq
- specification_laws(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 26
  Associated lean decls (15)
- variable_declaration(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (18)
- assertions(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (13)
- assignment_spec(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 35
  Associated lean decls (3)
- binary_exponentiation(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (7)
- binary_laws_basic(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (22)
- bunch_derived_laws(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (10)
- bunch_named_bunch_laws(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (4)
- bunch_nat_axioms(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 22
  Associated lean decls (2)
  - LaPToP.BasicTheories.Bunch.nat_construction
  - LaPToP.BasicTheories.Bunch.nat_induction
- bunch_null_laws(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (5)
- bunch_operator_distribution(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 4downstream unlocks: 24
  Associated lean decls (6)
- data_queue_theory(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (10)
- for_loop(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 4downstream unlocks: 4
  Associated lean decls (8)
- function_on_bunches(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (11)
- function_totality(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (14)
- inconsistent_axiom_bad(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (10)
- list_derived_laws(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (3)
- list_packaging(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 6downstream unlocks: 46
  Associated lean decls (9)
- nat_induction_versions(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (18)
- predicates_relations(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 57
  Associated lean decls (8)
- program_definition(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 17
  Associated lean decls (4)
- quantifier_laws_basic(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (5)
- quantifier_laws_logical(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (34)
- quantifier_laws_numeric(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (21)
- quantifier_numeric(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 6downstream unlocks: 22
  Associated lean decls (7)
- recursive_program(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 4downstream unlocks: 11
  Associated lean decls (3)
- recursive_program_construction(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (5)
- refinement_by_steps_parts_cases(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 5downstream unlocks: 25
  Associated lean decls (13)
- refinement_laws(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 28
  Associated lean decls (8)
- selective_union(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 19
  Associated lean decls (5)
- set_axioms(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (9)
- simple_data_stack_theory(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (5)
- solution_quantifier(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 6downstream unlocks: 53
  Associated lean decls (6)
- specification_notations(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 10downstream unlocks: 38
  Associated lean decls (12)
- string_axioms_join_length(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (7)
- string_interval_laws(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (5)
- substitution_law(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 9downstream unlocks: 27
  Associated lean decls (4)
- termination(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (12)
- while_loop(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 4downstream unlocks: 8
  Associated lean decls (5)
- binary_laws_algebra(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (38)
- binary_laws_case(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 27
  Associated lean decls (22)
- binary_laws_reasoning(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (18)
- boolean_excluded_middle(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (2)
  - LaPToP.BasicTheories.Binary.excluded_middle
  - boolean_excluded_middle
- bunch_axioms_algebra(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 26
  Associated lean decls (12)
- bunch_axioms_inclusion(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 3
  Associated lean decls (8)
- bunch_axioms_membership(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 20
  Associated lean decls (5)
- bunch_axioms_size(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 44
  Associated lean decls (4)
- bunch_interval(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 13
  Associated lean decls (1)
  - LaPToP.BasicTheories.Bunch.interval
- bunch_named_bunches(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 6downstream unlocks: 68
  Associated lean decls (7)
- bunch_primitives(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 7downstream unlocks: 74
  Associated lean decls (3)
- collatz_conjecture(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - collatz_conjecture
- concurrent_composition(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
- function_as_data(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
- function_axioms(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 21
  Associated lean decls (7)
- function_notation(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 34
  Associated lean decls (7)
- list_append_nil(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (2)
  - LaPToP.DataStructures.Str.append_nil
  - list_append_nil
- nat_add_zero(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (2)
  - LaPToP.BasicTheories.Number.add_zero
  - nat_add_zero
- nat_repeat_zero(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - nat_repeat_zero
- number_domain(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 26
  Associated lean decls (4)
- number_laws_additive(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (22)
- number_laws_multiplicative(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (20)
- number_laws_order(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (9)
- quantifier_forall_exists(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 5downstream unlocks: 26
  Associated lean decls (8)
- recursive_data_construction(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 3
  Associated lean decls (8)
- set_packaging(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (4)
- skip_refines_true(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 29
  Associated lean decls (2)
  - LaPToP.ProgramTheory.Spec.top_refines_ok
  - skip_refines_true
- specification_implementability(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 25
  Associated lean decls (8)
- stack_theory_incomplete(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (9)
- string_axioms_copies_update(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (6)
- string_axioms_indexing(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 9
  Associated lean decls (5)
- string_axioms_order(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (3)
- string_syntax(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 50
  Associated lean decls (6)

No prerequisites (6)

bunch_vs_set(Definition)
Associated lean decls (2)
- LaPToP.BasicTheories.Bunch
- LaPToP.BasicTheories.HSet
collatz_step(Definition)
Associated lean decls (2)
- collatzStep
- collatzTerminatesAtOne
calculation_style(Definition)
state_as_variables(Definition)
Associated lean decls (1)
- LaPToP.ProgramTheory.Spec.State
boolean_domain(Definition)
Associated lean decls (5)
list_as_string(Definition)
Associated lean decls (4)

No dependents (42)

Proof debt hotspots (1)

A small exploratory demo chapter about the Collatz iteration. It is not part of Hehner's book; it exists so the Blueprint graph has an intentionally unfinished node from day one.collatz_core

Grouped proof/code debt derived from the current incomplete-declaration snapshots.

affected entries: 1incomplete decls: 1missing decls: 0total debt: 1