ExampleConstruction: AI-generatedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Substituting into $K_{2}$ gives the join and substituting into $\overline{K_{2}}$ gives the disjoint union

Example

Let $G_{1}$ and $G_{2}$ be nonnull graphs on vertex sets disjoint from each other and from the two template vertices below. Successively substituting $G_{1}$ and $G_{2}$ for the two vertices of $K_{2}$ gives the join $G_{1} \lor G_{2}$ , obtained from their disjoint union by adding every edge between the two vertex sets. Successively substituting them for the two vertices of $\overline{K_{2}}$ gives the disjoint union $G_{1} ⊔ G_{2}$ .

Facts & Assumptions

Given: Nonnull graphs $G_{1}$ and $G_{2}$ whose vertex sets are disjoint from each other and from ${x, y}$ , the complete graph $K_{2}$ on vertices $x, y$ , and the edgeless graph $\overline{K_{2}}$ on the same vertex set.

[L1]

Substituting a graph for a vertex replaces that vertex by the inserted graph and joins every outside vertex to all of it or none of it according to the original adjacency (Substituting one graph for a vertex of another).

Verification

technique · direct

1.1

First substitute $G_{1}$ for $x$ , leaving $y$ as a one-vertex part, and then substitute $G_{2}$ for $y$ . Since $x$ and $y$ are adjacent in $K_{2}$ , [L1] makes every vertex of $G_{1}$ adjacent to every vertex of $G_{2}$ , while preserving the edges internal to both graphs. The result is exactly $G_{1} \lor G_{2}$ .

L1given

1.2

Carrying out the same two substitutions in $\overline{K_{2}}$ leaves the two copied vertex sets anticomplete because $x$ and $y$ are nonadjacent. The result is exactly $G_{1} ⊔ G_{2}$ .

L1given

2.1

Thus join and disjoint union are the two binary substitutions obtained from the edge and the nonedge templates.

step 1.1step 1.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

12 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Substituting into K2K2​ gives the join and substituting into K2‾K2​​ gives the disjoint union