Lean4
/-- Return true iff `e₁` is a "subset" of `e₂`.
Example: The result is `true` for `e₁ := a*a*a*b*d` and `e₂ := a*a*a*a*b*b*c*d*d`.
The result is also `true` for `e₁ := a` and `e₂ := a*a*a*b*c`. -/
def isSubset : (e₁ e₂ : ACApps) → Bool
| .ofExpr a, .ofExpr b => a == b
| .ofExpr a, .apps _ args => args.contains a
| .apps _ _, .ofExpr _ => false
| .apps op₁ args₁, .apps op₂ args₂ =>
if op₁ == op₂ then
if args₁.size ≤ args₂.size then
Id.run
(do
let mut i₁ := 0
let mut i₂ := 0
while h : i₁ < args₁.size ∧ i₂ < args₂.size do
if args₁[i₁] == args₂[i₂] then
i₁ := i₁ + 1
i₂ := i₂ + 1
else if Expr.lt args₂[i₂] args₁[i₁] then
i₂ := i₂ + 1
else
return false
return i₁ == args₁.size)
else false
else false
