arxo.order_composition

en · unofficial · sha256:30f35c587509a19bcfedb33d57ab4a3f64c7b9405df4ad5b867fea085c827f30EN

{"composition":{"conclusion":{"args":["o","a","d"],"predicate":"urn:arxo:arxo.order#strictly_before"},"links":[{"consumer":1,"producer":0}],"output":"jointly_supported_strict_chain","package":{"name":"arxo.order_composition","namespace":"urn:arxo:arxo.order_composition","version":"0.1.0"},"parameters":[{"id":"o","type_symbol":"Order"},{"id":"a","type_symbol":"Element"},{"id":"b","type_symbol":"Element"},{"id":"c","type_symbol":"Element"},{"id":"d","type_symbol":"Element"}],"sources":{"isabelle":{"policy":"isabelle-policy.json","recipe":"isabelle-recipe.json"},"lean":{"policy":"lean-policy.json","recipe":"lean-recipe.json"}},"steps":[{"args":["o","a","b","c"],"declaration":"le_trans","source":"lean"},{"args":["o","a","c","d"],"declaration":"Orderings.preorder_class.le_less_trans","source":"isabelle"}],"vocabulary":"arxo.order"},"reports":{"isabelle":{"decisions":[{"alternatives":[{"reason":"structurally_compatible_under_interpretation","target":"urn:arxo:arxo.order#StrictImpliesWeak"},{"reason":"target variable/type count differs","target":"urn:arxo:arxo.order#WeakTransitivity"}],"conditions":{"all_source_conditions_retained":true,"interpretation_basis":"declared_mapping_assumption","interpretation_hash":"sha256:a6ba7de62a0f9c9b3d555bbc03f7db772fa110f2f9ed055ec4f5a30e72be9fed","semantic_equivalence_proved":false,"source_shape":{"head":["urn:arxo:arxo.order#before_or_equal",[0,1,2]],"premise_mode":"supported","premises":[["urn:arxo:arxo.order#preorder_structure",[0]],["urn:arxo:arxo.order#in_carrier",[0,1]],["urn:arxo:arxo.order#in_carrier",[0,2]],["urn:arxo:arxo.order#strictly_before",[0,1,2]]],"types":["urn:arxo:arxo.order#Order","urn:arxo:arxo.order#Element","urn:arxo:arxo.order#Element"]}},"direction":"source_to_target_under_interpretation","evidence":{"source":[{"anchor":"Orderings.preorder_class.less_imp_le","declaration":"Orderings.preorder_class.less_imp_le","document":"src/HOL/Orderings.thy","document_hash":"sha256:9504399a7e06d858a65fb2c0e2613ffe33d1b179fe7a203eb5b4d90b9fd10406","end":9308,"locator":"Orderings.preorder_class.less_imp_le","start":9254}],"target":[{"anchors":["urn:arxo:arxo.order#ORDER_CONTRACT"],"binder_map":[2,0,1],"package":"arxo.order","rule":"urn:arxo:arxo.order#StrictImpliesWeak","rule_hash":"sha256:bf2d373b969f7d5eaa922e8ff3923dbba62b781c9d7976a99b60733d2522940a","shape":{"head":["urn:arxo:arxo.order#before_or_equal",[1,2,0]],"premise_mode":"supported","premises":[["urn:arxo:arxo.order#strictly_before",[1,2,0]],["urn:arxo:arxo.order#preorder_structure",[1]],["urn:arxo:arxo.order#in_carrier",[1,2]],["urn:arxo:arxo.order#in_carrier",[1,0]]],"types":["urn:arxo:arxo.order#Element","urn:arxo:arxo.order#Order","urn:arxo:arxo.order#Element"]}}]},"id":"sha256:3a9ac9ff49edf677c31208fa472a1dabde8eadb7e4581dd75c563e3687a9d1f4","output":"supported_d7f7657f6e55615a91c9c02daa264114e1e11bbf2b338953074bacd124f339ca","parameters":[{"id":"Orderings.preorder_class.less_imp_le/carrier","type_symbol":"SortedCarrier"},{"id":"Orderings.preorder_class.less_imp_le/var/0","type_symbol":"CarrierElement"},{"id":"Orderings.preorder_class.less_imp_le/var/1","type_symbol":"CarrierElement"}],"reasons":[],"relation":"conditional_rule_implementation","source":"Orderings.preorder_class.less_imp_le","status":"accepted","target":"urn:arxo:arxo.order#StrictImpliesWeak"},{"alternatives":[{"reason":"structurally_compatible_under_interpretation","target":"urn:arxo:arxo.order#StrictTransitivity"},{"reason":"target condition absent from source under a consistent binder map","target":"urn:arxo:arxo.order#WeakThenStrict"}],"conditions":{"all_source_conditions_retained":true,"interpretation_basis":"declared_mapping_assumption","interpretation_hash":"sha256:a6ba7de62a0f9c9b3d555bbc03f7db772fa110f2f9ed055ec4f5a30e72be9fed","semantic_equivalence_proved":false,"source_shape":{"head":["urn:arxo:arxo.order#strictly_before",[0,1,3]],"premise_mode":"supported","premises":[["urn:arxo:arxo.order#preorder_structure",[0]],["urn:arxo:arxo.order#in_carrier",[0,1]],["urn:arxo:arxo.order#in_carrier",[0,2]],["urn:arxo:arxo.order#in_carrier",[0,3]],["urn:arxo:arxo.order#strictly_before",[0,1,2]],["urn:arxo:arxo.order#strictly_before",[0,2,3]]],"types":["urn:arxo:arxo.order#Order","urn:arxo:arxo.order#Element","urn:arxo:arxo.order#Element","urn:arxo:arxo.order#Element"]}},"direction":"source_to_target_under_interpretation","evidence":{"source":[{"anchor":"Orderings.preorder_class.less_trans","declaration":"Orderings.preorder_class.less_trans","document":"src/HOL/Orderings.thy","document_hash":"sha256:9504399a7e06d858a65fb2c0e2613ffe33d1b179fe7a203eb5b4d90b9fd10406","end":9722,"locator":"Orderings.preorder_class.less_trans","start":9649}],"target":[{"anchors":["urn:arxo:arxo.order#ORDER_CONTRACT"],"binder_map":[0,1,2,3],"package":"arxo.order","rule":"urn:arxo:arxo.order#StrictTransitivity","rule_hash":"sha256:5090adef5b8d1489d0ddd91302c2ad62c57f50c615e85de4c70851c865d2319f","shape":{"head":["urn:arxo:arxo.order#strictly_before",[0,1,3]],"premise_mode":"supported","premises":[["urn:arxo:arxo.order#in_carrier",[0,2]],["urn:arxo:arxo.order#strictly_before",[0,2,3]],["urn:arxo:arxo.order#strictly_before",[0,1,2]],["urn:arxo:arxo.order#preorder_structure",[0]],["urn:arxo:arxo.order#in_carrier",[0,3]],["urn:arxo:arxo.order#in_carrier",[0,1]]],"types":["urn:arxo:arxo.order#Order","urn:arxo:arxo.order#Element","urn:arxo:arxo.order#Element","urn:arxo:arxo.order#Element"]}}]},"id":"sha256:50bc92ec5f62262e494bac475a39b971a5a1b5cff63d9236ecc3a9ba97fead88","output":"supported_ba9f606b3dfff6f0efb044b968493c82752c7719f3ec01a66d852f23de4aa087","parameters":[{"id":"Orderings.preorder_class.less_trans/carrier","type_symbol":"SortedCarrier"},{"id":"Orderings.preorder_class.less_trans/var/0","type_symbol":"CarrierElement"},{"id":"Orderings.preorder_class.less_trans/var/1","type_symbol":"CarrierElement"},{"id":"Orderings.preorder_class.less_trans/var/2","type_symbol":"CarrierElement"}],"reasons":[],"relation":"conditional_rule_implementation","source":"Orderings.preorder_class.less_trans","status":"accepted","target":"urn:arxo:arxo.order#StrictTransitivity"},{"alternatives":[{"reason":"target condition absent from source under a consistent binder map","target":"urn:arxo:arxo.order#StrictTransitivity"},{"reason":"structurally_compatible_under_interpretation","target":"urn:arxo:arxo.order#WeakThenStrict"}],"conditions":{"all_source_conditions_retained":true,"interpretation_basis":"declared_mapping_assumption","interpretation_hash":"sha256:a6ba7de62a0f9c9b3d555bbc03f7db772fa110f2f9ed055ec4f5a30e72be9fed","semantic_equivalence_proved":false,"source_shape":{"head":["urn:arxo:arxo.order#strictly_before",[0,1,3]],"premise_mode":"supported","premises":[["urn:arxo:arxo.order#preorder_structure",[0]],["urn:arxo:arxo.order#in_carrier",[0,1]],["urn:arxo:arxo.order#in_carrier",[0,2]],["urn:arxo:arxo.order#in_carrier",[0,3]],["urn:arxo:arxo.order#before_or_equal",[0,1,2]],["urn:arxo:arxo.order#strictly_before",[0,2,3]]],"types":["urn:arxo:arxo.order#Order","urn:arxo:arxo.order#Element","urn:arxo:arxo.order#Element","urn:arxo:arxo.order#Element"]}},"direction":"source_to_target_under_interpretation","evidence":{"source":[{"anchor":"Orderings.preorder_class.le_less_trans","declaration":"Orderings.preorder_class.le_less_trans","document":"src/HOL/Orderings.thy","document_hash":"sha256:9504399a7e06d858a65fb2c0e2613ffe33d1b179fe7a203eb5b4d90b9fd10406","end":9858,"locator":"Orderings.preorder_class.le_less_trans","start":9778}],"target":[{"anchors":["urn:arxo:arxo.order#ORDER_CONTRACT"],"binder_map":[3,2,0,1],"package":"arxo.order","rule":"urn:arxo:arxo.order#WeakThenStrict","rule_hash":"sha256:00f31692b27134b241ca1f0a4c5b023864934a160d8570868d82ac436b6c551d","shape":{"head":["urn:arxo:arxo.order#strictly_before",[2,3,0]],"premise_mode":"supported","premises":[["urn:arxo:arxo.order#before_or_equal",[2,3,1]],["urn:arxo:arxo.order#in_carrier",[2,0]],["urn:arxo:arxo.order#in_carrier",[2,1]],["urn:arxo:arxo.order#preorder_structure",[2]],["urn:arxo:arxo.order#in_carrier",[2,3]],["urn:arxo:arxo.order#strictly_before",[2,1,0]]],"types":["urn:arxo:arxo.order#Element","urn:arxo:arxo.order#Element","urn:arxo:arxo.order#Order","urn:arxo:arxo.order#Element"]}}]},"id":"sha256:cf7c23306a665bc0ff3fc08fffff0bd96bd3f400ad65990bf0a58da580b5d646","output":"supported_2bbcae2cd2f015a5e79d256e59269689eaf32b8a5d2cff20c1e8029f9dbec088","parameters":[{"id":"Orderings.preorder_class.le_less_trans/carrier","type_symbol":"SortedCarrier"},{"id":"Orderings.preorder_class.le_less_trans/var/0","type_symbol":"CarrierElement"},{"id":"Orderings.preorder_class.le_less_trans/var/1","type_symbol":"CarrierElement"},{"id":"Orderings.preorder_class.le_less_trans/var/2","type_symbol":"CarrierElement"}],"reasons":[],"relation":"conditional_rule_implementation","source":"Orderings.preorder_class.le_less_trans","status":"accepted","target":"urn:arxo:arxo.order#WeakThenStrict"}],"discovery":{"channel":"declared_mapping_and_rule_structure","complete":true,"source":"sha256:cff8c2424e95c34e999dc5272b53ebaafcf5bdcfea02b08f74626805fc998d6b","source_declarations":3,"target_rules":6,"targets":{"arxo.order":"sha256:8869ba90876ca91af3ec11c64b90a51c76f7931e886451cc213ebe832d7f6c68"}},"format":"arxo.concept-rule-alignment.report/0.1","policy":{"enabled":true,"format":"arxo.concept-rule-alignment.policy/0.1","interpretation_basis":"declared_mapping_assumption","interpretation_hash":"sha256:a6ba7de62a0f9c9b3d555bbc03f7db772fa110f2f9ed055ec4f5a30e72be9fed","package":{"name":"isabelle.order","namespace":"urn:arxo:isabelle.order","version":"0.1.0"},"profile":"isabelle-order-conditional-rules/0.1","projection_hash":"sha256:20804f70b048ce9cd056437d16be955e25f7c5d9d3469a7a8be87bf100ef7e1d","source_project":"isabelle","target_packages":["arxo.order"]},"policy_hash":"sha256:0d84c4c58704a8486bc52f9f097145e56a4d53944e985cfff57bf5f6cb67c17c","previous_hash":null,"profile":"isabelle-order-conditional-rules/0.1","sources":{"native":{"input_hash":"sha256:afbcd9c3b6dbac703d934ee7d2e787e52cd064d678072a2a36cd48aa59c11905","mapping_hash":"sha256:5d2df75f4ca36f03e770e064081df1583c2f3a73161dac860aa0eba843220856","project":"isabelle","revision":"Isabelle2025-2"},"targets":{"arxo.order":{"content_hash":"sha256:dd131bb594e38f5aec813104a2c59b00b90d33725c587ce0745980df7fe44db6","namespace":"urn:arxo:arxo.order","version":"0.1.0"}}},"validator_hash":"sha256:7dd4a739573b8d49a4207cb58706c90141996fb314c9f35165cd3cc584bbe1a6"},"lean":{"decisions":[{"alternatives":[{"reason":"structurally_compatible_under_interpretation","target":"urn:arxo:arxo.order#LinearOrderIsPartialOrder"}],"conditions":{"all_source_conditions_retained":true,"interpretation_basis":"declared_mapping_assumption","interpretation_hash":"sha256:0a9e8f1ffdc76ec22f8c8a09cb5394801ecee7147a340c2f22c32f13e39fac4d","semantic_equivalence_proved":false,"source_shape":{"head":["urn:arxo:arxo.order#partial_order_structure",[0]],"premise_mode":"supported","premises":[["urn:arxo:arxo.order#linear_order_structure",[0]]],"types":["urn:arxo:arxo.order#Order"]}},"direction":"source_to_target_under_interpretation","evidence":{"source":[{"anchor":"LinearOrder.toPartialOrder","declaration":"LinearOrder.toPartialOrder","document":"Mathlib/Order/Defs/LinearOrder.lean","document_hash":"sha256:837dba1e44eb02eb7837e8e7b72b59c277e85899454f45d3be66de44ecd98632","end":3389,"locator":"LinearOrder.toPartialOrder","start":2097}],"target":[{"anchors":["urn:arxo:arxo.order#ORDER_CONTRACT"],"binder_map":[0],"package":"arxo.order","rule":"urn:arxo:arxo.order#LinearOrderIsPartialOrder","rule_hash":"sha256:a371865bca6c3fd9b00b69de0cad6629b0745aecd31b29aa5c5c4d20fa674c3f","shape":{"head":["urn:arxo:arxo.order#partial_order_structure",[0]],"premise_mode":"supported","premises":[["urn:arxo:arxo.order#linear_order_structure",[0]]],"types":["urn:arxo:arxo.order#Order"]}}]},"id":"sha256:22aeb98e3dca72b4f5436967cb0eee630aabde47fd171b0942bac99c612760af","output":"supported_fe781d4b45f1c0e419bffbc13071c03144c7491b558ca2f2bfff627e57c43adc","parameters":[{"id":"LinearOrder.toPartialOrder/parameter/0","type_symbol":"SortedCarrier"}],"reasons":[],"relation":"conditional_rule_implementation","source":"LinearOrder.toPartialOrder","status":"accepted","target":"urn:arxo:arxo.order#LinearOrderIsPartialOrder"},{"alternatives":[{"reason":"structurally_compatible_under_interpretation","target":"urn:arxo:arxo.order#StrictImpliesWeak"},{"reason":"target variable/type count differs","target":"urn:arxo:arxo.order#WeakTransitivity"}],"conditions":{"all_source_conditions_retained":true,"interpretation_basis":"declared_mapping_assumption","interpretation_hash":"sha256:0a9e8f1ffdc76ec22f8c8a09cb5394801ecee7147a340c2f22c32f13e39fac4d","semantic_equivalence_proved":false,"source_shape":{"head":["urn:arxo:arxo.order#before_or_equal",[0,1,2]],"premise_mode":"supported","premises":[["urn:arxo:arxo.order#preorder_structure",[0]],["urn:arxo:arxo.order#in_carrier",[0,1]],["urn:arxo:arxo.order#in_carrier",[0,2]],["urn:arxo:arxo.order#strictly_before",[0,1,2]]],"types":["urn:arxo:arxo.order#Order","urn:arxo:arxo.order#Element","urn:arxo:arxo.order#Element"]}},"direction":"source_to_target_under_interpretation","evidence":{"source":[{"anchor":"le_of_lt","declaration":"le_of_lt","document":"Mathlib/Order/Defs/PartialOrder.lean","document_hash":"sha256:324e420cd942d09b60b6ac8d662b01e29f13f0cd60513e2c4750b3e5676dcf46","end":2709,"locator":"le_of_lt","start":2625}],"target":[{"anchors":["urn:arxo:arxo.order#ORDER_CONTRACT"],"binder_map":[2,0,1],"package":"arxo.order","rule":"urn:arxo:arxo.order#StrictImpliesWeak","rule_hash":"sha256:bf2d373b969f7d5eaa922e8ff3923dbba62b781c9d7976a99b60733d2522940a","shape":{"head":["urn:arxo:arxo.order#before_or_equal",[1,2,0]],"premise_mode":"supported","premises":[["urn:arxo:arxo.order#strictly_before",[1,2,0]],["urn:arxo:arxo.order#preorder_structure",[1]],["urn:arxo:arxo.order#in_carrier",[1,2]],["urn:arxo:arxo.order#in_carrier",[1,0]]],"types":["urn:arxo:arxo.order#Element","urn:arxo:arxo.order#Order","urn:arxo:arxo.order#Element"]}}]},"id":"sha256:7518ca9bf69a1dab886b841a3d0a1a8863349caf8a43819ce8fd0f39379bf690","output":"supported_65b6ecbfa5036509e4685321bf5478f566880e1b5f45e091a8b4bfe4d1134945","parameters":[{"id":"le_of_lt/parameter/0","type_symbol":"SortedCarrier"},{"id":"le_of_lt/parameter/1","type_symbol":"CarrierElement"},{"id":"le_of_lt/parameter/2","type_symbol":"CarrierElement"}],"reasons":[],"relation":"conditional_rule_implementation","source":"le_of_lt","status":"accepted","target":"urn:arxo:arxo.order#StrictImpliesWeak"},{"alternatives":[{"reason":"target variable/type count differs","target":"urn:arxo:arxo.order#StrictImpliesWeak"},{"reason":"structurally_compatible_under_interpretation","target":"urn:arxo:arxo.order#WeakTransitivity"}],"conditions":{"all_source_conditions_retained":true,"interpretation_basis":"declared_mapping_assumption","interpretation_hash":"sha256:0a9e8f1ffdc76ec22f8c8a09cb5394801ecee7147a340c2f22c32f13e39fac4d","semantic_equivalence_proved":false,"source_shape":{"head":["urn:arxo:arxo.order#before_or_equal",[0,1,3]],"premise_mode":"supported","premises":[["urn:arxo:arxo.order#preorder_structure",[0]],["urn:arxo:arxo.order#in_carrier",[0,1]],["urn:arxo:arxo.order#in_carrier",[0,2]],["urn:arxo:arxo.order#in_carrier",[0,3]],["urn:arxo:arxo.order#before_or_equal",[0,1,2]],["urn:arxo:arxo.order#before_or_equal",[0,2,3]]],"types":["urn:arxo:arxo.order#Order","urn:arxo:arxo.order#Element","urn:arxo:arxo.order#Element","urn:arxo:arxo.order#Element"]}},"direction":"source_to_target_under_interpretation","evidence":{"source":[{"anchor":"le_trans","declaration":"le_trans","document":"Mathlib/Order/Defs/PartialOrder.lean","document_hash":"sha256:324e420cd942d09b60b6ac8d662b01e29f13f0cd60513e2c4750b3e5676dcf46","end":2227,"locator":"le_trans","start":2097}],"target":[{"anchors":["urn:arxo:arxo.order#ORDER_CONTRACT"],"binder_map":[0,1,2,3],"package":"arxo.order","rule":"urn:arxo:arxo.order#WeakTransitivity","rule_hash":"sha256:ad50d0ef999613f00a42e5eec706f52c768cc597d376727e271115c43beabf32","shape":{"head":["urn:arxo:arxo.order#before_or_equal",[0,1,3]],"premise_mode":"supported","premises":[["urn:arxo:arxo.order#before_or_equal",[0,2,3]],["urn:arxo:arxo.order#in_carrier",[0,2]],["urn:arxo:arxo.order#before_or_equal",[0,1,2]],["urn:arxo:arxo.order#preorder_structure",[0]],["urn:arxo:arxo.order#in_carrier",[0,3]],["urn:arxo:arxo.order#in_carrier",[0,1]]],"types":["urn:arxo:arxo.order#Order","urn:arxo:arxo.order#Element","urn:arxo:arxo.order#Element","urn:arxo:arxo.order#Element"]}}]},"id":"sha256:c37e5578bf2e12f9752f6e310241b44b6743c7c058f83b4bdd23140f16287537","output":"supported_45030394b40076410bd1334e2484ec6ef2c5dc46054fff2e6e61b63b0d3be99d","parameters":[{"id":"le_trans/parameter/0","type_symbol":"SortedCarrier"},{"id":"le_trans/parameter/1","type_symbol":"CarrierElement"},{"id":"le_trans/parameter/2","type_symbol":"CarrierElement"},{"id":"le_trans/parameter/3","type_symbol":"CarrierElement"}],"reasons":[],"relation":"conditional_rule_implementation","source":"le_trans","status":"accepted","target":"urn:arxo:arxo.order#WeakTransitivity"},{"alternatives":[{"reason":"structurally_compatible_under_interpretation","target":"urn:arxo:arxo.order#PartialOrderIsPreorder"}],"conditions":{"all_source_conditions_retained":true,"interpretation_basis":"declared_mapping_assumption","interpretation_hash":"sha256:0a9e8f1ffdc76ec22f8c8a09cb5394801ecee7147a340c2f22c32f13e39fac4d","semantic_equivalence_proved":false,"source_shape":{"head":["urn:arxo:arxo.order#preorder_structure",[0]],"premise_mode":"supported","premises":[["urn:arxo:arxo.order#partial_order_structure",[0]]],"types":["urn:arxo:arxo.order#Order"]}},"direction":"source_to_target_under_interpretation","evidence":{"source":[{"anchor":"PartialOrder.toPreorder","declaration":"PartialOrder.toPreorder","document":"Mathlib/Order/Defs/PartialOrder.lean","document_hash":"sha256:324e420cd942d09b60b6ac8d662b01e29f13f0cd60513e2c4750b3e5676dcf46","end":6533,"locator":"PartialOrder.toPreorder","start":6406}],"target":[{"anchors":["urn:arxo:arxo.order#ORDER_CONTRACT"],"binder_map":[0],"package":"arxo.order","rule":"urn:arxo:arxo.order#PartialOrderIsPreorder","rule_hash":"sha256:22e06f73c540f88ade4a9f51ee94d270a13fad356fe4a99c1a149f597ae0e509","shape":{"head":["urn:arxo:arxo.order#preorder_structure",[0]],"premise_mode":"supported","premises":[["urn:arxo:arxo.order#partial_order_structure",[0]]],"types":["urn:arxo:arxo.order#Order"]}}]},"id":"sha256:cb430046b1e38484a123fc047a67b89f9c0585a649a14e9095c3cdddee482831","output":"supported_bb8dac886fd22637fdc265b0fba534cd13e058077172a5e831175b34e6e7c5aa","parameters":[{"id":"PartialOrder.toPreorder/parameter/0","type_symbol":"SortedCarrier"}],"reasons":[],"relation":"conditional_rule_implementation","source":"PartialOrder.toPreorder","status":"accepted","target":"urn:arxo:arxo.order#PartialOrderIsPreorder"}],"discovery":{"channel":"declared_mapping_and_rule_structure","complete":true,"source":"sha256:82c75bc7966c92afa6f36d38721e68ded1433a86848fcdd33d686d90ce5d24d1","source_declarations":4,"target_rules":6,"targets":{"arxo.order":"sha256:8869ba90876ca91af3ec11c64b90a51c76f7931e886451cc213ebe832d7f6c68"}},"format":"arxo.concept-rule-alignment.report/0.1","policy":{"enabled":true,"format":"arxo.concept-rule-alignment.policy/0.1","interpretation_basis":"declared_mapping_assumption","interpretation_hash":"sha256:0a9e8f1ffdc76ec22f8c8a09cb5394801ecee7147a340c2f22c32f13e39fac4d","package":{"name":"mathlib.order","namespace":"urn:arxo:mathlib.order","version":"0.1.0"},"profile":"lean-order-conditional-rules/0.1","projection_hash":"sha256:8af8addffe076d95a1edeadab64d58d231d2d9b395b5a9df7ca0d7f1b2ffd663","source_project":"mathlib4","target_packages":["arxo.order"]},"policy_hash":"sha256:81dba6612f4e6763ced5198ea9d59d80ee304a6088f80f9bccecf47cf0d81b77","previous_hash":null,"profile":"lean-order-conditional-rules/0.1","sources":{"native":{"input_hash":"sha256:3b6c350ce58b8dbed4246dca73ba6caa268dd4aed460abdcb9f5576f79b06097","mapping_hash":"sha256:57ebad75d5845442a91479f53d1bdadc50d88095342edd29da8b6067bfbabd32","project":"mathlib4","revision":"db584cd6d46c92f209a44c0f1c829460d327499d"},"targets":{"arxo.order":{"content_hash":"sha256:dd131bb594e38f5aec813104a2c59b00b90d33725c587ce0745980df7fe44db6","namespace":"urn:arxo:arxo.order","version":"0.1.0"}}},"validator_hash":"sha256:2b677de7c1b487853bcde8fb1c85707f9cdd5a0a2f346f471be2373df0ebd873"}}}

Ссылаются нормы: Import_Rule_6b176bb86abf8dc884d0466d8c02331e87623c5bbdc748c4674ab4bbddd8fca1