Source / pinned edition
arxo.metamath_dependencies
Source of package arxo.metamath_dependencies · sha256:e51d1b0375eda65630235827afcbc620cc3324cf7cfdbf2c4b2676c0d8aec146
- work
- urn:arxo:arxo.metamath_dependencies#Import_Source_1900eab6c028483d7126599ee6f50de0d27907b5c65fa90524580b4b0f9852b0
- number
- sha256:e51d1b0375eda65630235827afcbc620cc3324cf7cfdbf2c4b2676c0d8aec146
- kind
- urn:arxo:arxo.metamath_dependencies#treatise
Import_Edition_1900eab6c028483d7126599ee6f50de0d27907b5c65fa90524580b4b0f9852b0
- edition
- urn:arxo:arxo.metamath_dependencies#Import_Edition_1900eab6c028483d7126599ee6f50de0d27907b5c65fa90524580b4b0f9852b0
- language
- en
- officiality
- unofficial
- materialisation
- PINNED_UNOFFICIAL_COPY
- life cycle
- —
Publications
| URI | Type | documentHash | Retrieved |
|---|---|---|---|
| urn:arxo:metamath:reviewed-profile:sha256:125830e009b5f9d1c9ad68c5bc3fe4a5299d53e86aee1ce186bf6521bee04916 | text/plain; charset=utf-8 | sha256:46c4f549fe5d0b72198f0eec3efc6dd611dfae6749f681c79b504a3d97ec5d99 | 2026-09-17T12:30:00Z |
Fragments — 3
/rules/DependsTransitive · lemma · referenced by: 1
en · unofficial · sha256:8c188ce81ed57cd19b3ec9e84ad1fcdbecfcca74aecad5a93d47cbece1f96ce1
{
"parameters": {"a": "Statement", "b": "Statement", "c": "Statement"},
"premises": [["proof_reference", ["a", "b"]], ["depends_on", ["b", "c"]]],
"conclusion": ["depends_on", ["a", "c"]]
}Referencing norms: Import_Rule_a06360149446ee7ec2ead1a67bc06e165c5e92916759b9bc7eb190efd57c7661
/rules/UsesAxiom · lemma · referenced by: 1
en · unofficial · sha256:805923f1c919096e5e1d9accb3144a93519c58c99179ff725c86d34ba9f3ba54
{
"parameters": {"a": "Statement", "x": "Statement"},
"premises": [["depends_on", ["a", "x"]], ["statement_axiom", ["x"]]],
"conclusion": ["uses_axiom", ["a", "x"]]
}Referencing norms: Import_Rule_00e8f5254e94fa514ce2ce0fbb8577e08766e63b780a3949afe0cf9a0c54c876
/rules/DependsFromProof · lemma · referenced by: 1
en · unofficial · sha256:d61b01f44a16780f4cdfa911d09f8a0fd27d0e006c278df7752433ce76d65d74
{
"parameters": {"a": "Statement", "b": "Statement"},
"premises": [["proof_reference", ["a", "b"]]],
"conclusion": ["depends_on", ["a", "b"]]
}Referencing norms: Import_Rule_9d1bda6637da77e36777944fe20dfa4e58525052410556122f8d9d1d0f7adc24
The hash beside the text is the sha256 of its exact bytes. It is the check that the text shown matches the one pinned in the package: a divergence fails the oracle’s static analysis.