Blueprint Summary
Overview
Total entries126completed: 126; deps incomplete: 0; sorries: 0; no proof: 0
Ready now0Entries with an actionable next formalization step.
Fully closed126Local code and prerequisite closure are both complete.
Actionable priorities0Entries ready now and already unlocking downstream work.
Missing informal coverage90Entries with Lean code but missing an informal statement or proof block.
Missing informal coverage (90)
-
Associated lean decls (2)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (4)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (5)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (3)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (3)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (4)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (12)
-
Bigraph.Logic.Compose.closeBridge' -
Bigraph.Logic.Compose.CloseBridgeStatement' -
Bigraph.Logic.Compose.closeBridge_faceOk -
Bigraph.Logic.Compose.closeBridge_ground -
Bigraph.Logic.Compose.closeBridge_ground_nodup -
Bigraph.Logic.Compose.hidden_disjoint -
Bigraph.Logic.Compose.hidden_inj -
Bigraph.Logic.Compose.close_fits -
Bigraph.Logic.Compose.closeBridge_refuted -
Bigraph.Logic.Compose.CloseBridgeStatement -
Bigraph.Logic.Compose.Inst.closeBridge_a2 -
Bigraph.Logic.Compose.Inst.closeBridge_ground_a2
-
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (4)
-
Associated lean decls (4)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (9)
-
Bigraph.Logic.OccPreserve.occTrack_param -
Bigraph.Logic.OccPreserve.kept_ctrl -
Bigraph.Logic.OccPreserve.kept_link -
Bigraph.Logic.OccPreserve.kept_parOf_node -
Bigraph.Logic.OccPreserve.param_parOf_root -
Bigraph.Logic.OccPreserve.kept_parOf_root -
Bigraph.Logic.OccPreserve.result_kept_at -
Bigraph.Logic.OccPreserve.kept_at_ctrl -
Bigraph.Logic.OccPreserve.kept_at_parOf
-
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (3)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
Entry index (126)
Definitions36completed: 36; deps incomplete: 0; sorries: 0; no proof: 0
Lemmas1completed: 1; deps incomplete: 0; sorries: 0; no proof: 0
Theorems89completed: 89; deps incomplete: 0; sorries: 0; no proof: 0
Definition Index (36)
-
Associated lean decls (4)
-
Associated lean decls (3)
-
Associated lean decls (6)
-
Associated lean decls (6)
-
Associated lean decls (4)
-
Associated lean decls (4)
-
Associated lean decls (3)
-
Associated lean decls (4)
-
Associated lean decls (4)
-
Associated lean decls (4)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (3)
-
Associated lean decls (4)
-
Associated lean decls (5)
-
Associated lean decls (3)
-
Associated lean decls (5)
-
Associated lean decls (2)
-
Associated lean decls (3)
-
Associated lean decls (3)
-
Associated lean decls (3)
-
Associated lean decls (5)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (4)
-
Associated lean decls (3)
Theorem / Proposition / Lemma / Corollary Index (90)
-
Associated lean decls (2)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (4)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (5)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (3)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (3)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (4)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (12)
-
Bigraph.Logic.Compose.closeBridge' -
Bigraph.Logic.Compose.CloseBridgeStatement' -
Bigraph.Logic.Compose.closeBridge_faceOk -
Bigraph.Logic.Compose.closeBridge_ground -
Bigraph.Logic.Compose.closeBridge_ground_nodup -
Bigraph.Logic.Compose.hidden_disjoint -
Bigraph.Logic.Compose.hidden_inj -
Bigraph.Logic.Compose.close_fits -
Bigraph.Logic.Compose.closeBridge_refuted -
Bigraph.Logic.Compose.CloseBridgeStatement -
Bigraph.Logic.Compose.Inst.closeBridge_a2 -
Bigraph.Logic.Compose.Inst.closeBridge_ground_a2
-
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (4)
-
Associated lean decls (4)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (9)
-
Bigraph.Logic.OccPreserve.occTrack_param -
Bigraph.Logic.OccPreserve.kept_ctrl -
Bigraph.Logic.OccPreserve.kept_link -
Bigraph.Logic.OccPreserve.kept_parOf_node -
Bigraph.Logic.OccPreserve.param_parOf_root -
Bigraph.Logic.OccPreserve.kept_parOf_root -
Bigraph.Logic.OccPreserve.result_kept_at -
Bigraph.Logic.OccPreserve.kept_at_ctrl -
Bigraph.Logic.OccPreserve.kept_at_parOf
-
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (3)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
Dependency insights
Statement-used entries73Entries reused in statement dependencies.
Most used in statements (73)
-
Reverse dependencies recorded in statement dependencies.statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 26
Associated lean decls (4)
-
Reverse dependencies recorded in statement dependencies.statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 18
Associated lean decls (5)
-
Reverse dependencies recorded in statement dependencies.statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 13
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 16
Associated lean decls (4)
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 11
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 9
-
Reverse dependencies recorded in statement dependencies.statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 6
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 14
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 10
Associated lean decls (4)
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 8
Associated lean decls (3)
-
Show all 63 more statement-used entries
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 8
Associated lean decls (5)
-
Reverse dependencies recorded in statement dependencies.statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 4
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 19
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 12
Associated lean decls (4)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 12
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 7
Associated lean decls (4)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 7
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 4
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 3
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 15
Associated lean decls (4)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 8
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 8
Associated lean decls (4)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 6
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 6
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 4
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
Associated lean decls (5)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
Associated lean decls (4)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 19
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 19
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 10
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 9
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
Associated lean decls (6)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (4)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (2)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (6)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (3)
-
Reverse dependencies recorded in statement dependencies.statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (3)
-
Metadata
Tags in use5Distinct tags currently attached to blueprint entries.
Tag rollups (5)
-
tag: newentries: 21actionable: 0quick wins: 0linked PRs: 0
-
tag: from sourceentries: 18actionable: 0quick wins: 0linked PRs: 0
-
tag: bridgedentries: 12actionable: 0quick wins: 0linked PRs: 0
-
tag: not auditedentries: 9actionable: 0quick wins: 0linked PRs: 0
-
tag: unbridgedentries: 6actionable: 0quick wins: 0linked PRs: 0
Metadata audit
Missing owner126
Missing effort126
Untagged90
Missing owner (126)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.tag: from sourcetag: bridgedtag: unbridged
Associated lean decls (4)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.tag: from source
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Show all 116 more entries missing owner
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.tag: from source
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.tag: from sourcetag: new
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.tag: unbridgedtag: new
Associated lean decls (5)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.tag: from source
-
Missing owner metadata.tag: from sourcetag: new
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.tag: from sourcetag: newtag: not audited
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.tag: from sourcetag: not audited
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.tag: from sourcetag: bridgedtag: new
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.tag: from sourcetag: not audited
Associated lean decls (4)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.tag: from source
Associated lean decls (4)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.tag: newtag: not audited
Associated lean decls (4)
-
Missing owner metadata.tag: from source
Associated lean decls (4)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (4)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (4)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.tag: from source
Associated lean decls (4)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.tag: bridgedtag: not audited
-
Missing owner metadata.
-
Missing owner metadata.tag: bridged
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.tag: new
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (9)
-
Bigraph.Logic.OccPreserve.occTrack_param -
Bigraph.Logic.OccPreserve.kept_ctrl -
Bigraph.Logic.OccPreserve.kept_link -
Bigraph.Logic.OccPreserve.kept_parOf_node -
Bigraph.Logic.OccPreserve.param_parOf_root -
Bigraph.Logic.OccPreserve.kept_parOf_root -
Bigraph.Logic.OccPreserve.result_kept_at -
Bigraph.Logic.OccPreserve.kept_at_ctrl -
Bigraph.Logic.OccPreserve.kept_at_parOf
-
-
Missing owner metadata.
-
Missing owner metadata.tag: bridgedtag: not audited
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (4)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.tag: unbridgedtag: new
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.tag: bridgedtag: new
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.tag: new
-
Missing owner metadata.
Associated lean decls (4)
-
Missing owner metadata.tag: new
Associated lean decls (6)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.tag: bridgedtag: unbridgedtag: new
Associated lean decls (4)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.tag: new
Associated lean decls (6)
-
Missing owner metadata.
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.tag: from sourcetag: new
Associated lean decls (2)
-
Missing owner metadata.tag: from sourcetag: bridgedtag: unbridged
-
Missing owner metadata.tag: from sourcetag: new
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (5)
-
Missing owner metadata.tag: from source
Associated lean decls (5)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.tag: bridgedtag: new
Associated lean decls (4)
-
Missing owner metadata.
Associated lean decls (12)
-
Bigraph.Logic.Compose.closeBridge' -
Bigraph.Logic.Compose.CloseBridgeStatement' -
Bigraph.Logic.Compose.closeBridge_faceOk -
Bigraph.Logic.Compose.closeBridge_ground -
Bigraph.Logic.Compose.closeBridge_ground_nodup -
Bigraph.Logic.Compose.hidden_disjoint -
Bigraph.Logic.Compose.hidden_inj -
Bigraph.Logic.Compose.close_fits -
Bigraph.Logic.Compose.closeBridge_refuted -
Bigraph.Logic.Compose.CloseBridgeStatement -
Bigraph.Logic.Compose.Inst.closeBridge_a2 -
Bigraph.Logic.Compose.Inst.closeBridge_ground_a2
-
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.tag: from sourcetag: unbridgedtag: new
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.tag: newtag: not audited
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
-
Missing owner metadata.tag: bridgedtag: new
Associated lean decls (5)
-
Missing owner metadata.tag: bridgedtag: not audited
-
Missing owner metadata.
-
Missing owner metadata.tag: newtag: not audited
-
Missing owner metadata.
Associated lean decls (3)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing owner metadata.tag: bridgedtag: new
Associated lean decls (2)
-
Missing owner metadata.
Associated lean decls (1)
-
Missing effort (126)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.tag: from sourcetag: bridgedtag: unbridged
Associated lean decls (4)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.tag: from source
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Show all 116 more entries missing effort
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.tag: from source
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.tag: from sourcetag: new
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.tag: unbridgedtag: new
Associated lean decls (5)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.tag: from source
-
Missing effort metadata.tag: from sourcetag: new
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.tag: from sourcetag: newtag: not audited
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.tag: from sourcetag: not audited
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.tag: from sourcetag: bridgedtag: new
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.tag: from sourcetag: not audited
Associated lean decls (4)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.tag: from source
Associated lean decls (4)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.tag: newtag: not audited
Associated lean decls (4)
-
Missing effort metadata.tag: from source
Associated lean decls (4)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (4)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (4)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.tag: from source
Associated lean decls (4)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.tag: bridgedtag: not audited
-
Missing effort metadata.
-
Missing effort metadata.tag: bridged
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.tag: new
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (9)
-
Bigraph.Logic.OccPreserve.occTrack_param -
Bigraph.Logic.OccPreserve.kept_ctrl -
Bigraph.Logic.OccPreserve.kept_link -
Bigraph.Logic.OccPreserve.kept_parOf_node -
Bigraph.Logic.OccPreserve.param_parOf_root -
Bigraph.Logic.OccPreserve.kept_parOf_root -
Bigraph.Logic.OccPreserve.result_kept_at -
Bigraph.Logic.OccPreserve.kept_at_ctrl -
Bigraph.Logic.OccPreserve.kept_at_parOf
-
-
Missing effort metadata.
-
Missing effort metadata.tag: bridgedtag: not audited
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (4)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.tag: unbridgedtag: new
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.tag: bridgedtag: new
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.tag: new
-
Missing effort metadata.
Associated lean decls (4)
-
Missing effort metadata.tag: new
Associated lean decls (6)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.tag: bridgedtag: unbridgedtag: new
Associated lean decls (4)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.tag: new
Associated lean decls (6)
-
Missing effort metadata.
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.tag: from sourcetag: new
Associated lean decls (2)
-
Missing effort metadata.tag: from sourcetag: bridgedtag: unbridged
-
Missing effort metadata.tag: from sourcetag: new
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (5)
-
Missing effort metadata.tag: from source
Associated lean decls (5)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.tag: bridgedtag: new
Associated lean decls (4)
-
Missing effort metadata.
Associated lean decls (12)
-
Bigraph.Logic.Compose.closeBridge' -
Bigraph.Logic.Compose.CloseBridgeStatement' -
Bigraph.Logic.Compose.closeBridge_faceOk -
Bigraph.Logic.Compose.closeBridge_ground -
Bigraph.Logic.Compose.closeBridge_ground_nodup -
Bigraph.Logic.Compose.hidden_disjoint -
Bigraph.Logic.Compose.hidden_inj -
Bigraph.Logic.Compose.close_fits -
Bigraph.Logic.Compose.closeBridge_refuted -
Bigraph.Logic.Compose.CloseBridgeStatement -
Bigraph.Logic.Compose.Inst.closeBridge_a2 -
Bigraph.Logic.Compose.Inst.closeBridge_ground_a2
-
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.tag: from sourcetag: unbridgedtag: new
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.tag: newtag: not audited
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
-
Missing effort metadata.tag: bridgedtag: new
Associated lean decls (5)
-
Missing effort metadata.tag: bridgedtag: not audited
-
Missing effort metadata.
-
Missing effort metadata.tag: newtag: not audited
-
Missing effort metadata.
Associated lean decls (3)
-
Missing effort metadata.
Associated lean decls (1)
-
Missing effort metadata.tag: bridgedtag: new
Associated lean decls (2)
-
Missing effort metadata.
Associated lean decls (1)
-
Untagged (90)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (2)
-
Show all 80 more untagged entries
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (4)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (4)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (9)
-
Bigraph.Logic.OccPreserve.occTrack_param -
Bigraph.Logic.OccPreserve.kept_ctrl -
Bigraph.Logic.OccPreserve.kept_link -
Bigraph.Logic.OccPreserve.kept_parOf_node -
Bigraph.Logic.OccPreserve.param_parOf_root -
Bigraph.Logic.OccPreserve.kept_parOf_root -
Bigraph.Logic.OccPreserve.result_kept_at -
Bigraph.Logic.OccPreserve.kept_at_ctrl -
Bigraph.Logic.OccPreserve.kept_at_parOf
-
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (4)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (4)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (5)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (12)
-
Bigraph.Logic.Compose.closeBridge' -
Bigraph.Logic.Compose.CloseBridgeStatement' -
Bigraph.Logic.Compose.closeBridge_faceOk -
Bigraph.Logic.Compose.closeBridge_ground -
Bigraph.Logic.Compose.closeBridge_ground_nodup -
Bigraph.Logic.Compose.hidden_disjoint -
Bigraph.Logic.Compose.hidden_inj -
Bigraph.Logic.Compose.close_fits -
Bigraph.Logic.Compose.closeBridge_refuted -
Bigraph.Logic.Compose.CloseBridgeStatement -
Bigraph.Logic.Compose.Inst.closeBridge_a2 -
Bigraph.Logic.Compose.Inst.closeBridge_ground_a2
-
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (2)
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
-
Missing tag metadata.
-
Missing tag metadata.
Associated lean decls (3)
-
Missing tag metadata.
Associated lean decls (1)
-
Missing tag metadata.
Associated lean decls (1)
-
Structure and coverage
Fully closed126Local code and ancestor closure are both complete.
Heaviest prerequisites (111)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 3statement deps: 3proof deps: 0direct uses: 2downstream unlocks: 3
-
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 (1)
-
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 (1)
-
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 (2)
-
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 (2)
-
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 (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 3
Associated lean decls (5)
-
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 (1)
-
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 (1)
-
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 (3)
-
Show all 101 more heaviest-prerequisite entries
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 6
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 3
-
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 (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
-
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)
-
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 (3)
-
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)
-
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 (3)
-
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)
-
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 (2)
-
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)
-
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)
-
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 (2)
-
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 (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 7
Associated lean decls (4)
-
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 (2)
-
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 (6)
-
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 (3)
-
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 (1)
-
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)
-
Bigraph.Logic.Compose.closeBridge' -
Bigraph.Logic.Compose.CloseBridgeStatement' -
Bigraph.Logic.Compose.closeBridge_faceOk -
Bigraph.Logic.Compose.closeBridge_ground -
Bigraph.Logic.Compose.closeBridge_ground_nodup -
Bigraph.Logic.Compose.hidden_disjoint -
Bigraph.Logic.Compose.hidden_inj -
Bigraph.Logic.Compose.close_fits -
Bigraph.Logic.Compose.closeBridge_refuted -
Bigraph.Logic.Compose.CloseBridgeStatement -
Bigraph.Logic.Compose.Inst.closeBridge_a2 -
Bigraph.Logic.Compose.Inst.closeBridge_ground_a2
-
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 4
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 4
Associated lean decls (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 6downstream unlocks: 18
Associated lean decls (5)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 2
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 3
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 6
Associated lean decls (1)
-
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)
-
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)
-
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)
-
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)
-
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)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 4
Associated lean decls (1)
-
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)
-
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)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 2
Associated lean decls (3)
-
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)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 8
Associated lean decls (3)
-
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)
-
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 (1)
-
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 (3)
-
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 (3)
-
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)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 8
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 3
-
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)
-
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)
-
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)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 8
Associated lean decls (4)
-
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)
-
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)
-
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 (3)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 12
Associated lean decls (2)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
-
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)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
-
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)
-
Bigraph.Logic.OccPreserve.occTrack_param -
Bigraph.Logic.OccPreserve.kept_ctrl -
Bigraph.Logic.OccPreserve.kept_link -
Bigraph.Logic.OccPreserve.kept_parOf_node -
Bigraph.Logic.OccPreserve.param_parOf_root -
Bigraph.Logic.OccPreserve.kept_parOf_root -
Bigraph.Logic.OccPreserve.result_kept_at -
Bigraph.Logic.OccPreserve.kept_at_ctrl -
Bigraph.Logic.OccPreserve.kept_at_parOf
-
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
-
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 (3)
-
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 (1)
-
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)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 6downstream unlocks: 13
Associated lean decls (3)
-
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)
-
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 (1)
-
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)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 7
Associated lean decls (2)
-
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 (1)
-
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 (1)
-
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 (1)
-
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 (4)
-
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 (6)
-
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)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 15
Associated lean decls (4)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 2
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 9
Associated lean decls (2)
-
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 (5)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 8
Associated lean decls (5)
-
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)
-
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)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 2
Associated lean decls (1)
-
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 (1)
-
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)
-
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 (1)
-
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)
-
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 (3)
-
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)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 19
Associated lean decls (2)
-
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)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 3
Associated lean decls (2)
-
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)
-
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)
-
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)
-
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)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 19
Associated lean decls (2)
-
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 (3)
-
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)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 4
Associated lean decls (1)
-
Prerequisite fan-in measured from the current statement/proof dependency graph.total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 4
Associated lean decls (2)
-
No prerequisites (15)
-
Associated lean decls (4)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (4)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (4)
-
Show all 5 more entries without prerequisites
-
Associated lean decls (4)
-
Associated lean decls (3)
-
Associated lean decls (4)
No dependents (53)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (4)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (5)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (3)
-
Show all 43 more entries without dependents
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (4)
-
Associated lean decls (2)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (9)
-
Bigraph.Logic.OccPreserve.occTrack_param -
Bigraph.Logic.OccPreserve.kept_ctrl -
Bigraph.Logic.OccPreserve.kept_link -
Bigraph.Logic.OccPreserve.kept_parOf_node -
Bigraph.Logic.OccPreserve.param_parOf_root -
Bigraph.Logic.OccPreserve.kept_parOf_root -
Bigraph.Logic.OccPreserve.result_kept_at -
Bigraph.Logic.OccPreserve.kept_at_ctrl -
Bigraph.Logic.OccPreserve.kept_at_parOf
-
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (3)
-
Associated lean decls (12)
-
Bigraph.Logic.Compose.closeBridge' -
Bigraph.Logic.Compose.CloseBridgeStatement' -
Bigraph.Logic.Compose.closeBridge_faceOk -
Bigraph.Logic.Compose.closeBridge_ground -
Bigraph.Logic.Compose.closeBridge_ground_nodup -
Bigraph.Logic.Compose.hidden_disjoint -
Bigraph.Logic.Compose.hidden_inj -
Bigraph.Logic.Compose.close_fits -
Bigraph.Logic.Compose.closeBridge_refuted -
Bigraph.Logic.Compose.CloseBridgeStatement -
Bigraph.Logic.Compose.Inst.closeBridge_a2 -
Bigraph.Logic.Compose.Inst.closeBridge_ground_a2
-
-
Associated lean decls (2)
-
Associated lean decls (1)
-
Associated lean decls (4)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (2)
-
Associated lean decls (3)
-
Associated lean decls (3)
-
Associated lean decls (2)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (3)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (1)
-
Associated lean decls (3)