Value Members

1.  final def !=(arg0: Any): Boolean

   Definition Classes

   AnyRef → Any

2.  final def ##(): Int

   Definition Classes

   AnyRef → Any

3.  final def ==(arg0: Any): Boolean

   Definition Classes

   AnyRef → Any

4.  def allL(e: Term): DependentPositionWithAppliedInputTactic

   Definition Classes

   SequentCalculus

5.  def allL(e: Option[Term]): DependentPositionWithAppliedInputTactic

   all left: instantiate a universal quantifier in the antecedent by the concrete instance e (itself if None).

   all left: instantiate a universal quantifier in the antecedent by the concrete instance e (itself if None).

   Definition Classes

   SequentCalculus

   Annotations

   @Tactic( x$481 , x$485 , x$486 , x$483 , x$484 , x$487 , x$488 , x$489 , x$490 , x$491 , x$482 , x$492 )

6.  def allL(x: Variable, inst: Term): BuiltInPositionTactic

   all left: instantiate a universal quantifier for variable x in the antecedent by the concrete instance inst.

   all left: instantiate a universal quantifier for variable x in the antecedent by the concrete instance inst.

   p(inst), G |- D
   ------------------------ ∀L
   \forall x p(x), G |- D

   Definition Classes

   SequentCalculus

7.  val allL: DependentPositionTactic

   all left: instantiate a universal quantifier in the antecedent by itself.

   all left: instantiate a universal quantifier in the antecedent by itself.

   Definition Classes

   SequentCalculus

8.  def allLPos(instPos: Position): DependentPositionTactic

   all left: instantiate a universal quantifier in the antecedent by the term obtained from position instPos.

   all left: instantiate a universal quantifier in the antecedent by the term obtained from position instPos.

   Definition Classes

   SequentCalculus

9.  def allLkeep(e: Term): DependentPositionWithAppliedInputTactic

   all left keep: keeping around the quantifier, instantiate a universal quantifier in the antecedent by the concrete instance e.

   all left keep: keeping around the quantifier, instantiate a universal quantifier in the antecedent by the concrete instance e.

   \forll x p(x), G, p(e) |- D
   --------------------------- ∀L
   \forall x p(x), G |- D

   Definition Classes

   SequentCalculus

   Annotations

   @Tactic( x$505 , x$509 , x$510 , x$507 , x$508 , x$511 , x$512 , x$513 , x$514 , x$515 , x$506 , x$516 )

10.  def allLmon(q: Formula): DependentPositionWithAppliedInputTactic

    Universal monotonicity in antecedent: replace p(x) with a characteristic property q(x).

    Universal monotonicity in antecedent: replace p(x) with a characteristic property q(x).

    Use:                      Show:
    G, \forall x q(x) |- D    G, p(x) |- D, q(x)
    -------------------------------------------- M∀L
    G, \forall x p(x) |- D

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$493 , x$497 , x$498 , x$495 , x$496 , x$499 , x$500 , x$501 , x$502 , x$503 , x$494 , x$504 )

11.  val allR: BuiltInPositionTactic

    all right: Skolemize a universal quantifier in the succedent (Skolemize) Skolemization with bound renaming on demand.

    all right: Skolemize a universal quantifier in the succedent (Skolemize) Skolemization with bound renaming on demand.

    G |- p(x), D
    ----------------------- (Skolemize) provided x not in G,D
    G |- \forall x p(x), D

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$217 , x$220 , x$221 , x$218 , x$219 , x$222 , x$223 , x$224 , x$225 , x$226 , x$227 , x$228 )

    Examples:

    1. y>5   |- x^2>=0
       --------------------------allSkolemize(1)
       y>5   |- \forall x x^2>=0

    ,

    2. Uniformly renames other occurrences of the quantified variable in the context on demand to avoid SkolemClashException.

       x_0>0 |- x^2>=0
       --------------------------allSkolemize(1)
       x>0   |- \forall x x^2>=0

    See also

    edu.cmu.cs.ls.keymaerax.core.Skolemize

12.  def allRi(t: Term, x: Option[Variable]): DependentPositionWithAppliedInputTactic

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$469 , x$474 , x$475 , x$471 , x$472 , x$476 , x$477 , x$473 , x$478 , x$479 , x$470 , x$480 )

13.  def alphaRen(what: Variable, to: Variable): DependentPositionWithAppliedInputTactic

    Alpha bound renaming of what to to at a specific position (for quantifier/assignment/ode).

    Alpha bound renaming of what to to at a specific position (for quantifier/assignment/ode). Variable to must not occur free at the applied position.

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$565 , x$570 , x$566 , x$567 , x$568 , x$571 , x$572 , x$573 , x$574 , x$575 , x$569 , x$576 )

    Example:

    1. x=y |- [{y'=y}]y>=0      x=y |- [{x'=x}]x>=0, x=y
       ------------------------------------------------- alphaRen("x","y",1)
       x=y |- [{x'=x}]x>=0

14.  def alphaRenAll(what: Variable, to: Variable): InputTactic

    Alpha renaming of what to to everywhere in the sequent.

    Alpha renaming of what to to everywhere in the sequent. Formulas that have variable to occur free are excluded from the renaming.

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$577 , x$582 , x$578 , x$579 , x$580 , x$583 , x$584 , x$585 , x$586 , x$587 , x$581 , x$588 )

    Example:

    1. [y:=0;]y>=0 |- [{y'=y}]y>=0, [x:=y;]x=y      [x:=0;]x>=0 |- [{x'=x}]x>=0, x:=y;]x=y, x=y
       ---------------------------------------------------------------------------------------- alphaRenAll("x","y",1)
       [x:=0;]x>=0 |- [{x'=x}]x>=0, [x:=y;]x=y

15.  val alphaRenAllBy: DependentPositionTactic

    Alpha renaming everywhere in the sequent using an equality at a specific position in the antecedent.

    Alpha renaming everywhere in the sequent using an equality at a specific position in the antecedent.

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$589 , x$593 , x$590 , x$592 , x$591 , x$594 , x$595 , x$596 , x$597 , x$598 , x$599 , x$600 )

16.  val andL: CoreLeftTactic

    &L And left: split a conjunction in the antecedent into separate assumptions (AndLeft)

    &L And left: split a conjunction in the antecedent into separate assumptions (AndLeft)

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$241 , x$244 , x$245 , x$242 , x$243 , x$246 , x$247 , x$248 , x$249 , x$250 , x$251 , x$252 )

17.  def andLi(keepLeft: Boolean): BuiltInTwoPositionTactic

    Inverse of andL.

    Inverse of andL.

      G, G', G'', a&b  |- D
    -------------------------
      G, a, G', b, G'' |- D

    Definition Classes

    SequentCalculus

18.  val andLi: AppliedBuiltinTwoPositionTactic

    Definition Classes

    SequentCalculus

19.  val andR: DependentPositionTactic

    &R And right: prove a conjunction in the succedent on two separate branches (AndRight)

    &R And right: prove a conjunction in the succedent on two separate branches (AndRight)

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$169 , x$172 , x$173 , x$170 , x$171 , x$174 , x$175 , x$176 , x$177 , x$178 , x$179 , x$180 )

20.  val andRRule: CoreRightTactic

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$361 , x$364 , x$365 , x$362 , x$363 , x$366 , x$367 , x$368 , x$369 , x$370 , x$371 , x$372 )

21.  val applyEqualities: BuiltInTactic

    Rewrites all atom equalities in the assumptions.

    Rewrites all atom equalities in the assumptions.

    Definition Classes

    SequentCalculus

22.  final def asInstanceOf[T0]: T0

    Definition Classes

    Any

23.  def clone(): AnyRef

    Attributes

    protected[java.lang]

    Definition Classes

    AnyRef

    Annotations

    @native() @throws( ... )

24.  def close(a: Int, s: Int): BelleExpr

    Definition Classes

    SequentCalculus

25.  val close: BuiltInTactic

    close: closes the branch when the same formula is in the antecedent and succedent or true right or false left.

    close: closes the branch when the same formula is in the antecedent and succedent or true right or false left.

           *
    ------------------ (Id)
      p, G |- p, D

          *
    ------------------ (close true)
      G |- true, D

           *
    ------------------ (close false)
      false, G |- D

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$157 , x$161 , x$158 , x$159 , x$160 , x$162 , x$163 , x$164 , x$165 , x$166 , x$167 , x$168 )

26.  val closeF: BuiltInTactic

    closeF: closes the branch when false is in the antecedent (CloseFalse).

    closeF: closes the branch when false is in the antecedent (CloseFalse).

           *
    ------------------ (close false)
      false, G |- D

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$325 , x$329 , x$326 , x$327 , x$328 , x$330 , x$331 , x$332 , x$333 , x$334 , x$335 , x$336 )

27.  val closeId: BuiltInTwoPositionTactic

    close: closes the branch when the same formula is in the antecedent and succedent at the indicated positions (Close).

    close: closes the branch when the same formula is in the antecedent and succedent at the indicated positions (Close).

           *
    ------------------ (Id)
      p, G |- p, D

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$123 , x$121 , x$122 , x$124 , x$125 , x$126 , x$127 , x$128 , x$129 , x$130 , x$131 , x$132 )

28.  val closeIdWith: BuiltInPositionTactic

    closeIdWith: closes the branch with the formula at the given position when the same formula is in the antecedent and succedent (Close)

    closeIdWith: closes the branch with the formula at the given position when the same formula is in the antecedent and succedent (Close)

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$305 , x$304 , x$301 , x$302 , x$303 , x$306 , x$307 , x$308 , x$309 , x$310 , x$311 , x$312 )

29.  val closeT: BuiltInTactic

    closeT: closes the branch when true is in the succedent (CloseTrue).

    closeT: closes the branch when true is in the succedent (CloseTrue).

          *
    ------------------ (close true)
      G |- true, D

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$73 , x$77 , x$74 , x$75 , x$76 , x$78 , x$79 , x$80 , x$81 , x$82 , x$83 , x$84 )

30.  val cohide: BuiltInPositionTactic

    CoHide/coweaken whether left or right: drop all other formulas from the sequent (CoHideLeft)

    CoHide/coweaken whether left or right: drop all other formulas from the sequent (CoHideLeft)

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$229 , x$233 , x$230 , x$231 , x$232 , x$234 , x$235 , x$236 , x$237 , x$238 , x$239 , x$240 )

31.  val cohide2: BuiltInTwoPositionTactic

    CoHide2/coweaken2 both left and right: drop all other formulas from the sequent (CoHide2)

    CoHide2/coweaken2 both left and right: drop all other formulas from the sequent (CoHide2)

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( "WLR" , "coHide2" , "Co-Weaken Both" , "P |- Q" , "Γ, P |- Q, Δ" , macros.this.Tactic.<init>$default$6 , macros.this.Tactic.<init>$default$7 , macros.this.Tactic.<init>$default$8 , macros.this.Tactic.<init>$default$9 , ... , ... , ... )

32.  val cohideL: CoreLeftTactic

    CoHide/weaken left: drop all other formulas from the sequent (CoHideLeft)

    CoHide/weaken left: drop all other formulas from the sequent (CoHideLeft)

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$349 , x$353 , x$350 , x$351 , x$352 , x$354 , x$355 , x$356 , x$357 , x$358 , x$359 , x$360 )

33.  val cohideOnlyL: BuiltInLeftTactic

    Cohides in antecedent, but leaves succedent as is.

    Cohides in antecedent, but leaves succedent as is.

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$277 , x$281 , x$278 , x$279 , x$280 , x$282 , x$283 , x$284 , x$285 , x$286 , x$287 , x$288 )

34.  val cohideOnlyR: BuiltInRightTactic

    Cohides in succedent, but leaves antecedent as is.

    Cohides in succedent, but leaves antecedent as is.

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$313 , x$317 , x$314 , x$315 , x$316 , x$318 , x$319 , x$320 , x$321 , x$322 , x$323 , x$324 )

35.  val cohideR: CoreRightTactic

    CoHide/weaken right: drop all other formulas from the sequent (CoHideRight)

    CoHide/weaken right: drop all other formulas from the sequent (CoHideRight)

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$85 , x$89 , x$86 , x$87 , x$88 , x$90 , x$91 , x$92 , x$93 , x$94 , x$95 , x$96 )

36.  lazy val commuteEqual: BuiltInPositionTactic

    Commute equality a=b to b=a

    Commute equality a=b to b=a

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$193 , x$196 , x$194 , x$197 , x$195 , x$198 , x$199 , x$200 , x$201 , x$202 , x$203 , x$204 )

37.  val commuteEquivL: CoreLeftTactic

    Commute equivalence on the left CommuteEquivLeft.

    Commute equivalence on the left CommuteEquivLeft.

    q<->p, G |-  D
    -------------- (<->cL)
    p<->q, G |-  D

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$601 , x$605 , x$602 , x$603 , x$604 , x$606 , x$607 , x$608 , x$609 , x$610 , x$611 , x$612 )

38.  val commuteEquivR: CoreRightTactic

    Commute equivalence on the right CommuteEquivRight.

    Commute equivalence on the right CommuteEquivRight.

    G |- q<->p, D
    ------------- (<->cR)
    G |- p<->q, D

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$205 , x$209 , x$206 , x$207 , x$208 , x$210 , x$211 , x$212 , x$213 , x$214 , x$215 , x$216 )

39.  def cut(f: Formula): InputTactic

    cut a formula in to prove it on one branch and then assume it on the other.

    cut a formula in to prove it on one branch and then assume it on the other. Or to perform a case distinction on whether it holds (Cut).

    Use:          Show:
    G, c |- D     G |- D, c
    ----------------------- (cut)
            G |- D

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$436 , x$437 , x$438 , x$433 , x$434 , x$439 , x$440 , x$441 , x$442 , x$443 , x$435 , x$444 )

40.  def cutL(f: Formula): DependentPositionWithAppliedInputTactic

    cut a formula in in place of pos on the left to prove its implication on the second branch and assume it on the first.

    cut a formula in in place of pos on the left to prove its implication on the second branch and assume it on the first. (CutLeft).

    c, G |- D    G |- D, p->c
    ------------------------- (Cut Left)
           p, G |- D

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$460 , x$461 , x$462 , x$457 , x$458 , x$463 , x$464 , x$465 , x$466 , x$467 , x$459 , x$468 )

41.  def cutLR(f: Formula): DependentPositionWithAppliedInputTactic

    cut a formula in in place of pos to prove its implication on the second branch and assume it on the first (whether pos is left or right).

    cut a formula in in place of pos to prove its implication on the second branch and assume it on the first (whether pos is left or right). (CutLeft or CutRight).

    c, G |- D    G |- D, p->c
    ------------------------- (Cut Left at antecedent<0)
           p, G |- D

    G |- c, D    G |- c->p, D
    ------------------------- (Cut right at succedent>0)
           G |- p, D

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( macros.this.Tactic.<init>$default$1 , macros.this.Tactic.<init>$default$2 , macros.this.Tactic.<init>$default$3 , macros.this.Tactic.<init>$default$4 , macros.this.Tactic.<init>$default$5 , macros.this.Tactic.<init>$default$6 , macros.this.Tactic.<init>$default$7 , macros.this.Tactic.<init>$default$8 , macros.this.Tactic.<init>$default$9 , ... , ... , ... )

42.  def cutR(f: Formula): DependentPositionWithAppliedInputTactic

    cut a formula in in place of pos on the right to prove its implication on the second branch and assume it on the first.

    cut a formula in in place of pos on the right to prove its implication on the second branch and assume it on the first. (CutRight).

    G |- c, D    G |- c->p, D
    ------------------------- (Cut right)
           G |- p, D

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$448 , x$449 , x$450 , x$445 , x$446 , x$451 , x$452 , x$453 , x$454 , x$455 , x$447 , x$456 )

43.  final def eq(arg0: AnyRef): Boolean

    Definition Classes

    AnyRef

44.  def equals(arg0: Any): Boolean

    Definition Classes

    AnyRef → Any

45.  val equivL: DependentPositionTactic

    <->L Equiv left: use an equivalence by considering both true or both false cases (EquivLeft)

    <->L Equiv left: use an equivalence by considering both true or both false cases (EquivLeft)

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$397 , x$400 , x$401 , x$398 , x$399 , x$402 , x$403 , x$404 , x$405 , x$406 , x$407 , x$408 )

46.  val equivLRule: CoreLeftTactic

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$409 , x$412 , x$413 , x$410 , x$411 , x$414 , x$415 , x$416 , x$417 , x$418 , x$419 , x$420 )

47.  val equivR: DependentPositionTactic

    <->R Equiv right: prove an equivalence by proving both implications (EquivRight)

    <->R Equiv right: prove an equivalence by proving both implications (EquivRight)

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$61 , x$64 , x$65 , x$62 , x$63 , x$66 , x$67 , x$68 , x$69 , x$70 , x$71 , x$72 )

48.  val equivRRule: CoreRightTactic

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$421 , x$424 , x$425 , x$422 , x$423 , x$426 , x$427 , x$428 , x$429 , x$430 , x$431 , x$432 )

49.  val equivifyR: CoreRightTactic

    Turn implication a->b on the right into an equivalence a<->b, which is useful to prove by CE etc.

    Turn implication a->b on the right into an equivalence a<->b, which is useful to prove by CE etc. (EquivifyRight).

    G |- a<->b, D
    -------------
    G |- a->b,  D

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$181 , x$185 , x$182 , x$183 , x$184 , x$186 , x$187 , x$188 , x$189 , x$190 , x$191 , x$192 )

50.  val exchangeL: BuiltInTwoPositionTactic

    Exchange left rule reorders antecedent.

    Exchange left rule reorders antecedent.

    q, p, G |- D
    ------------- (Exchange left)
    p, q, G |- D

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$289 , x$293 , x$290 , x$291 , x$292 , x$294 , x$295 , x$296 , x$297 , x$298 , x$299 , x$300 )

51.  val exchangeR: BuiltInTwoPositionTactic

    Exchange right rule reorders succedent.

    Exchange right rule reorders succedent.

    G |- q, p, D
    ------------- (Exchange right)
    G |- p, q, D

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$337 , x$341 , x$338 , x$339 , x$340 , x$342 , x$343 , x$344 , x$345 , x$346 , x$347 , x$348 )

52.  val existsL: BuiltInPositionTactic

    exists left: Skolemize an existential quantifier in the antecedent by introducing a new name for the witness.

    exists left: Skolemize an existential quantifier in the antecedent by introducing a new name for the witness.

              p(x), G |- D
    ------------------------ (Skolemize) provided x not in G,D
    \exists x p(x), G |- D

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$265 , x$268 , x$269 , x$266 , x$267 , x$270 , x$271 , x$272 , x$273 , x$274 , x$275 , x$276 )

53.  def existsLi(t: Term, x: Option[Variable]): DependentPositionWithAppliedInputTactic

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$517 , x$522 , x$523 , x$519 , x$520 , x$524 , x$525 , x$521 , x$526 , x$527 , x$518 , x$528 )

54.  def existsR(e: Term): BuiltInPositionTactic

    Definition Classes

    SequentCalculus

55.  def existsR(e: Option[Term]): DependentPositionWithAppliedInputTactic

    exists right: instantiate an existential quantifier in the succedent by a concrete instance inst as a witness

    exists right: instantiate an existential quantifier in the succedent by a concrete instance inst as a witness

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$529 , x$533 , x$534 , x$531 , x$532 , x$535 , x$536 , x$537 , x$538 , x$539 , x$530 , x$540 )

56.  def existsR(x: Variable, inst: Term): BuiltInPositionTactic

    exists right: instantiate an existential quantifier for x in the succedent by a concrete instance inst as a witness.

    exists right: instantiate an existential quantifier for x in the succedent by a concrete instance inst as a witness.

    G |- p(inst), D
    ----------------------- ∃R
    G |- \exists x p(x), D

    Definition Classes

    SequentCalculus

57.  val existsR: DependentPositionTactic

    exists right: instantiate an existential quantifier for x in the succedent by itself as a witness

    exists right: instantiate an existential quantifier for x in the succedent by itself as a witness

    Definition Classes

    SequentCalculus

58.  def existsRPos(instPos: Position): DependentPositionTactic

    exists right: instantiate an existential quantifier in the succedent by a concrete term obtained from position instPos.

    exists right: instantiate an existential quantifier in the succedent by a concrete term obtained from position instPos.

    Definition Classes

    SequentCalculus

59.  def existsRmon(q: Formula): DependentPositionWithAppliedInputTactic

    Existential monotonicity in succedent: replace p(x) with a characteristic property q(x).

    Existential monotonicity in succedent: replace p(x) with a characteristic property q(x).

    Use:                      Show:
    G |- \exists x q(x), D    G, q(x) |- p(x), D
    -------------------------------------------- M∃R
    G |- \exists x p(x), D

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$541 , x$545 , x$546 , x$543 , x$544 , x$547 , x$548 , x$549 , x$550 , x$551 , x$542 , x$552 )

60.  val expandAll: BuiltInTactic

    Expands all special functions (abs/min/max).

    Expands all special functions (abs/min/max).

    Definition Classes

    SequentCalculus

61.  def finalize(): Unit

    Attributes

    protected[java.lang]

    Definition Classes

    AnyRef

    Annotations

    @throws( classOf[java.lang.Throwable] )

62.  final def getClass(): Class[_]

    Definition Classes

    AnyRef → Any

    Annotations

    @native()

63.  def hashCode(): Int

    Definition Classes

    AnyRef → Any

    Annotations

    @native()

64.  val hide: BuiltInPositionTactic

    Hide/weaken whether left or right

    Hide/weaken whether left or right

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$133 , x$137 , x$134 , x$135 , x$136 , x$138 , x$139 , x$140 , x$141 , x$142 , x$143 , x$144 )

65.  val hideL: CoreLeftTactic

    Hide/weaken left: weaken a formula to drop it from the antecedent (HideLeft)

    Hide/weaken left: weaken a formula to drop it from the antecedent (HideLeft)

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$25 , x$29 , x$26 , x$27 , x$28 , x$30 , x$31 , x$32 , x$33 , x$34 , x$35 , x$36 )

66.  val hideR: CoreRightTactic

    Hide/weaken right: weaken a formula to drop it from the succcedent (HideRight)

    Hide/weaken right: weaken a formula to drop it from the succcedent (HideRight)

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$49 , x$53 , x$50 , x$51 , x$52 , x$54 , x$55 , x$56 , x$57 , x$58 , x$59 , x$60 )

67.  val id: BuiltInTactic

    id: closes the branch when the same formula is in the antecedent and succedent (Close).

    id: closes the branch when the same formula is in the antecedent and succedent (Close).

           *
    ------------------ (id)
      p, G |- p, D

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$16 , x$15 , x$17 , x$13 , x$14 , x$18 , x$19 , x$20 , x$21 , x$22 , x$23 , x$24 )

68.  val idx: DependentTactic

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$555 , x$556 , x$557 , x$553 , x$554 , x$558 , x$559 , x$560 , x$561 , x$562 , x$563 , x$564 )

69.  val implyL: DependentPositionTactic

    ->L Imply left: use an implication in the antecedent by proving its left-hand side on one branch and using its right-hand side on the other branch (ImplyLeft)

    ->L Imply left: use an implication in the antecedent by proving its left-hand side on one branch and using its right-hand side on the other branch (ImplyLeft)

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$253 , x$256 , x$257 , x$254 , x$255 , x$258 , x$259 , x$260 , x$261 , x$262 , x$263 , x$264 )

70.  val implyLRule: CoreLeftTactic

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$385 , x$388 , x$389 , x$386 , x$387 , x$390 , x$391 , x$392 , x$393 , x$394 , x$395 , x$396 )

71.  val implyR: CoreRightTactic

    ->R Imply right: prove an implication in the succedent by assuming its left-hand side and proving its right-hand side (ImplyRight)

    ->R Imply right: prove an implication in the succedent by assuming its left-hand side and proving its right-hand side (ImplyRight)

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$1 , x$4 , x$5 , x$2 , x$3 , x$6 , x$7 , x$8 , x$9 , x$10 , x$11 , x$12 )

72.  def implyRi(keep: Boolean = false): BuiltInTwoPositionTactic

    Inverse of implyR.

    Inverse of implyR.

      G, G' |- D, D', a -> b
    -------------------------
      G, a, G' |- D, b, D'

    Definition Classes

    SequentCalculus

73.  val implyRi: AppliedBuiltinTwoPositionTactic

    Definition Classes

    SequentCalculus

74.  val implyRiX: BuiltInTwoPositionTactic

    eXternal wrapper for implyRi

    eXternal wrapper for implyRi

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( "implyRi" , "implyRi" , macros.this.Tactic.<init>$default$3 , macros.this.Tactic.<init>$default$4 , macros.this.Tactic.<init>$default$5 , macros.this.Tactic.<init>$default$6 , macros.this.Tactic.<init>$default$7 , macros.this.Tactic.<init>$default$8 , macros.this.Tactic.<init>$default$9 , ... , ... , ... )

75.  final def isInstanceOf[T0]: Boolean

    Definition Classes

    Any

76.  def label(s: String): InputTactic

    Call/label the current proof branch by the top-level label s.

    Call/label the current proof branch by the top-level label s.

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( macros.this.Tactic.<init>$default$1 , macros.this.Tactic.<init>$default$2 , macros.this.Tactic.<init>$default$3 , macros.this.Tactic.<init>$default$4 , macros.this.Tactic.<init>$default$5 , macros.this.Tactic.<init>$default$6 , macros.this.Tactic.<init>$default$7 , macros.this.Tactic.<init>$default$8 , macros.this.Tactic.<init>$default$9 , ... , ... , ... )

    See also

    Idioms.<()

    sublabel()

    BelleLabels

77.  def label(s: BelleLabel): BelleExpr

    Call/label the current proof branch by the given label s.

    Call/label the current proof branch by the given label s.

    Definition Classes

    SequentCalculus

    See also

    Idioms.<()

    sublabel()

    BelleLabels

78.  def modusPonens(assumption: AntePos, implication: AntePos): BelleExpr

    Modus Ponens: p&(p->q) -> q.

    Modus Ponens: p&(p->q) -> q.

    assumption

    Position pointing to p

    implication

    Position pointing to p->q

    Definition Classes

    SequentCalculus

    Example:

    1.    p, q, G |- D
       ---------------- modusPonens
       p, p->q, G |- D

79.  final def ne(arg0: AnyRef): Boolean

    Definition Classes

    AnyRef

80.  val notL: CoreLeftTactic

    !L Not left: move an negation in the antecedent to the succedent (NotLeft)

    !L Not left: move an negation in the antecedent to the succedent (NotLeft)

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$109 , x$112 , x$113 , x$110 , x$111 , x$114 , x$115 , x$116 , x$117 , x$118 , x$119 , x$120 )

81.  val notR: CoreRightTactic

    !R Not right: move an negation in the succedent to the antecedent (NotRight)

    !R Not right: move an negation in the succedent to the antecedent (NotRight)

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$97 , x$100 , x$101 , x$98 , x$99 , x$102 , x$103 , x$104 , x$105 , x$106 , x$107 , x$108 )

82.  final def notify(): Unit

    Definition Classes

    AnyRef

    Annotations

    @native()

83.  final def notifyAll(): Unit

    Definition Classes

    AnyRef

    Annotations

    @native()

84.  val orL: DependentPositionTactic

    |L Or left: use a disjunction in the antecedent by assuming each option on separate branches (OrLeft)

    |L Or left: use a disjunction in the antecedent by assuming each option on separate branches (OrLeft)

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$37 , x$40 , x$41 , x$38 , x$39 , x$42 , x$43 , x$44 , x$45 , x$46 , x$47 , x$48 )

85.  val orLRule: CoreLeftTactic

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$373 , x$376 , x$377 , x$374 , x$375 , x$378 , x$379 , x$380 , x$381 , x$382 , x$383 , x$384 )

86.  val orR: CoreRightTactic

    |R Or right: split a disjunction in the succedent into separate formulas to show alternatively (OrRight)

    |R Or right: split a disjunction in the succedent into separate formulas to show alternatively (OrRight)

    Definition Classes

    SequentCalculus

    Annotations

    @Tactic( x$145 , x$148 , x$149 , x$146 , x$147 , x$150 , x$151 , x$152 , x$153 , x$154 , x$155 , x$156 )

87.  def orRi(keepLeft: Boolean): BuiltInTwoPositionTactic

    Inverse of orR.

    Inverse of orR.

      G |- D, D', D'', a | b
    -------------------------
      G |- D, a, D', b, D''

    Definition Classes

    SequentCalculus

88.  val orRi: AppliedBuiltinTwoPositionTactic

    Definition Classes

    SequentCalculus

89.  def sublabel(s: String): BelleExpr

    Mark the current proof branch and all subbranches s.

    Mark the current proof branch and all subbranches s.

    Definition Classes

    SequentCalculus

    See also

    label()

90.  final def synchronized[T0](arg0: ⇒ T0): T0

    Definition Classes

    AnyRef

91.  def toString(): String

    Definition Classes

    AnyRef → Any

92.  final def wait(): Unit

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

93.  final def wait(arg0: Long, arg1: Int): Unit

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

94.  final def wait(arg0: Long): Unit

    Definition Classes

    AnyRef

    Annotations

    @native() @throws( ... )