Releases: leanprover-community/con-nf
Releases · leanprover-community/con-nf
Create blueprint for rewrite
Full Changelog: v0.4...v0.5
First draft of complete proof
Complete the proof Signed-off-by: zeramorphic <[email protected]>
Finish main induction
Signed-off-by: zeramorphic <[email protected]>
Prove #(Tangle β) = #μ
Prove mk_tangle Signed-off-by: zeramorphic <[email protected]>
Prove freedom of action theorem
Proven freedom of action theorem Signed-off-by: zeramorphic <[email protected]>