gapt.examples.sequence.SumOfOnesF2ExampleProof
Attributes
-
Graph
-
-
Supertypes
-
class TacticsProof
class TacticsProof0
class Object
trait Matchable
class Any
Show all
-
Self type
-
Members list
Applies the quantified equation ∀x(e_l=e_r) to the left side of the equation tgt_l=tgt_r, leaving open the subgoal e_r σ = tgt_r.
Applies the quantified equation ∀x(e_l=e_r) to the left side of the equation tgt_l=tgt_r, leaving open the subgoal e_r σ = tgt_r.
Attributes
-
Inherited from:
-
ExplicitEqualityTactics
Applies the quantified equation ∀x(e_l=e_r) to the right side of the equation tgt_l=tgt_r, leaving open the subgoal tgt_l = e_l σ.
Applies the quantified equation ∀x(e_l=e_r) to the right side of the equation tgt_l=tgt_r, leaving open the subgoal tgt_l = e_l σ.
Attributes
-
Inherited from:
-
ExplicitEqualityTactics
Attributes
-
Inherited from:
-
TacticsProof
Attributes
-
Inherited from:
-
TacticsProof0