Extended phi-calculus

[Anatolay]

PR-Codex overview

The focus of this PR is to refactor the term-rewriting system metatheory in the ARS.lean file.

Detailed summary

• Added definitions for properties like Reflexive and Transitive
• Defined ReflTransGen for reflexive transitive closure
• Implemented DiamondProperty, Confluence, Takahashi
• Added functions for implications between properties

The following files were skipped due to too many changes: Extended/ARS.lean, Extended/Record.lean, Extended/Reduction/Regular/Definition.lean, Extended/Reduction/Parallel/Definition.lean, Extended/Confluence/CompleteDevelopment.lean, Extended/Confluence/Equivalence.lean

✨ Ask PR-Codex anything about this PR by commenting with /codex {your question}

[0crat]

@Anatolay It is not a good idea to name Git branches like "extended". As per our policy, this violates the naming convention and incurs a -12 point penalty. For future reference, name your branch after the ticket number you're working on, e.g., "46". This helps maintain consistency and clarity in our workflow. Your current balance stands at +33.

[0crat]

@Anatolay Hey there! 👋 Thanks for your contribution, but it looks like we've got some room for improvement. Your 1510 hits-of-code are impressive, but remember, quality over quantity! 😉 We had to deduct points for the high hit count and lack of code review. Only 1 comment? Let's aim for at least 6 next time to avoid deductions. Despite the setbacks, you've earned 4 points (we always ensure a minimum reward). Keep the contributions coming, but focus on smaller, reviewable chunks. Your current balance stands at -14. Let's work on boosting that score!