Packages

c

edu.cmu.cs.ls.keymaerax.infrastruct

USubstAboveURen

final class USubstAboveURen extends RenUSubstBase

Renaming Uniform Substitution that, in Sequent direction, first runs a uniform renaming and on the result subsequently the uniform substituion.

s(RG) |- s(RD)
-------------- USubst
  RG  |- RD
-------------- URen
   G  |- D
Note

reading in Hilbert direction from top to bottom, the uniform substitution comes first to ensure the subsequent uniform renaming no longer has nonrenamable program constants since no semantic renaming.

Linear Supertypes
RenUSubstBase, RenUSubst, (Expression) ⇒ Expression, AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. USubstAboveURen
  2. RenUSubstBase
  3. RenUSubst
  4. Function1
  5. AnyRef
  6. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new USubstAboveURen(subsDefsInput: Seq[(Expression, Expression)])

Type Members

  1. type RenUSubstRepl = (Expression, Expression)

    A renaming substitution pair for a renaming uniform substitution.

    A renaming substitution pair for a renaming uniform substitution.

    Definition Classes
    RenUSubst
    See also

    edu.cmu.cs.ls.keymaerax.core.SubstitutionPair

    edu.cmu.cs.ls.keymaerax.infrastruct.Augmentors.TermAugmentor.~>()

    edu.cmu.cs.ls.keymaerax.infrastruct.Augmentors.FormulaAugmentor.~>()

    edu.cmu.cs.ls.keymaerax.infrastruct.Augmentors.ProgramAugmentor.~>()

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. def ++(other: RenUSubst): RenUSubst

    Union of renaming uniform substitutions, i.e., both replacement lists merged.

    Union of renaming uniform substitutions, i.e., both replacement lists merged.

    Definition Classes
    RenUSubst
  4. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  5. def andThen[A](g: (Expression) ⇒ A): (Expression) ⇒ A
    Definition Classes
    Function1
    Annotations
    @unspecialized()
  6. def apply(p: DifferentialProgram): DifferentialProgram
    Definition Classes
    USubstAboveURen → RenUSubst
  7. def apply(p: Program): Program
    Definition Classes
    USubstAboveURen → RenUSubst
  8. def apply(f: Formula): Formula
    Definition Classes
    USubstAboveURen → RenUSubst
  9. def apply(t: Term): Term
    Definition Classes
    USubstAboveURen → RenUSubst
  10. def apply(s: Sequent): Sequent

    Apply everywhere in the sequent.

    Apply everywhere in the sequent.

    Definition Classes
    RenUSubst
  11. def apply(e: Expression): Expression
    Definition Classes
    RenUSubst → Function1
  12. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  13. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  14. def compose[A](g: (A) ⇒ Expression): (A) ⇒ Expression
    Definition Classes
    Function1
    Annotations
    @unspecialized()
  15. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  16. def equals(e: Any): Boolean
    Definition Classes
    USubstAboveURen → AnyRef → Any
  17. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  18. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  19. def getRenamingTactic: BelleExpr

    Get the renaming tactic part

    Get the renaming tactic part

    Definition Classes
    RenUSubstBase → RenUSubst
  20. def hashCode(): Int
    Definition Classes
    USubstAboveURen → AnyRef → Any
  21. def isEmpty: Boolean

    Returns true if there is no replacement.

    Returns true if there is no replacement.

    Definition Classes
    RenUSubst
  22. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  23. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  24. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  25. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  26. def reapply(subs: Seq[(Expression, Expression)]): USubstAboveURen

    Create a similar RenUSubst of the same class with the alternative list of replacements

    Create a similar RenUSubst of the same class with the alternative list of replacements

    Definition Classes
    USubstAboveURen → RenUSubstBase → RenUSubst
  27. def renaming: RenUSubst

    The uniform renaming part of this renaming uniform substitution

    The uniform renaming part of this renaming uniform substitution

    Definition Classes
    RenUSubstBase → RenUSubst
  28. final val rens: Seq[(Variable, Variable)]

    Renaming part, with identity renaming no-ops filtered out.

    Renaming part, with identity renaming no-ops filtered out.

    Attributes
    protected
    Definition Classes
    RenUSubstBase
  29. final val subsDefs: Seq[SubstitutionPair]

    Substitution part, with identity substitution no-ops filtered out.

    Substitution part, with identity substitution no-ops filtered out.

    Attributes
    protected
    Definition Classes
    RenUSubstBase
  30. def substitution: RenUSubst

    The uniform substitution part of this renaming uniform substitution

    The uniform substitution part of this renaming uniform substitution

    Definition Classes
    RenUSubstBase → RenUSubst
    See also

    usubst

  31. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  32. val toCore: (Expression) ⇒ Nothing

    This RenUSubst implemented strictly from the core.

    This RenUSubst implemented strictly from the core.

    Definition Classes
    USubstAboveURen → RenUSubst
    Note

    For contract purposes

  33. def toForward: (ProvableSig) ⇒ ProvableSig

    Central operation to convert to forward tactic using the core's respective uniform renaming and uniform substitution rules.

    Central operation to convert to forward tactic using the core's respective uniform renaming and uniform substitution rules.

    Definition Classes
    USubstAboveURen → RenUSubst
  34. def toString(): String
    Definition Classes
    USubstAboveURen → RenUSubstBase → Function1 → AnyRef → Any
  35. def toTactic(form: Sequent): BelleExpr

    Convert to tactic to reduce to form by successively using the respective uniform renaming and uniform substitution rules

    Convert to tactic to reduce to form by successively using the respective uniform renaming and uniform substitution rules

    Definition Classes
    USubstAboveURen → RenUSubstBase
  36. final lazy val usubst: USubst

    The uniform substitution part of this renaming uniform substitution

    The uniform substitution part of this renaming uniform substitution

    Definition Classes
    RenUSubstBase → RenUSubst
    Note

    lazy val and postponing applicable() until actual use case would make it possible for useAt(inst) to modify before exception. Not sure that's worth it though.

    See also

    substitution

  37. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  38. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  39. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from RenUSubstBase

Inherited from RenUSubst

Inherited from (Expression) ⇒ Expression

Inherited from AnyRef

Inherited from Any

Ungrouped