Proof step 1 from proof equiv-both-leq (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(C_≡T_A(cioaut, aioaut) ↔ C_≤T_A(cioaut, aioaut) ∧ C_≤T_A(aioaut, cioaut)) ⊦

Rule argument

Additional information

Proof step 2 from proof equiv-both-leq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ⊦ (∀ β. trace(cioaut)(β) ↔ trace(aioaut)(β)) ↔ (∀ β. trace(cioaut)(β) → trace(aioaut)(β)) ∧ (∀ β. trace(aioaut)(β) → trace(cioaut)(β))

Rule argument

Additional information

Used simplifier rules: equiv-def: ⊦ C_≡T_A(cioaut, aioaut) ↔ (∀ β. trace(cioaut)(β) ↔ trace(aioaut)(β)); leq-def: ⊦ C_≤T_A(cioaut, aioaut) ↔ (∀ β. trace(cioaut)(β) → trace(aioaut)(β));

Proof step 3 from proof equiv-both-leq (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 4:

  ∀ β. trace(cioaut)(β) ↔ trace(aioaut)(β) ⊦ (∀ β. trace(cioaut)(β) → trace(aioaut)(β)) ∧ (∀ β. trace(aioaut)(β) → trace(cioaut)(β))

• Proof step 8:

  ∀ β. trace(cioaut)(β) → trace(aioaut)(β), ∀ β. trace(aioaut)(β) → trace(cioaut)(β) ⊦ ∀ β. trace(cioaut)(β) ↔ trace(aioaut)(β)

Rule argument

Additional information

Proof step 4 from proof equiv-both-leq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ∀ β. trace(cioaut)(β) ↔ trace(aioaut)(β) ⊦ (trace(cioaut)(β) → trace(aioaut)(β)) ∧ (trace(aioaut)(β0) → trace(cioaut)(β0))

Rule argument

Additional information

Proof step 5 from proof equiv-both-leq (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 6:

  trace(cioaut)(β), ¬ trace(aioaut)(β), ∀ β. trace(cioaut)(β) ↔ trace(aioaut)(β) ⊦

• Proof step 7:

  trace(aioaut)(β0), ¬ trace(cioaut)(β0), ∀ β. trace(cioaut)(β) ↔ trace(aioaut)(β) ⊦

Rule argument

Additional information

Proof step 6 from proof equiv-both-leq (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: β

Proof step 7 from proof equiv-both-leq (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: β0

Proof step 8 from proof equiv-both-leq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  ¬(trace(cioaut)(β) ↔ trace(aioaut)(β)), ∀ β. trace(aioaut)(β) → trace(cioaut)(β), ∀ β. trace(cioaut)(β) → trace(aioaut)(β) ⊦

Rule argument

Additional information

Proof step 9 from proof equiv-both-leq (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 10:

  trace(cioaut)(β), ¬ trace(aioaut)(β), ∀ β. trace(cioaut)(β) → trace(aioaut)(β), ∀ β. trace(aioaut)(β) → trace(cioaut)(β) ⊦

• Proof step 11:

  trace(aioaut)(β), ¬ trace(cioaut)(β), ∀ β. trace(cioaut)(β) → trace(aioaut)(β), ∀ β. trace(aioaut)(β) → trace(cioaut)(β) ⊦

Rule argument

Additional information

Proof step 10 from proof equiv-both-leq (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: β

Proof step 11 from proof equiv-both-leq (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: β