Packages

object Ax extends Logging

Central Database of Derived Axioms and Derived Axiomatic Rules, including information about core axioms and axiomatic rules from This registry of also provides meta information for matching keys and recursors for unificiation and chasing using the @Axiom]] annotation.

Using Axioms and Axiomatic Rules

Using a (derived) axiom merely requires indicating the position where to use it:

UnifyUSCalculus.useAt(Ax.choiceb)(1)

Closing a proof or using an axiomatic rule after unification works as follows:

UnifyUSCalculus.byUS(Ax.choiceb)

Closing a proof or using an axiomatic rule verbatim without unification works as follows:

UnifyUSCalculus.by(Ax.choiceb)

Equivalently one can also write TactixLibrary.useAt or TactixLibrary.byUS because TactixLibrary extends UnifyUSCalculus.

Adding Derived Axioms and Derived Axiomatic Rules

Core Axioms are loaded from the core and their meta information is annotated in this file e.g. as follows:

@Axiom(("[∪]", "[++]"), conclusion = "__[a∪b]P__↔[a]P∧[b]P",
       key = "0", recursor = "0;1", unifier = "surjlinear")
val choiceb = coreAxiom("[++] choice")

Derived Axioms are proved with a tactic and their meta information is annotated in this file e.g. as follows:

@Axiom("V", conclusion = "p→__[a]p__",
       key = "1", recursor = "*")
lazy val V = derivedAxiom("V vacuous",
  "p() -> [a{|^@|};]p()".asFormula,
  useAt(Ax.VK, PosInExpr(1::Nil))(1) &
  useAt(Ax.boxTrue)(1)
)

Derived Axiomatic Rules are derived with a tactic and their meta information is annotated in this file as follows:

@ProofRule("M[]", conclusion = "[a;]P |- [a;]Q", premises = "P |- Q")
lazy val monb = derivedRuleSequent("M[]",
  Sequent(immutable.IndexedSeq("[a_;]p_(||)".asFormula), immutable.IndexedSeq("[a_;]q_(||)".asFormula)),
  someTactic)
Note

To simplify bootstrap and avoid dependency management, the proofs of the derived axioms are written with explicit reference to other scala-objects representing provables (which will be proved on demand) as opposed to by referring to the names, which needs a map canonicalName->tacticOnDemand.

,

Lemmas are lazy vals, since their proofs may need a fully setup prover with QE

,

Derived axioms use the Provable facts of other derived axioms in order to avoid initialization cycles with AxiomInfo's contract checking.

See also

edu.cmu.cs.ls.keymaerax.core.AxiomBase

edu.cmu.cs.ls.keymaerax.btactics.macros.AxiomInfo

edu.cmu.cs.ls.keymaerax.btactics.macros.Axiom

UnifyUSCalculus.matcherFor()

Linear Supertypes
Logging, LazyLogging, LoggerHolder, AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. Ax
  2. Logging
  3. LazyLogging
  4. LoggerHolder
  5. AnyRef
  6. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Type Members

  1. type LemmaID = String

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. lazy val CEimplyCongruence: DerivedRuleInfo

    Rule "CEimply congruence".

    Rule "CEimply congruence". Premise p_(||) <-> q_(||) Conclusion ctx_{p_(||)} -> ctx_{q_(||)} End.

    Annotations
    @ProofRule( x$874 , x$877 , x$878 , x$876 , x$875 , x$879 , x$880 , x$881 , x$882 )
  5. lazy val CErevimplyCongruence: DerivedRuleInfo

    Rule "CErevimply congruence".

    Rule "CErevimply congruence". Premise q_(||) <-> p_(||) Conclusion ctx_{p_(||)} -> ctx_{q_(||)} End.

    Annotations
    @ProofRule( x$883 , x$886 , x$887 , x$885 , x$884 , x$888 , x$889 , x$890 , x$891 )
  6. val CErule: AxiomaticRuleInfo
  7. lazy val CQimplyCongruence: DerivedRuleInfo

    Rule "CQimply equation congruence".

    Rule "CQimply equation congruence". Premise f_(||) = g_(||) Conclusion ctx_(f_(||)) -> ctx_(g_(||)) End.

    Annotations
    @ProofRule( x$856 , x$859 , x$860 , x$858 , x$857 , x$861 , x$862 , x$863 , x$864 )
  8. lazy val CQrevimplyCongruence: DerivedRuleInfo

    Rule "CQrevimply equation congruence".

    Rule "CQrevimply equation congruence". Premise g_(||) = f_(||) Conclusion ctx_(f_(||)) -> ctx_(g_(||)) End.

    Annotations
    @ProofRule( x$865 , x$868 , x$869 , x$867 , x$866 , x$870 , x$871 , x$872 , x$873 )
  9. val CQrule: AxiomaticRuleInfo
  10. lazy val CTtermCongruence: DerivedRuleInfo

    Rule "CT term congruence".

    Rule "CT term congruence". Premise f_(||) = g_(||) Conclusion ctxT_(f_(||)) = ctxT_(g_(||)) End.

    Annotations
    @ProofRule( x$829 , x$832 , x$833 , x$831 , x$830 , x$834 , x$835 , x$836 , x$837 )
  11. val Cont: CoreAxiomInfo
  12. lazy val DBXeq: DerivedAxiomInfo

    Darboux equality

    Axiom "DBX=".
      (e=0 -> [c&q(||)]e=0) <- [c&q(||)](e)'=g*e
    End.

    Darboux equality

    Annotations
    @Axiom( x$2323 , x$2329 , x$2330 , x$2324 , x$2328 , x$2325 , x$2331 , x$2326 , x$2327 )
    Note

    More precisely: this derivation assumes that y_,z_ do not occur, hence the more fancy space dependents.

    ,

    For soundness, the cofactor g must not mention divisions that are not guarded by the ODE domain constraint (see DG)

    See also

    André Platzer and Yong Kiam Tan. Differential Equation Invariance Axiomatization. arXiv:1905.13429, May 2019.

    DBXge

  13. lazy val DBXge: DerivedAxiomInfo

    Non-strict Darboux inequality / Grönwall inequality.

    Axiom "DBX>=".
      (e>=0 -> [c&q(||)]e>=0) <- [c&q(||)](e)'>=g*e
    End.

    Non-strict Darboux inequality / Grönwall inequality.

    Annotations
    @Axiom( x$2314 , x$2320 , x$2321 , x$2315 , x$2319 , x$2316 , x$2322 , x$2317 , x$2318 )
    Note

    More precisely: this derivation assumes that y_,z_ do not occur, hence the more fancy space dependents.

    ,

    For soundness, the cofactor g must not mention divisions that are not guarded by the ODE domain constraint (see DG)

    See also

    André Platzer and Yong Kiam Tan. Differential Equation Invariance Axiomatization. arXiv:1905.13429, May 2019.

    DBXgt

  14. lazy val DBXgt: DerivedAxiomInfo

    Strict Darboux inequality / Grönwall inequality.

    Axiom "DBX>".
      (e>0 -> [c&q(||)]e>0) <- [c&q(||)](e)'>=g*e
    End.

    Strict Darboux inequality / Grönwall inequality.

    Annotations
    @Axiom( x$2287 , x$2293 , x$2294 , x$2288 , x$2292 , x$2289 , x$2295 , x$2290 , x$2291 )
    Note

    More precisely: this derivation assumes that y_ does not occur, hence the more fancy space dependents.

    ,

    For soundness, the cofactor g must not mention divisions that are not guarded by the ODE domain constraint (see DG).

    See also

    André Platzer and Yong Kiam Tan. Differential Equation Invariance Axiomatization. arXiv:1905.13429, May 2019.

    DBXgtOpen

  15. lazy val DBXgtOpen: DerivedAxiomInfo

    Strict Darboux inequality / Grönwall inequality benefiting from open inequality in postcondition.

    Axiom "DBX> open".
      (e>0 -> [c&q(||)]e>0) <- [c&q(||)](e>0 -> (e)'>=g*e)
    End.

    Strict Darboux inequality / Grönwall inequality benefiting from open inequality in postcondition.

    Annotations
    @Axiom( x$2305 , x$2310 , x$2311 , x$2306 , x$2309 , x$2312 , x$2313 , x$2307 , x$2308 )
    Note

    More precisely: this derivation assumes that y_ does not occur, hence the more fancy space dependents.

    ,

    For soundness, the cofactor g must not mention divisions that are not guarded by the ODE domain constraint (see DG)

    See also

    André Platzer and Yong Kiam Tan. Differential Equation Invariance Axiomatization. arXiv:1905.13429, May 2019.

    DBXgt

  16. lazy val DBXle: DerivedAxiomInfo

    Non-strict Darboux inequality / Grönwall inequality.

    Axiom "DBX<=".
      (e<=0 -> [c&q(||)]e<=0) <- [c&q(||)](e)'<=g*e
    End.

    Non-strict Darboux inequality / Grönwall inequality.

    Annotations
    @Axiom( x$2341 , x$2347 , x$2348 , x$2342 , x$2346 , x$2343 , x$2349 , x$2344 , x$2345 )
    Note

    More precisely: this derivation assumes that y_,z_ do not occur, hence the more fancy space dependents.

    ,

    For soundness, the cofactor g must not mention divisions that are not guarded by the ODE domain constraint (see DG)

    See also

    André Platzer and Yong Kiam Tan. Differential Equation Invariance Axiomatization. arXiv:1905.13429, May 2019.

    DBXgt

  17. lazy val DBXltOpen: DerivedAxiomInfo

    Strict Darboux inequality / Grönwall inequality benefiting from open inequality in postcondition.

    Axiom "DBX> open".
      (e>0 -> [c&q(||)]e>0) <- [c&q(||)](e>0 -> (e)'>=g*e)
    End.

    Strict Darboux inequality / Grönwall inequality benefiting from open inequality in postcondition.

    Annotations
    @Axiom( x$2332 , x$2337 , x$2338 , x$2333 , x$2336 , x$2339 , x$2340 , x$2334 , x$2335 )
    Note

    More precisely: this derivation assumes that y_ does not occur, hence the more fancy space dependents.

    ,

    For soundness, the cofactor g must not mention divisions that are not guarded by the ODE domain constraint (see DG)

    See also

    André Platzer and Yong Kiam Tan. Differential Equation Invariance Axiomatization. arXiv:1905.13429, May 2019.

    DBXgt

  18. lazy val DBXneOpen: DerivedAxiomInfo

    Strict Darboux != benefiting from open inequality in postcondition.

    Axiom "DBX!= open".
      (e!=0 -> [c&q(||)]e!=0) <- [c&q(||)](e!=0 -> (e)'=g*e)
    End.

    Strict Darboux != benefiting from open inequality in postcondition.

    Annotations
    @Axiom( x$2350 , x$2355 , x$2356 , x$2351 , x$2354 , x$2357 , x$2358 , x$2352 , x$2353 )
    Note

    More precisely: this derivation assumes that y_ does not occur, hence the more fancy space dependents.

    ,

    For soundness, the cofactor g must not mention divisions that are not guarded by the ODE domain constraint (see DG)

    See also

    André Platzer and Yong Kiam Tan. Differential Equation Invariance Axiomatization. arXiv:1905.13429, May 2019.

    DBXgt

  19. lazy val DC: DerivedAxiomInfo

    Axiom "DC differential cut".
       ([{c&q(||)}]p(||) <-> [{c&(q(||)&r(||))}]p(||)) <- [{c&q(||)}]r(||)
    End.
    
    @Derived
    Annotations
    @Axiom( x$2053 , x$2060 , x$2061 , x$2054 , x$2058 , x$2055 , x$2059 , x$2056 , x$2057 )
  20. val DCC: CoreAxiomInfo
  21. lazy val DCdaxiom: DerivedAxiomInfo

    Axiom "DCd diamond differential cut".
      (<{c&q(||)}>p(||) <-> <{c&(q(||)&r(||))}>p(||)) <- [{c&q(||)}]r(||)
      // (p(x) <-> p(x)) <- [x'=f(x)&q(x);]r(x) THEORY
    End.
    Annotations
    @Axiom( x$2197 , x$2201 , x$2202 , x$2198 , x$2203 , x$2204 , x$2205 , x$2199 , x$2200 )
  22. val DE: CoreAxiomInfo
  23. val DEs: CoreAxiomInfo
  24. lazy val DEsysy: DerivedAxiomInfo

    Semantically renamed

    Semantically renamed

    Axiom "DE differential effect (system) y"
       // @note Soundness: f(||) cannot have ' by data structure invariant. AtomicODE requires explicit-form so f(||) cannot have differentials/differential symbols
       [{y_'=f(||),c&q(||)}]p(||) <-> [{c,y_'=f(||)&q(||)}][y_':=f(||);]p(||)
    End.
    Annotations
    @Axiom( x$568 , x$573 , x$574 , x$569 , x$575 , x$570 , x$576 , x$571 , x$572 )
    Note

    needs semantic renaming

  25. val DGC: CoreAxiomInfo
  26. val DGCa: CoreAxiomInfo
  27. lazy val DGCd: DerivedAxiomInfo

    Axiom "DGCd diamond differential ghost const".
       <{c{|y_|}&q(|y_|)}>p(|y_|) <-> \forall y_ <{c{|y_|},y_'=b(|y_|)&q(|y_|)}>p(|y_|)
    End.
    Annotations
    @Axiom( x$2170 , x$2172 , x$2173 , x$2171 , x$2174 , x$2175 , x$2176 , x$2177 , x$2178 )
  28. lazy val DGCdc: DerivedAxiomInfo
    Annotations
    @Axiom( "DGCdc" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  29. lazy val DGCde: DerivedAxiomInfo
    Annotations
    @Axiom( "DGCde" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  30. val DGa: CoreAxiomInfo
  31. lazy val DGd: DerivedAxiomInfo

    Axiom "DGd diamond differential ghost".
       <{c{|y_|}&q(|y_|)}>p(|y_|) <-> \forall y_ <{c{|y_|},y_'=(a(|y_|)*y_)+b(|y_|)&q(|y_|)}>p(|y_|)
       // p(x) <-> \forall y <{x'=f(x),y'=(a(x)*y)+b(x))&q(x)}>p(x) THEORY
    End.
    Annotations
    @Axiom( "DGd" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  32. lazy val DGdi: DerivedAxiomInfo

    Axiom "DGd diamond inverse differential ghost implicational".
       <{c{|y_|}&q(|y_|)}>p(|y_|)  ->  \exists y_ <{y_'=a(||),c{|y_|}&q(|y_|)}>p(|y_|)
    End.
    Annotations
    @Axiom( "DGdi" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  33. val DGi: CoreAxiomInfo
  34. val DGpp: CoreAxiomInfo
  35. lazy val DGpreghost: DerivedAxiomInfo

    Pre Differential Auxiliary / Differential Ghost -- not strictly necessary but saves a lot of reordering work.

    Axiom "DG differential pre-ghost".
       [{c{|y_|}&q(|y_|)}]p(|y_|) <-> \exists y_ [{y_'=(a(|y_|)*y_)+b(|y_|),c{|y_|}&q(|y_|)}]p(|y_|)
       // [x'=f(x)&q(x);]p(x) <-> \exists y [{y'=(a(x)*y)+b(x), x'=f(x))&q(x)}]p(x) THEORY
    End.

    Pre Differential Auxiliary / Differential Ghost -- not strictly necessary but saves a lot of reordering work.

    Annotations
    @Axiom( "DG" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  36. lazy val DI: DerivedAxiomInfo

    Axiom "DI differential invariant".
       [{c&q(||)}]p(||) <- (q(||)-> (p(||) & [{c&q(||)}]((p(||))')))
       // [x'=f(x)&q(x);]p(x) <- (q(x) -> (p(x) & [x'=f(x)&q(x);]((p(x))'))) THEORY
    End.
    Annotations
    @Axiom( x$2017 , x$2023 , x$2024 , x$2018 , x$2020 , x$2019 , x$2025 , x$2021 , x$2022 )
  37. val DIequiv: CoreAxiomInfo
  38. val DIogreater: CoreAxiomInfo
  39. lazy val DIoless: DerivedAxiomInfo

    Axiom "DIo open differential invariance <".
       ([{c&q(||)}]f(||)<g(||) <-> [?q(||);]f(||)<g(||)) <- (q(||) -> [{c&q(||)}](f(||)<g(||) -> (f(||)<g(||))'))
    End.
    Annotations
    @Axiom( x$2071 , x$2076 , x$2077 , x$2072 , x$2073 , x$2078 , x$2079 , x$2074 , x$2075 )
  40. val DMP: CoreAxiomInfo
  41. lazy val DR: DerivedAxiomInfo

    Axiom "DR differential refine".
       ([{c&q(||)}]p(||) <- [{c&r(||)}]p(||)) <- [{c&q(||)}]r(||)
    End.
    
    @Derived
    Annotations
    @Axiom( x$2026 , x$2031 , x$2032 , x$2027 , x$2029 , x$2033 , x$2030 , x$2028 , x$2034 )
  42. lazy val DRd: DerivedAxiomInfo

    Axiom "DR<> diamond differential refine".
       (<{c&q(||)}>p(||) <- <{c&r(||)}>p(||)) <- [{c&r(||)}]q(||)
    End.
    
    @Derived
    Annotations
    @Axiom( x$2044 , x$2049 , x$2050 , x$2045 , x$2047 , x$2051 , x$2048 , x$2046 , x$2052 )
  43. val DS: CoreAxiomInfo
  44. lazy val DSddomain: DerivedAxiomInfo

    Axiom "Dsol& differential equation solution".
       <{x'=c()&q(x)}>p(||) <-> \exists t (t>=0 & ((\forall s ((0<=s&s<=t) -> q(x+(c()*s)))) & <x:=x+(c()*t);>p(||)))
    End.
    Annotations
    @Axiom( x$2134 , x$2136 , x$2137 , x$2138 , x$2135 , x$2139 , x$2140 , x$2141 , x$2142 )
  45. lazy val DSdnodomain: DerivedAxiomInfo

    Axiom "Dsol differential equation solution".
       <{x'=c()}>p(x) <-> \exists t (t>=0 & <x:=x+(c()*t);>p(x))
    End.
    Annotations
    @Axiom( x$2125 , x$2130 , x$2131 , x$2126 , x$2129 , x$2132 , x$2133 , x$2127 , x$2128 )
    To do

    postcondition formulation is weaker than that of DS&

  46. lazy val DSnodomain: DerivedAxiomInfo

    Axiom "DS differential equation solution".
       [{x'=c()}]p(x) <-> \forall t (t>=0 -> [x:=x+(c()*t);]p(x))
    End.
    Annotations
    @Axiom( x$2107 , x$2112 , x$2113 , x$2108 , x$2111 , x$2114 , x$2115 , x$2109 , x$2110 )
    To do

    postcondition formulation is weaker than that of DS&

  47. lazy val DW: DerivedAxiomInfo

    Axiom "DW differential weakening".
       [{c&q(||)}]p(||) <-> ([{c&q(||)}](q(||)->p(||)))
       /* [x'=f(x)&q(x);]p(x) <-> ([x'=f(x)&q(x);](q(x)->p(x))) THEORY */
    End.
    Annotations
    @Axiom( x$1981 , x$1986 , x$1987 , x$1982 , x$1985 , x$1988 , x$1989 , x$1983 , x$1984 )
    See also

    footnote 3 in "Andre Platzer. A uniform substitution calculus for differential dynamic logic. In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, volume 9195 of LNCS, pages 467-481. Springer, 2015. arXiv 1503.01981, 2015."

  48. lazy val DWQinitial: DerivedAxiomInfo

    Axiom "DW Q initial".
       (q(||) -> [{c&q(||)}]p(||)) <-> [{c&q(||)}]p(||)
    End.
    Annotations
    @Axiom( x$2008 , x$2010 , x$2011 , x$2009 , x$2012 , x$2013 , x$2014 , x$2015 , x$2016 )
  49. val DWbase: CoreAxiomInfo
  50. lazy val DWd: DerivedAxiomInfo

    Axiom "DWd diamond differential weakening".
       <{c&q_(||)}>p_(||) <-> <{c&q_(||)}>(q_(||)&p_(||))
    End.
    Annotations
    @Axiom( "DWd" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  51. lazy val DWd2: DerivedAxiomInfo

    Axiom "DWd2 diamond differential weakening".
       <{c&q_(||)}>p_(||) <-> <{c&q_(||)}>(q_(||)->p_(||))
    End.
    Annotations
    @Axiom( "DWd2" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  52. lazy val DWdQinitial: DerivedAxiomInfo

    Axiom "DWd Q initial".
       q_(||)&<{c&q_(||)}>p_(||) <-> <{c&q_(||)}>p_(||)
    End.
    Annotations
    @Axiom( "DWd Q initial" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  53. lazy val DWeakenAnd: DerivedAxiomInfo

    Axiom "DW differential weakening and".
       [{c&q(||)}]p(||) -> ([{c&q(||)}](q(||)&p(||)))
    End.
    Annotations
    @Axiom( x$1999 , x$2001 , x$2002 , x$2000 , x$2003 , x$2004 , x$2005 , x$2006 , x$2007 )
  54. val DX: CoreAxiomInfo
  55. val Dand: CoreAxiomInfo
  56. lazy val DassignDual2: DerivedAxiomInfo
    Annotations
    @Axiom( "':=D" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  57. val Dassignb: CoreAxiomInfo
  58. val Dassignbeq: CoreAxiomInfo
  59. lazy val Dassignbequalityexists: DerivedAxiomInfo
    Annotations
    @Axiom( ("[':=]", "[':=] assign exists") , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  60. lazy val Dassignby: DerivedAxiomInfo

    Axiom "[':=] differential assign y".
       [y_':=f();]p(y_') <-> p(f())
    End.
    Annotations
    @Axiom( x$1324 , x$1328 , x$1329 , x$1325 , x$1326 , x$1327 , x$1330 , x$1331 , x$1332 )
  61. lazy val Dassignd: DerivedAxiomInfo

    Axiom "<':=> differential assign".
       <v':=t();>p(v') <-> p(t())
    End.
    Annotations
    @Axiom( x$1333 , x$1336 , x$1337 , x$1338 , x$1339 , x$1340 , x$1341 , x$1334 , x$1335 )
  62. lazy val DassigndAxiom: DerivedAxiomInfo
    Annotations
    @Axiom( x$1243 , x$1248 , x$1249 , x$1244 , x$1247 , x$1250 , x$1251 , x$1245 , x$1246 )
  63. lazy val DassigndEqualityAxiom: DerivedAxiomInfo
    Annotations
    @Axiom( x$1261 , x$1266 , x$1267 , x$1262 , x$1268 , x$1263 , x$1269 , x$1264 , x$1265 )
  64. val Dcomp: CoreAxiomInfo
  65. val Dcompose: CoreAxiomInfo
  66. val Dconst: CoreAxiomInfo
  67. val Dequal: DerivedAxiomInfo
  68. val Dexists: CoreAxiomInfo
  69. val Dforall: CoreAxiomInfo
  70. val Dgreater: CoreAxiomInfo
  71. val Dgreaterequal: CoreAxiomInfo
  72. lazy val Dimply: DerivedAxiomInfo

    Axiom "->' derive imply".
       (p(||) -> q(||))' <-> (!p(||) | q(||))'
    End.
    Annotations
    @Axiom( x$1846 , x$1851 , x$1852 , x$1847 , x$1850 , x$1853 , x$1854 , x$1848 , x$1849 )
  73. val Dless: DerivedAxiomInfo

    Axiom "<' derive <"
       (f(||) < g(||))' <-> ((f(||))' <= (g(||))')
       // sic(!) easier
    End.
  74. val Dlessequal: DerivedAxiomInfo

    Axiom "<=' derive <=".
       (f(||) <= g(||))' <-> ((f(||))' <= (g(||))')
    End.
  75. lazy val Dlinear: DerivedAxiomInfo

    Axiom "' linear".
       (c()*f(||))' = c()*(f(||))'
    End.
    Annotations
    @Axiom( x$2503 , x$2507 , x$2508 , x$2509 , x$2504 , x$2510 , x$2511 , x$2505 , x$2506 )
  76. lazy val DlinearRight: DerivedAxiomInfo

    Axiom "' linear right".
       (f(||)*c())' = f(||)'*c()
    End.
    Annotations
    @Axiom( x$2530 , x$2534 , x$2535 , x$2536 , x$2533 , x$2537 , x$2538 , x$2531 , x$2532 )
  77. val Dminus: CoreAxiomInfo
  78. val Dneg: CoreAxiomInfo
  79. val Dnotequal: DerivedAxiomInfo

    Axiom "!=' derive !="
       (f(||) != g(||))' <-> ((f(||))' = (g(||))')
       // sic!
    End.
  80. val Dor: CoreAxiomInfo
  81. val Dplus: CoreAxiomInfo
  82. val Dpower: CoreAxiomInfo
  83. val Dquotient: CoreAxiomInfo
  84. val Dselfassignb: CoreAxiomInfo
  85. val Dtimes: CoreAxiomInfo
  86. val DvarAxiom: CoreAxiomInfo
  87. lazy val DvariableAxiom: DerivedAxiomInfo

    Axiom "x' derive variable".
       \forall x_ ((x_)' = x_')
    End.
    Annotations
    @Axiom( x$2494 , x$2496 , x$2497 , x$2495 , x$2498 , x$2499 , x$2500 , x$2501 , x$2502 )
  88. lazy val DvariableCommutedAxiom: DerivedAxiomInfo

    Axiom "x' derive var commuted".
       (x_') = (x_)'
    End.
    Annotations
    @Axiom( x$2476 , x$2477 , x$2482 , x$2478 , x$2479 , x$2483 , x$2484 , x$2480 , x$2481 )
  89. val FPrule: AxiomaticRuleInfo
  90. lazy val Goedel: DerivedRuleInfo

    Rule "Goedel".

    Rule "Goedel". Premise p(||) Conclusion [a;]p(||) End.

        p(||)
    ----------- G
     [a{|^@|};]p(||)
    Annotations
    @ProofRule( x$721 , x$724 , x$725 , x$723 , x$722 , x$726 , x$727 , x$728 , x$729 )
    Note

    Unsound for hybrid games

  91. lazy val I: DerivedAxiomInfo

    Axiom "Ieq induction".
       [{a;}*]p(||) <-> p(||) & [{a;}*](p(||)->[{a;}]p(||))
    End.
    Annotations
    @Axiom( x$1540 , x$1546 , x$1547 , x$1541 , x$1545 , x$1542 , x$1548 , x$1543 , x$1544 )
    See also

    Section 7.7.4 in textbook

  92. lazy val IIinduction: DerivedAxiomInfo

    Axiom "II induction".
       [{a;}*](p(||)->[a;]p(||)) -> (p(||)->[{a;}*]p(||))
    End.
    Annotations
    @Axiom( x$1459 , x$1461 , x$1462 , x$1463 , x$1464 , x$1460 , x$1465 , x$1466 , x$1467 )
  93. val IVT: CoreAxiomInfo
  94. val Iind: CoreAxiomInfo
  95. val K: CoreAxiomInfo
  96. lazy val KDomD: DerivedAxiomInfo

    Axiom "K<&>".
       [{c & q(||) & !p(||)}]!r(||) -> (<{c & q(||)}>r(||) -> <{c & q(||)}>p(||))
    End.
    Annotations
    @Axiom( x$3133 , x$3137 , x$3138 , x$3134 , x$3139 , x$3140 , x$3141 , x$3135 , x$3136 )
    Note

    postcondition refinement

  97. lazy val Kand: DerivedAxiomInfo

    Axiom "K modal modus ponens &".
       [a;](p_(||)->q_(||)) & [a;]p_(||) -> [a;]q_(||)
    End.
    Annotations
    @Axiom( x$1099 , x$1104 , x$1105 , x$1100 , x$1103 , x$1106 , x$1107 , x$1101 , x$1102 )
    Note

    unsound for hybrid games

  98. lazy val Kd: DerivedAxiomInfo

    Axiom "Kd diamond modus ponens".
      [a{|^@|};](p(||)->q(||)) -> (<a{|^@|};>p(||) -> <a{|^@|};>q(||))
    End.
    Annotations
    @Axiom( x$1054 , x$1059 , x$1060 , x$1055 , x$1058 , x$1061 , x$1062 , x$1056 , x$1057 )
  99. lazy val Kd2: DerivedAxiomInfo

    Axiom "Kd2 diamond modus ponens".
      [a{|^@|};]p(||) -> (<a{|^@|};>q(||) -> <a{|^@|};>(p(||)&q(||)))
    End.
    Annotations
    @Axiom( x$1072 , x$1077 , x$1078 , x$1073 , x$1076 , x$1079 , x$1080 , x$1074 , x$1075 )
  100. lazy val PC1: DerivedAxiomInfo

    Axiom "PC1".
       p()&q() -> p()
    End.
    Annotations
    @Axiom( x$1144 , x$1146 , x$1147 , x$1148 , x$1145 , x$1149 , x$1150 , x$1151 , x$1152 )
    Note

    implements Cresswell, Hughes. A New Introduction to Modal Logic, PC1

  101. lazy val PC10: DerivedAxiomInfo

    Axiom "PC10".
       q() -> p() | q()
    End.
    Annotations
    @Axiom( x$1711 , x$1713 , x$1714 , x$1715 , x$1712 , x$1716 , x$1717 , x$1718 , x$1719 )
    Note

    implements Cresswell, Hughes. A New Introduction to Modal Logic, PC10

  102. lazy val PC2: DerivedAxiomInfo

    Axiom "PC2".
       p()&q() -> q()
    End.
    Annotations
    @Axiom( x$1207 , x$1209 , x$1210 , x$1211 , x$1208 , x$1212 , x$1213 , x$1214 , x$1215 )
    Note

    implements Cresswell, Hughes. A New Introduction to Modal Logic, PC2

  103. lazy val PC3: DerivedAxiomInfo

    Axiom "PC3".
       p()&q() -> ((p()->r())->(p()->q()&r())) <-> true
    End.
    Annotations
    @Axiom( x$1693 , x$1695 , x$1696 , x$1697 , x$1694 , x$1698 , x$1699 , x$1700 , x$1701 )
    Note

    implements Cresswell, Hughes. A New Introduction to Modal Logic, PC3

  104. lazy val PC9: DerivedAxiomInfo

    Axiom "PC9".
       p() -> p() | q()
    End.
    Annotations
    @Axiom( x$1702 , x$1704 , x$1705 , x$1706 , x$1703 , x$1707 , x$1708 , x$1709 , x$1710 )
    Note

    implements Cresswell, Hughes. A New Introduction to Modal Logic, PC9

  105. val RI: CoreAxiomInfo
  106. val RIclosedgeq: CoreAxiomInfo
  107. lazy val TExge: DerivedAxiomInfo

    ODELiveness

    ODELiveness

    Annotations
    @Axiom( "TExge" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  108. lazy val TExgt: DerivedAxiomInfo
    Annotations
    @Axiom( "TExgt" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  109. val Uniq: CoreAxiomInfo
  110. lazy val UniqIff: DerivedAxiomInfo

    Axiom "Uniq uniqueness iff"
       <{c&q(||)}>p(||) & <{c&r(||)}>p(||) <-> <{c & q(||)&r(||)}>(p(||))
    End.
    Annotations
    @Axiom( x$2539 , x$2544 , x$2545 , x$2540 , x$2543 , x$2546 , x$2547 , x$2541 , x$2542 )
  111. lazy val V: DerivedAxiomInfo

      Axiom "V vacuous".
     p() -> [a{|^@|};]p()
    End.
    Annotations
    @Axiom( x$730 , x$735 , x$736 , x$731 , x$734 , x$737 , x$738 , x$732 , x$733 )
    Note

    unsound for hybrid games

  112. val VK: CoreAxiomInfo
  113. lazy val abs: DerivedAxiomInfo

    Axiom "abs".
      (abs(s()) = t()) <->  ((s()>=0 & t()=s()) | (s()<0 & t()=-s()))
    End.
    Annotations
    @Axiom( "abs" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  114. lazy val allDist: DerivedAxiomInfo

    Axiom "all distribute".
      (\forall x (p(x)->q(x))) -> ((\forall x p(x))->(\forall x q(x)))
    Annotations
    @Axiom( x$1027 , x$1031 , x$1032 , x$1028 , x$1033 , x$1034 , x$1035 , x$1029 , x$1030 )
  115. lazy val allDistElim: DerivedAxiomInfo

    Axiom "all distribute elim".
      (\forall x (P->Q)) -> ((\forall x P)->(\forall x Q))
    Annotations
    @Axiom( x$712 , x$716 , x$717 , x$713 , x$718 , x$719 , x$720 , x$714 , x$715 )
  116. lazy val allGeneralize: DerivedRuleInfo

    Rule "all generalization".

    Rule "all generalization". Premise p(||) Conclusion \forall x p(||) End.

    Annotations
    @ProofRule( x$676 , x$679 , x$680 , x$677 , x$678 , x$681 , x$682 , x$683 , x$684 )
    Note

    generalization of p(x) to p(||) as in Theorem 14

  117. lazy val allInst: DerivedAxiomInfo

    Axiom /*\\foralli */ "all instantiate"
       (\forall x_ p(x_)) -> p(f())
    End.
    Annotations
    @Axiom( x$748 , x$752 , x$753 , x$749 , x$754 , x$755 , x$756 , x$750 , x$751 )
    Note

    Core axiom derivable thanks to [:=]= and [:=]

  118. lazy val allInstPrime: DerivedAxiomInfo
    Annotations
    @Axiom( x$775 , x$779 , x$780 , x$776 , x$781 , x$782 , x$783 , x$777 , x$778 )
  119. val allPd: CoreAxiomInfo
  120. lazy val allStutter: DerivedAxiomInfo

    Axiom "all stutter".
       \forall x P <-> \forall x P
    End.
    Annotations
    @Axiom( x$3052 , x$3056 , x$3057 , x$3058 , x$3059 , x$3055 , x$3060 , x$3053 , x$3054 )
    Note

    Trivial reflexive stutter axiom, only used with a different recursor pattern in AxiomIndex.

  121. lazy val allStutterPrime: DerivedAxiomInfo
    Annotations
    @Axiom( x$3061 , x$3065 , x$3066 , x$3067 , x$3068 , x$3064 , x$3069 , x$3062 , x$3063 )
  122. lazy val allSubstitute: DerivedAxiomInfo

    Axiom "all substitute".
       (\forall x (x=t() -> p(x))) <-> p(t())
    End.
    Annotations
    @Axiom( x$1297 , x$1301 , x$1302 , x$1298 , x$1303 , x$1304 , x$1305 , x$1299 , x$1300 )
  123. lazy val allThenExists: DerivedAxiomInfo

    Axiom "all then exists".
       (\forall x p(||)) -> (\exists x p(||))
    End.
    Annotations
    @Axiom( x$1576 , x$1578 , x$1579 , x$1577 , x$1580 , x$1581 , x$1582 , x$1583 , x$1584 )
    See also

    forallThenExists

  124. lazy val allV: DerivedAxiomInfo

    Axiom "vacuous all quantifier"
      (\forall x_ p()) <-> p()
    End.
    Annotations
    @Axiom( x$802 , x$805 , x$806 , x$807 , x$808 , x$809 , x$810 , x$803 , x$804 )
    Note

    Half of this is a base axiom officially but already derives from [:*] and V

  125. val alld: CoreAxiomInfo

    all dual

  126. lazy val alldt: DerivedAxiomInfo

    Semantically renamed

    Semantically renamed

    Axiom "all dual time"
       (!\exists t_ !p(||)) <-> \forall t_ p(||)
    End.
    Annotations
    @Axiom( x$586 , x$588 , x$589 , x$590 , x$591 , x$587 , x$592 , x$593 , x$594 )
    Note

    needs semantic renaming

  127. lazy val alldy: DerivedAxiomInfo

    Semantically renamed

    Semantically renamed

    Axiom "all dual y"
       (!\exists y_ !p(||)) <-> \forall y_ p(||)
    End.
    Annotations
    @Axiom( x$577 , x$579 , x$580 , x$581 , x$582 , x$578 , x$583 , x$584 , x$585 )
    Note

    needs semantic renaming

  128. val alle: CoreAxiomInfo

    all eliminate

  129. val alleprime: CoreAxiomInfo
  130. lazy val ally: DerivedAxiomInfo

    Semantically renamed

    Semantically renamed

    Axiom "all eliminate y"
      (\forall y_ p(||)) -> p(||)
    End.
    Annotations
    @Axiom( x$595 , x$597 , x$598 , x$599 , x$600 , x$596 , x$601 , x$602 , x$603 )
    Note

    needs semantic renaming

  131. lazy val andAssoc: DerivedAxiomInfo

    Axiom "& associative".
       ((p() & q()) & r()) <-> (p() & (q() & r()))
    End.
    Annotations
    @Axiom( x$1639 , x$1643 , x$1644 , x$1645 , x$1642 , x$1646 , x$1647 , x$1640 , x$1641 )
  132. lazy val andCommute: DerivedAxiomInfo

    Axiom "& commute".
       (p() & q()) <-> (q() & p())
    End.
    Annotations
    @Axiom( x$1612 , x$1616 , x$1617 , x$1618 , x$1615 , x$1619 , x$1620 , x$1613 , x$1614 )
  133. lazy val andFalse: DerivedAxiomInfo

    Axiom "&false".
       (p()&false) <-> false
    End.
    Annotations
    @Axiom( x$1882 , x$1885 , x$1886 , x$1883 , x$1884 , x$1887 , x$1888 , x$1889 , x$1890 )
  134. lazy val andImplies: DerivedAxiomInfo

    Axiom "&->".
       (A() & B() -> C()) <-> (A() -> B() -> C())
    End.
    Annotations
    @Axiom( "&->" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  135. lazy val andRecursor: DerivedAxiomInfo

    Axiom "& recursor".
       p() & q() <-> p() & q()
    End.
    Annotations
    @Axiom( x$2701 , x$2705 , x$2706 , x$2707 , x$2702 , x$2708 , x$2709 , x$2703 , x$2704 )
  136. lazy val andReflexive: DerivedAxiomInfo

    Axiom "& reflexive".
       p() & p() <-> p()
    End.
    Annotations
    @Axiom( x$1657 , x$1661 , x$1662 , x$1663 , x$1660 , x$1664 , x$1665 , x$1658 , x$1659 )
  137. lazy val andStutter: DerivedAxiomInfo

    Axiom "and stutter".
       P&Q <-> P&Q
    End.
    Annotations
    @Axiom( x$3088 , x$3092 , x$3093 , x$3094 , x$3095 , x$3091 , x$3096 , x$3089 , x$3090 )
    Note

    Trivial reflexive stutter axiom, only used with a different recursor pattern in AxiomIndex.

  138. lazy val andTrue: DerivedAxiomInfo

    Axiom "&true".
       (p()&true) <-> p()
    End.
    Annotations
    @Axiom( x$1081 , x$1084 , x$1085 , x$1082 , x$1083 , x$1086 , x$1087 , x$1088 , x$1089 )
  139. lazy val andTrueInv: DerivedAxiomInfo
    Annotations
    @Axiom( x$1891 , x$1894 , x$1895 , x$1896 , x$1897 , x$1898 , x$1899 , x$1892 , x$1893 )
  140. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  141. lazy val assignDAxiomb: ProvableSig

    Axiom "[':=] differential assign".
       [x_':=f();]p(x_') <-> p(f())
    End.
  142. lazy val assignDual: DerivedAxiomInfo

    Axiom ":= assign dual".
       <v:=t();>p(v) <-> [v:=t();]p(v)
    End.
    Annotations
    @Axiom( ":=D" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
    See also

    assignDual2

  143. lazy val assignDual2: DerivedAxiomInfo

    Axiom ":= assign dual 2".
       <x:=f();>p(||) <-> [x:=f();]p(||)
    End.
    Annotations
    @Axiom( x$1216 , x$1220 , x$1221 , x$1217 , x$1222 , x$1223 , x$1224 , x$1218 , x$1219 )
    See also

    assignDual

  144. val assignbAxiom: CoreAxiomInfo
  145. lazy val assignball: DerivedAxiomInfo

    Axiom "[:=] assign all".
     \forall x_ p_(||) -> [x_:=f_();]p_(||)
    End.
    Annotations
    @Axiom( ("[:=]∀","[:=]all") , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  146. val assignbeq: CoreAxiomInfo
  147. lazy val assignbequalityexists: DerivedAxiomInfo

    Axiom "[:=] assign equality exists".
      [x:=f();]p(||) <-> \exists x (x=f() & p(||))
    End.
    Annotations
    @Axiom( ("[:=]", "[:=] assign exists") , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
    To do

    does not derive yet

  148. lazy val assignbequational: DerivedAxiomInfo

    Axiom "[:=] assign equational".
       [v:=t();]p(v) <-> \forall v (v=t() -> p(v))
    End.
    Annotations
    @Axiom( x$1288 , x$1291 , x$1292 , x$1293 , x$1294 , x$1295 , x$1296 , x$1289 , x$1290 )
  149. lazy val assignbeqy: DerivedAxiomInfo

    Semantically renamed

    Semantically renamed

    Axiom "[:=] assign equality y"
       [y_:=f();]p(||) <-> \forall y_ (y_=f() -> p(||))
    End.
    Annotations
    @Axiom( x$550 , x$552 , x$553 , x$554 , x$555 , x$551 , x$556 , x$557 , x$558 )
    Note

    needs semantic renaming

  150. lazy val assignbexists: DerivedAxiomInfo

    Axiom "[:=] assign exists".
     [x_:=f_();]p_(||) -> \exists x_ p_(||)
    End.
    Annotations
    @Axiom( x$1270 , x$1274 , x$1275 , x$1276 , x$1277 , x$1271 , x$1278 , x$1272 , x$1273 )
  151. lazy val assignbup: DerivedAxiomInfo

    Axiom "[:=] assign update".
       [x:=t();]P <-> [x:=t();]P
    End.
    Annotations
    @Axiom( x$1306 , x$1309 , x$1310 , x$1311 , x$1312 , x$1313 , x$1314 , x$1307 , x$1308 )
    Note

    Trivial reflexive stutter axiom, only used with a different recursor pattern in AxiomIndex.

  152. lazy val assigndAxiom: DerivedAxiomInfo

    Axiom "<:=> assign".
       <v:=t();>p(v) <-> p(t())
    End.
    Annotations
    @Axiom( x$1225 , x$1230 , x$1231 , x$1226 , x$1229 , x$1232 , x$1233 , x$1227 , x$1228 )
  153. lazy val assigndEqualityAll: DerivedAxiomInfo

    Axiom "<:=> assign equality all".
       <x:=f();>p(||) <-> \forall x (x=f() -> p(||))
    End.
    Annotations
    @Axiom( x$1279 , x$1282 , x$1283 , x$1284 , x$1285 , x$1286 , x$1287 , x$1280 , x$1281 )
  154. lazy val assigndEqualityAxiom: DerivedAxiomInfo

    Axiom "<:=> assign equality".
       <x:=f();>p(||) <-> \exists x (x=f() & p(||))
    End.
    Annotations
    @Axiom( x$1252 , x$1257 , x$1258 , x$1253 , x$1259 , x$1254 , x$1260 , x$1255 , x$1256 )
  155. lazy val assigndup: DerivedAxiomInfo

    Axiom "<:=> assign update".
       <x:=t();>P <-> <x:=t();>P
    End.
    Annotations
    @Axiom( x$1315 , x$1318 , x$1319 , x$1320 , x$1321 , x$1322 , x$1323 , x$1316 , x$1317 )
    Note

    Trivial reflexive stutter axiom, only used with a different recursor pattern in AxiomIndex.

  156. lazy val backiterateb: DerivedAxiomInfo

    Axiom "[*-] backiterate".
       [{a;}*]p(||) <-> p(||) & [{a;}*][{a;}]p(||)
    End.
    Annotations
    @Axiom( x$1513 , x$1517 , x$1518 , x$1519 , x$1516 , x$1520 , x$1521 , x$1514 , x$1515 )
    See also

    Lemma 7.5 in textbook

  157. lazy val backiteratebnecc: DerivedAxiomInfo

    Axiom "[*-] backiterate necessity".
       [{a;}*]p(||) -> p(||) & [{a;}*][{a;}]p(||)
    End.
    Annotations
    @Axiom( x$1522 , x$1524 , x$1525 , x$1526 , x$1527 , x$1523 , x$1528 , x$1529 , x$1530 )
    See also

    Figure 7.8 in textbook

  158. lazy val backiteratebsuff: DerivedAxiomInfo

    Axiom "[*-] backiterate sufficiency".
       [{a;}*]p(||) <- p(||) & [{a;}*][{a;}]p(||)
    End.
    Annotations
    @Axiom( x$1531 , x$1533 , x$1534 , x$1535 , x$1536 , x$1532 , x$1537 , x$1538 , x$1539 )
    See also

    Lemma 7.5 in textbook

  159. val barcan: CoreAxiomInfo
  160. lazy val box: DerivedAxiomInfo

    Axiom "[] box".
       (!<a;>(!p(||))) <-> [a;]p(||)
    End.
    Annotations
    @Axiom( x$640 , x$646 , x$647 , x$641 , x$645 , x$642 , x$648 , x$643 , x$644 )
    Note

    almost same proof as "exists dual"

  161. lazy val boxAnd: DerivedAxiomInfo

    Axiom "[] split".
       [a;](p(||)&q(||)) <-> [a;]p(||)&[a;]q(||)
    End.
    Annotations
    @Axiom( x$1108 , x$1114 , x$1115 , x$1109 , x$1113 , x$1110 , x$1116 , x$1111 , x$1112 )
    Note

    unsound for hybrid games

    ,

    implements Cresswell, Hughes. A New Introduction to Modal Logic, K3 p. 28

  162. lazy val boxDiamondPropagation: DerivedAxiomInfo

    Axiom "[]~><> propagation".
       [a;]p(||) & <a;>q(||) -> <a;>(p(||) & q(||))
    End.
    Annotations
    @Axiom( "[]~><>" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
    Note

    unsound for hybrid games

  163. lazy val boxDiamondSubstPropagation: DerivedAxiomInfo

    Axiom "[]~><> subst propagation".
       <a;>true -> ([a;]p(||) -> <a;>p(||))
    End.
    Annotations
    @Axiom( "[]~><> subst" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
    Note

    unsound for hybrid games

  164. lazy val boxImpliesAnd: DerivedAxiomInfo

    Axiom "[] conditional split".
       [a;](p(||)->q(||)&r(||)) <-> [a;](p(||)->q(||)) & [a;](p(||)->r(||))
    End.
    Annotations
    @Axiom( x$1135 , x$1138 , x$1139 , x$1136 , x$1137 , x$1140 , x$1141 , x$1142 , x$1143 )
    Note

    unsound for hybrid games

  165. lazy val boxOrLeft: DerivedAxiomInfo

    Axiom "[] or left".
       [a;](p(||)) -> [a;](p(||)|[a;]q(||))
    End.
    Annotations
    @Axiom( x$1117 , x$1121 , x$1122 , x$1118 , x$1123 , x$1119 , x$1124 , x$1120 , x$1125 )
  166. lazy val boxOrRight: DerivedAxiomInfo

    Axiom "[] or right".
       [a;](p(||)) -> [a;](p(||)|[a;]q(||))
    End.
    Annotations
    @Axiom( x$1126 , x$1130 , x$1131 , x$1127 , x$1132 , x$1128 , x$1133 , x$1129 , x$1134 )
  167. val boxTrueAxiom: CoreAxiomInfo
  168. lazy val boxTrueTrue: ProvableSig
  169. lazy val branch2GrowLeft: DerivedAxiomInfo

    Annotations
    @Axiom( "branch2GrowLeft" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
    Note

    for the Left case, could actually just use branch2Left

  170. lazy val branch2GrowRight: DerivedAxiomInfo
    Annotations
    @Axiom( "branch2GrowRight" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  171. lazy val branch2Left: DerivedAxiomInfo
    Annotations
    @Axiom( "branch2Left " , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  172. lazy val branch2Right: DerivedAxiomInfo
    Annotations
    @Axiom( "branch2Right" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  173. lazy val branch2Value: DerivedAxiomInfo
    Annotations
    @Axiom( "branch2Value" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  174. lazy val branch3GrowLeft: DerivedAxiomInfo
    Annotations
    @Axiom( "branch3GrowLeft" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  175. lazy val branch3GrowMid: DerivedAxiomInfo
    Annotations
    @Axiom( "branch3GrowMid" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  176. lazy val branch3GrowRight: DerivedAxiomInfo
    Annotations
    @Axiom( "branch3GrowRight" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  177. lazy val branch3Left: DerivedAxiomInfo
    Annotations
    @Axiom( "branch3Left" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  178. lazy val branch3Mid: DerivedAxiomInfo
    Annotations
    @Axiom( "branch3Mid" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  179. lazy val branch3Right: DerivedAxiomInfo
    Annotations
    @Axiom( "branch3Right" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  180. lazy val branch3Value1: DerivedAxiomInfo
    Annotations
    @Axiom( "branch3Value1" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  181. lazy val branch3Value2: DerivedAxiomInfo
    Annotations
    @Axiom( "branch3Value2" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  182. val choiceb: CoreAxiomInfo
  183. lazy val choiced: DerivedAxiomInfo

    Axiom "<++> choice".
       <a;++b;>p(||) <-> (<a;>p(||) | <b;>p(||))
    End.
    Annotations
    @Axiom( x$1387 , x$1393 , x$1394 , x$1388 , x$1392 , x$1389 , x$1395 , x$1390 , x$1391 )
    To do

    first show de Morgan

  184. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  185. lazy val coefficientBigDecimalPrv: DerivedAxiomInfo
    Annotations
    @Axiom( "coefficientBigDecimalPrv" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  186. lazy val coefficientNegPrv: DerivedAxiomInfo
    Annotations
    @Axiom( "coefficientNegPrv" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  187. lazy val coefficientPlusPrv: DerivedAxiomInfo
    Annotations
    @Axiom( "coefficientPlusPrv" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  188. lazy val coefficientTimesPrv: DerivedAxiomInfo
    Annotations
    @Axiom( "coefficientTimesPrv" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  189. val commaCommute: CoreAxiomInfo
  190. lazy val commaCommuteD: DerivedAxiomInfo
    Annotations
    @Axiom( ", commute diamond" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  191. lazy val commaCommuted: DerivedAxiomInfo

    Axiom "DCd diamond differential cut".
      (<{c&q(||)}>p(||) <-> <{c&(q(||)&r(||))}>p(||)) <- [{c&q(||)}]r(||)
      // (p(x) <-> p(x)) <- [x'=f(x)&q(x);]r(x) THEORY
    End.
    Annotations
    @Axiom( "commaCommuted" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  192. val commaSort: CoreAxiomInfo
  193. val composeb: CoreAxiomInfo
  194. lazy val composed: DerivedAxiomInfo

    Axiom "<;> compose".
       <a;b;>p(||) <-> <a;><b;>p(||)
    End.
    Annotations
    @Axiom( x$1405 , x$1411 , x$1412 , x$1406 , x$1410 , x$1407 , x$1413 , x$1408 , x$1409 )
  195. lazy val conflat: DerivedRuleInfo

    Rule "con convergence flat".

    Rule "con convergence flat". Premisses: \exists x_ (x <= 0 & J(||)) |- P x_ > 0, J(||) |- <a{|x_|}><x_:=x_-1;> J(||) Conclusion \exists x_ J(||) |- <a{|x_|}*>P(||)

    \exists x_ (x_ <= 0 & J(x_)) |- P   x_ > 0, J(x_) |- <a{|x_|}>J(x_-1)
    ------------------------------------------------- con
     \exists x_ J(x_) |- <a{|x_|}*>P
    Annotations
    @ProofRule( x$901 , x$904 , x$905 , x$903 , x$902 , x$906 , x$907 , x$908 , x$909 )
  196. val conrule: AxiomaticRuleInfo
  197. lazy val constCongruence: DerivedAxiomInfo

    Axiom "const congruence"
         s() = t() -> ctxT_(s()) = ctxT_(t())
    End.
    Annotations
    @Axiom( x$928 , x$932 , x$933 , x$934 , x$931 , x$935 , x$936 , x$929 , x$930 )
  198. lazy val constFormulaCongruence: DerivedAxiomInfo

    Axiom "const formula congruence"
       s() = t() -> (ctxF_(s()) <-> ctxF_(t()))
    End.
    Annotations
    @Axiom( x$937 , x$941 , x$942 , x$943 , x$940 , x$944 , x$945 , x$938 , x$939 )
  199. lazy val constLemma: DerivedAxiomInfo
    Annotations
    @Axiom( "constLemma" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  200. lazy val contraposition2Rule: DerivedRuleInfo

    Rule "contra2".

    Rule "contra2". Premise !q(||) ==> !p(||) Conclusion p(||) ==> q(||) End.

    Annotations
    @ProofRule( x$613 , x$616 , x$617 , x$614 , x$615 , x$618 , x$619 , x$620 , x$621 )
  201. lazy val converseImply: DerivedAxiomInfo

    Contraposition

    Axiom "-> converse".
       (p() -> q()) <-> (!q() -> !p())
    End.

    Contraposition

    Annotations
    @Axiom( x$1045 , x$1048 , x$1049 , x$1050 , x$1051 , x$1052 , x$1053 , x$1046 , x$1047 )
  202. lazy val dBarcan: DerivedAxiomInfo

    Axiom "Kd diamond modus ponens".
      [a{|^@|};](p(||)->q(||)) -> (<a{|^@|};>p(||) -> <a{|^@|};>q(||))
    End.
    Annotations
    @Axiom( x$3160 , x$3166 , x$3167 , x$3161 , x$3165 , x$3162 , x$3168 , x$3163 , x$3164 )
  203. lazy val dDX: DerivedAxiomInfo

    Axiom "DX diamond differential skip".
       <{c&q(||)}>p(||) <- q(||)&p(||)
    End.
    Annotations
    @Axiom( x$2089 , x$2094 , x$2095 , x$2090 , x$2093 , x$2096 , x$2097 , x$2091 , x$2092 )
  204. def derivedAxiom(canonicalName: String, derived: ⇒ Sequent, tactic: ⇒ BelleExpr, codeNameOpt: Option[String] = None): DerivedAxiomInfo

    Derive an axiom for the given derivedAxiom with the given tactic, package it up as a Lemma and make it available

  205. def derivedAxiomFromFact(canonicalName: String, derived: Formula, fact: ProvableSig, codeNameOpt: Option[String] = None): DerivedAxiomInfo

    Derive an axiom from the given provable, package it up as a Lemma and make it available

  206. def derivedFact(name: String, fact: ProvableSig, storedNameOpt: Option[String] = None): DerivedAxiomInfo

    Derive an axiom from the given provable, package it up as a Lemma and make it available

  207. def derivedFormula(name: String, derived: Formula, tactic: ⇒ BelleExpr, codeNameOpt: Option[String] = None): DerivedAxiomInfo

    Derive an axiom for the given derivedAxiom with the given tactic, package it up as a Lemma and make it available

  208. def derivedRule(name: String, fact: ProvableSig, codeNameOpt: Option[String]): DerivedRuleInfo
  209. val diamond: CoreAxiomInfo
  210. lazy val diamondOr: DerivedAxiomInfo

    Axiom "<> split".
       <a;>(p(||)|q(||)) <-> <a;>p(||)|<a;>q(||)
    End.
    Annotations
    @Axiom( x$1162 , x$1168 , x$1169 , x$1163 , x$1167 , x$1164 , x$1170 , x$1165 , x$1166 )
    Note

    unsound for hybrid games

  211. lazy val distributive: DerivedAxiomInfo

    Axiom "distributive".
       f()*(g()+h()) = f()*g() + f()*h()
    End.
    Annotations
    @Axiom( "*+" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  212. lazy val divGtEq: DerivedAxiomInfo
    Annotations
    @Axiom( "divGtEq" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  213. lazy val divGtGe: DerivedAxiomInfo
    Annotations
    @Axiom( "divGtGe" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  214. lazy val divGtGt: DerivedAxiomInfo
    Annotations
    @Axiom( "divGtGt" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  215. lazy val divGtLe: DerivedAxiomInfo
    Annotations
    @Axiom( "divGtLe" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  216. lazy val divGtLt: DerivedAxiomInfo
    Annotations
    @Axiom( "divGtLt" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  217. lazy val divGtNe: DerivedAxiomInfo
    Annotations
    @Axiom( "divGtNe" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  218. lazy val divLtEq: DerivedAxiomInfo
    Annotations
    @Axiom( "divLtEq" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  219. lazy val divLtGe: DerivedAxiomInfo
    Annotations
    @Axiom( "divLtGe" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  220. lazy val divLtGt: DerivedAxiomInfo
    Annotations
    @Axiom( "divLtGt" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  221. lazy val divLtLe: DerivedAxiomInfo
    Annotations
    @Axiom( "divLtLe" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  222. lazy val divLtLt: DerivedAxiomInfo
    Annotations
    @Axiom( "divLtLt" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  223. lazy val divLtNe: DerivedAxiomInfo
    Annotations
    @Axiom( "divLtNe" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  224. lazy val divNeEq: DerivedAxiomInfo
    Annotations
    @Axiom( "divNeEq" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  225. lazy val divNeNe: DerivedAxiomInfo
    Annotations
    @Axiom( "divNeNe" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  226. lazy val divideIdentity: DerivedAxiomInfo
    Annotations
    @Axiom( "divideIdentity" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  227. lazy val divideNeg: DerivedAxiomInfo
    Annotations
    @Axiom( "divideNeg" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  228. lazy val divideNumber: DerivedAxiomInfo
    Annotations
    @Axiom( "divideNumber" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  229. lazy val divideRat: DerivedAxiomInfo
    Annotations
    @Axiom( "divideRat" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  230. lazy val domainCommute: DerivedAxiomInfo

    Axiom "Domain Constraint Conjunction Reordering".
       [{c & (H(||) & q(||))}]p(||) <-> [{c & (q(||) & H(||))}]p(||)
    End.
    Annotations
    @Axiom( ("{∧}C","{&}C") , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  231. lazy val doubleNegation: DerivedAxiomInfo

    Axiom "!! double negation".
     (!(!p())) <-> p()
    End.
    Annotations
    @Axiom( x$622 , x$627 , x$628 , x$623 , x$626 , x$629 , x$630 , x$624 , x$625 )
  232. lazy val dualDirectb: DerivedAxiomInfo

    Axiom "[d] dual direct".
     [{a;}^@]p(||) <-> <a;>p(||)
    End.
    Annotations
    @Axiom( x$2458 , x$2464 , x$2465 , x$2459 , x$2463 , x$2460 , x$2466 , x$2461 , x$2462 )
  233. lazy val dualDirectd: DerivedAxiomInfo

    Axiom " dual direct".
     <{a;}^@>p(||) <-> [a;]p(||)
    End.
    Annotations
    @Axiom( x$2467 , x$2472 , x$2473 , x$2468 , x$2471 , x$2474 , x$2475 , x$2469 , x$2470 )
  234. lazy val dualIVT: DerivedAxiomInfo

    Dual version of initial-value theorem.

    Dual version of initial-value theorem.

    Annotations
    @Axiom( x$2359 , x$2362 , x$2363 , x$2364 , x$2361 , x$2365 , x$2366 , x$2360 , x$2367 )
  235. lazy val dualb: DerivedAxiomInfo

    Axiom "[d] dual".
     [{a;}^@]p(||) <-> ![a;]!p(||)
    End.
    Annotations
    @Axiom( x$2440 , x$2446 , x$2447 , x$2441 , x$2445 , x$2442 , x$2448 , x$2443 , x$2444 )
  236. val duald: CoreAxiomInfo
  237. lazy val emptySprout: DerivedAxiomInfo
    Annotations
    @Axiom( "emptySprout" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  238. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  239. lazy val eqAddIff: DerivedAxiomInfo
    Annotations
    @Axiom( "eqAddIff" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  240. lazy val eqNormalize: DerivedAxiomInfo

    Polynomial Arithmetic edu.cmu.cs.ls.keymaerax.btactics.PolynomialArithV2

    Annotations
    @Axiom( x$2395 , x$2398 , x$2399 , x$2400 , x$2401 , x$2402 , x$2403 , x$2396 , x$2397 )
  241. lazy val equal2And: DerivedAxiomInfo

    Axiom "!= to or".
      (f() = g()) <-> f() <= g() & f() >= g()
    End.
    Annotations
    @Axiom( x$1783 , x$1787 , x$1788 , x$1784 , x$1785 , x$1786 , x$1789 , x$1790 , x$1791 )
  242. lazy val equalCommute: DerivedAxiomInfo

    Axiom "= commute".
      (f()=g()) <-> (g()=f())
    End.
    Annotations
    @Axiom( x$847 , x$852 , x$853 , x$848 , x$851 , x$854 , x$855 , x$849 , x$850 )
  243. lazy val equalExpand: DerivedAxiomInfo

    Axiom "= expand".
      f_()=g_() <-> f_()<=g_()&g_()<=f_()
    End.
    Annotations
    @Axiom( "equalExpand" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  244. lazy val equalRefl: DerivedAxiomInfo

    Annotations
    @Axiom( x$3025 , x$3029 , x$3030 , x$3031 , x$3026 , x$3032 , x$3033 , x$3027 , x$3028 )
    See also

    equivReflexive

  245. lazy val equalReflexive: DerivedAxiomInfo

    Axiom "= reflexive".
       s() = s()
    End.
    Annotations
    @Axiom( x$838 , x$842 , x$843 , x$839 , x$840 , x$844 , x$845 , x$841 , x$846 )
    See also

    equivReflexive

  246. lazy val equalSym: DerivedAxiomInfo
    Annotations
    @Axiom( "equalSym" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  247. lazy val equalityBySubtraction: DerivedAxiomInfo
    Annotations
    @Axiom( "equalityBySubtraction" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  248. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  249. lazy val equivExpand: DerivedAxiomInfo

    Convert <-> to two implications: (p_() <-> q_()) <-> (p_()->q_())&(q_()->p_())

    Convert <-> to two implications: (p_() <-> q_()) <-> (p_()->q_())&(q_()->p_())

    Annotations
    @Axiom( x$811 , x$813 , x$814 , x$815 , x$812 , x$816 , x$817 , x$818 , x$819 )
  250. lazy val equivExpandAnd: DerivedAxiomInfo

    Convert <-> to two conjunctions: (p_() <-> q_()) <-> (p_()&q_())|(!p_()&!q_())

    Convert <-> to two conjunctions: (p_() <-> q_()) <-> (p_()&q_())|(!p_()&!q_())

    Annotations
    @Axiom( x$919 , x$921 , x$922 , x$923 , x$920 , x$924 , x$925 , x$926 , x$927 )
  251. lazy val equivReflexive: DerivedAxiomInfo

    Axiom "<-> reflexive".
     p() <-> p()
    End.
    Annotations
    @Axiom( x$910 , x$915 , x$916 , x$911 , x$914 , x$917 , x$918 , x$912 , x$913 )
    See also

    equalReflexive

  252. lazy val equivStutter: DerivedAxiomInfo

    Axiom "equiv stutter".
       (P<->Q) <-> (P<->Q)
    End.
    Annotations
    @Axiom( x$3115 , x$3119 , x$3120 , x$3121 , x$3122 , x$3118 , x$3123 , x$3116 , x$3117 )
    Note

    Trivial reflexive stutter axiom, only used with a different recursor pattern in AxiomIndex.

  253. lazy val equivTrue: DerivedAxiomInfo

    Axiom "<-> true".
       (p() <-> true) <-> p()
    End.
    Annotations
    @Axiom( x$1666 , x$1670 , x$1671 , x$1672 , x$1669 , x$1673 , x$1674 , x$1667 , x$1668 )
  254. lazy val existsAnd: DerivedAxiomInfo

    Axiom "\\exists& exists and".
     \exists x_ (q_(||) & p_(||)) -> \exists x_ (p_(||))
    End.
    Annotations
    @Axiom( "∃∧" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  255. lazy val existsDistElim: DerivedAxiomInfo

    Axiom "exists distribute elim".
      (\forall x (P->Q)) -> ((\exists x P)->(\exists x Q))
    Annotations
    @Axiom( x$1036 , x$1040 , x$1041 , x$1037 , x$1042 , x$1043 , x$1044 , x$1038 , x$1039 )
  256. lazy val existsDual: DerivedAxiomInfo

    Axiom "exists dual".
      (!\forall x (!p(||))) <-> (\exists x p(||))
    End.
    Annotations
    @Axiom( x$946 , x$952 , x$953 , x$947 , x$951 , x$948 , x$954 , x$949 , x$950 )
  257. lazy val existsDualy: DerivedAxiomInfo
    Annotations
    @Axiom( x$982 , x$984 , x$985 , x$986 , x$987 , x$983 , x$988 , x$989 , x$990 )
  258. lazy val existsGeneralize: DerivedAxiomInfo

    Axiom "exists generalize".
       p(t()) -> (\exists x p(x))
    End.
    Annotations
    @Axiom( ("∃G","existsG") , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  259. lazy val existsGeneralizey: DerivedAxiomInfo
    Annotations
    @Axiom( x$1549 , x$1551 , x$1552 , x$1553 , x$1554 , x$1550 , x$1555 , x$1556 , x$1557 )
  260. lazy val existsOr: DerivedAxiomInfo

    Axiom "\\exists& exists or"
     (\exists x_ (p_(x_) |  q_(x_))) <-> (\exists x_ p_(x_) | \exists x_ q_(x_))
    End.
    Annotations
    @Axiom( "∃∨" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  261. lazy val existsPDual: DerivedAxiomInfo
    Annotations
    @Axiom( x$964 , x$967 , x$968 , x$969 , x$970 , x$971 , x$972 , x$965 , x$966 )
  262. lazy val existsStutter: DerivedAxiomInfo

    Axiom "exists stutter".
       \exists x P <-> \exists x P
    End.
    Annotations
    @Axiom( x$3070 , x$3074 , x$3075 , x$3076 , x$3077 , x$3073 , x$3078 , x$3071 , x$3072 )
    Note

    Trivial reflexive stutter axiom, only used with a different recursor pattern in AxiomIndex.

  263. lazy val existsStutterPrime: DerivedAxiomInfo
    Annotations
    @Axiom( x$3079 , x$3083 , x$3084 , x$3085 , x$3086 , x$3082 , x$3087 , x$3080 , x$3081 )
  264. lazy val existsV: DerivedAxiomInfo

    Axiom "vacuous exists quantifier".
       (\exists x p()) <-> p()
    End.
    Annotations
    @Axiom( x$1585 , x$1589 , x$1590 , x$1586 , x$1591 , x$1592 , x$1593 , x$1587 , x$1588 )
  265. lazy val existse: DerivedAxiomInfo

    Axiom "exists eliminate".
       p(||) -> (\exists x p(||))
    End.
    Annotations
    @Axiom( x$1558 , x$1563 , x$1564 , x$1559 , x$1562 , x$1565 , x$1566 , x$1560 , x$1561 )
  266. lazy val existsey: DerivedAxiomInfo

    Axiom "exists eliminate y"
       p(||) -> \exists y_ p(||)
    End.
    Annotations
    @Axiom( x$1567 , x$1569 , x$1570 , x$1571 , x$1572 , x$1568 , x$1573 , x$1574 , x$1575 )
  267. lazy val factorAndLeft: ProvableSig
  268. lazy val factorAndRight: ProvableSig
  269. lazy val factorImpliesOrLeft: ProvableSig
  270. lazy val factorImpliesOrRight: ProvableSig
  271. lazy val factorOrLeft: ProvableSig
  272. lazy val factorOrRight: ProvableSig
  273. lazy val falseAnd: DerivedAxiomInfo

    Axiom "false&".
       (false&p()) <-> false
    End.
    Annotations
    @Axiom( x$1909 , x$1912 , x$1913 , x$1910 , x$1911 , x$1914 , x$1915 , x$1916 , x$1917 )
  274. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  275. lazy val flipGreater: DerivedAxiomInfo

    Axiom "> flip".
      (f() > g()) <-> (g() < f())
    End.
    Annotations
    @Axiom( x$2575 , x$2579 , x$2580 , x$2581 , x$2576 , x$2582 , x$2583 , x$2577 , x$2578 )
  276. lazy val flipGreaterEqual: DerivedAxiomInfo

    Axiom ">= flip".
      (f() >= g()) <-> (g() <= f())
    End.
    Annotations
    @Axiom( x$2215 , x$2219 , x$2220 , x$2221 , x$2216 , x$2222 , x$2223 , x$2217 , x$2218 )
  277. lazy val flipLess: DerivedAxiomInfo

    Axiom "< flip".
      (f() < g()) <-> (g() > f())
    End.
    Annotations
    @Axiom( x$1756 , x$1758 , x$1759 , x$1760 , x$1757 , x$1761 , x$1762 , x$1763 , x$1764 )
  278. lazy val flipLessEqual: DerivedAxiomInfo

    Axiom "<= flip".
      (f() <= g()) <-> (g() >= f())
    End.
    Annotations
    @Axiom( x$1729 , x$1731 , x$1732 , x$1733 , x$1730 , x$1734 , x$1735 , x$1736 , x$1737 )
  279. lazy val foldAndLessEqExistsLemma: DerivedAxiomInfo
    Annotations
    @Axiom( "foldAndLessEqExistsLemma" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  280. lazy val forallImplies: DerivedAxiomInfo

    Axiom "\\forall-> forall implies".
     \forall x_ p_(||) -> \forall x_ (q_(||) -> p_(||))
    End.
    Annotations
    @Axiom( "∀→" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  281. lazy val forallThenExists: DerivedAxiomInfo

    Axiom "\forall->\exists".
       (\forall x p(x)) -> (\exists x p(x))
    End.
    Annotations
    @Axiom( x$1855 , x$1857 , x$1858 , x$1859 , x$1860 , x$1856 , x$1861 , x$1862 , x$1863 )
    See also

    allThenExists

  282. lazy val geNeg: DerivedAxiomInfo

    Axiom ">= neg".
      f_()>=g_() <-> -f_()<=-g_()
    End.
    Annotations
    @Axiom( "geNeg" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  283. lazy val geNormalize: DerivedAxiomInfo
    Annotations
    @Axiom( x$2368 , x$2371 , x$2372 , x$2373 , x$2374 , x$2375 , x$2376 , x$2369 , x$2370 )
  284. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  285. lazy val greater: DerivedAxiomInfo

    Axiom ">".
       f() > g() <-> g() < f()
    End.
    Annotations
    @Axiom( x$2647 , x$2649 , x$2650 , x$2651 , x$2648 , x$2652 , x$2653 , x$2654 , x$2655 )
  286. lazy val greaterEqual: DerivedAxiomInfo

    Axiom ">=".
      (f()>=g()) <-> ((f()>g()) | (f()=g()))
    End.
    Annotations
    @Axiom( x$2242 , x$2244 , x$2245 , x$2246 , x$2243 , x$2247 , x$2248 , x$2249 , x$2250 )
  287. lazy val greaterEqualRefl: DerivedAxiomInfo
    Annotations
    @Axiom( x$3043 , x$3047 , x$3048 , x$3049 , x$3044 , x$3050 , x$3051 , x$3045 , x$3046 )
  288. lazy val greaterEqualReflexive: DerivedAxiomInfo

    Axiom ">= reflexive".
       s() >= s()
    End.
    Annotations
    @Axiom( x$2557 , x$2561 , x$2562 , x$2563 , x$2558 , x$2564 , x$2565 , x$2559 , x$2560 )
  289. lazy val greaterEqualTotal: DerivedAxiomInfo
    Annotations
    @Axiom( "greaterEqualTotal" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  290. lazy val greaterImpliesNotEqual: DerivedAxiomInfo

    Axiom ">2!=".
      f()>g() -> f()!=g()
    End.
    Annotations
    @Axiom( ">2!=" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  291. lazy val greaterMonotone: DerivedAxiomInfo

    Axiom "> monotone".
      f()+h()>g() <- f()>g() & h()>=0
    End.
    Annotations
    @Axiom( ">mon" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  292. lazy val greaterNotRefl: DerivedAxiomInfo
    Annotations
    @Axiom( x$3007 , x$3011 , x$3012 , x$3013 , x$3008 , x$3014 , x$3015 , x$3009 , x$3010 )
  293. lazy val greaterNotSym: DerivedAxiomInfo
    Annotations
    @Axiom( "greaterNotSym" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  294. lazy val gtNeg: DerivedAxiomInfo

    Axiom "> neg".
      f_()>g_() <-> -f_() < -g_()
    End.
    Annotations
    @Axiom( "gtNeg" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  295. lazy val gtNormalize: DerivedAxiomInfo
    Annotations
    @Axiom( x$3151 , x$3154 , x$3155 , x$3156 , x$3157 , x$3158 , x$3159 , x$3152 , x$3153 )
  296. lazy val gtzImpNez: DerivedAxiomInfo
    Annotations
    @Axiom( "gtzImpNez" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  297. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  298. lazy val identityTimes: DerivedAxiomInfo

    Axiom "identity *".
       1*f() = f()
    End.
    Annotations
    @Axiom( "I*" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  299. lazy val impliesMonAndLeft: ProvableSig
  300. lazy val impliesMonAndRight: ProvableSig
  301. lazy val impliesRightAnd: ProvableSig
  302. lazy val implyDistAnd: DerivedAxiomInfo

    Axiom "-> distributes over &".
     (p() -> (q()&r())) <-> ((p()->q()) & (p()->r()))
    End.
    Annotations
    @Axiom( ("→∧", "->&") , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  303. lazy val implyDistEquiv: DerivedAxiomInfo

    Axiom "-> distributes over <->".
     (p() -> (q()<->r())) <-> ((p()->q()) <-> (p()->r()))
    End.
    Annotations
    @Axiom( ("→↔","-><->") , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  304. lazy val implyExpand: DerivedAxiomInfo

    Axiom "-> expand".
       (p() -> q()) <-> ((!p()) | q())
    End.
    Annotations
    @Axiom( x$1198 , x$1202 , x$1203 , x$1204 , x$1199 , x$1205 , x$1206 , x$1200 , x$1201 )
  305. lazy val implySelf: DerivedAxiomInfo

    Axiom "-> self".
       (p() -> p()) <-> true
    End.
    Annotations
    @Axiom( x$1153 , x$1156 , x$1157 , x$1158 , x$1159 , x$1160 , x$1161 , x$1154 , x$1155 )
  306. lazy val implyStutter: DerivedAxiomInfo

    Axiom "imply stutter".
       (P->Q) <-> (P->Q)
    End.
    Annotations
    @Axiom( x$3106 , x$3110 , x$3111 , x$3112 , x$3113 , x$3109 , x$3114 , x$3107 , x$3108 )
    Note

    Trivial reflexive stutter axiom, only used with a different recursor pattern in AxiomIndex.

  307. lazy val implyTautology: DerivedAxiomInfo

    Axiom "-> tautology".
       (p() -> (q() -> p()&q())) <-> true
    End.
    Annotations
    @Axiom( x$1090 , x$1092 , x$1093 , x$1094 , x$1091 , x$1095 , x$1096 , x$1097 , x$1098 )
  308. lazy val implyTrue: DerivedAxiomInfo

    Axiom "->true".
       (p()->true) <-> true
    End.
    Annotations
    @Axiom( x$1864 , x$1867 , x$1868 , x$1865 , x$1866 , x$1869 , x$1870 , x$1871 , x$1872 )
  309. lazy val implyWeaken: DerivedAxiomInfo

    Axiom "-> weaken".
     (p() -> q()) -> (p()&c() -> q())
    End.
    Annotations
    @Axiom( ("→W","->W") , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  310. lazy val indrule: DerivedRuleInfo

    Rule "ind induction".

    Rule "ind induction". Premise p(||) ==> [a;]p(||) Conclusion p(||) ==> [a*]p(||)

      p(x) |- [a]p(x)
    --------------------- ind
      p(x) |- [{a}*]p(x)

    Interderives with FP fixpoint rule.

    Annotations
    @ProofRule( x$633 , x$634 , x$635 , x$632 , x$631 , x$636 , x$637 , x$638 , x$639 )
    See also

    Lemma 4.1 of Andre Platzer. Differential game logic. ACM Trans. Comput. Log. 17(1), 2015. arXiv 1408.1980

    Lemma 7.2 and Corollary 16.1 of Andre Platzer. Logical Foundations of Cyber-Physical Systems. Springer, 2018.

  311. lazy val intervalDown1Divide: DerivedAxiomInfo

    Axiom "<=1Div down".
       h()<=1/f() <- ((f()<=F() & F()*f()>0) & (h()<=1/F()))
    End.
    Annotations
    @Axiom( "<=1/" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  312. lazy val intervalDownAbs: DerivedAxiomInfo

    Axiom "<=abs down".
       h()<=abs(f()) <- ((ff()<=f() & f() <= F()) & (h()<=ff() | h()<=-F()))
    End.
    Annotations
    @Axiom( x$2818 , x$2821 , x$2822 , x$2823 , x$2824 , x$2825 , x$2826 , x$2819 , x$2820 )
  313. lazy val intervalDownMax: DerivedAxiomInfo

    Axiom "<=max down".
       h()<=max(f(),g()) <- ((ff()<=f() & gg()<=g()) & (ff()<=h() | gg()<=h()))
    End.
    Annotations
    @Axiom( x$2827 , x$2830 , x$2831 , x$2832 , x$2833 , x$2834 , x$2835 , x$2828 , x$2829 )
  314. lazy val intervalDownMin: DerivedAxiomInfo

    Axiom "<=min down".
       h()<=min(f(),g()) <- ((ff()<=f() & gg()<=g()) & (h()<=ff() & h()<=gg()))
    End.
    Annotations
    @Axiom( x$2836 , x$2839 , x$2840 , x$2841 , x$2842 , x$2843 , x$2844 , x$2837 , x$2838 )
  315. lazy val intervalDownMinus: DerivedAxiomInfo

    Axiom "<=- down".
       h()<=f()-g() <- ((ff()<=f() & g()<=G()) & h()<=ff()-G())
    End.
    Annotations
    @Axiom( x$2854 , x$2857 , x$2858 , x$2859 , x$2860 , x$2861 , x$2862 , x$2855 , x$2856 )
  316. lazy val intervalDownNeg: DerivedAxiomInfo

    Axiom "<=neg down".
       h<=-f() <- (f()<=F() & h() <= -F())
    End.
    Annotations
    @Axiom( x$2809 , x$2812 , x$2813 , x$2814 , x$2815 , x$2816 , x$2817 , x$2810 , x$2811 )
  317. lazy val intervalDownPlus: DerivedAxiomInfo

    Axiom "<=+ down".
       h()<=f()+g() <- ((ff()<=f() & gg()<=g()) & h()<=ff()+gg())
    End.
    Annotations
    @Axiom( x$2845 , x$2848 , x$2849 , x$2850 , x$2851 , x$2852 , x$2853 , x$2846 , x$2847 )
  318. lazy val intervalDownPower: DerivedAxiomInfo

    Axiom "<=pow down".
       h()<=f()^2 <- ((ff()<=f() & f()<=F()) & ((0<= ff_() & h()<=ff()^2) | (F_() <0 & h()<=F()^2)))
    End.
    Annotations
    @Axiom( x$2872 , x$2875 , x$2876 , x$2877 , x$2878 , x$2879 , x$2880 , x$2873 , x$2874 )
  319. lazy val intervalDownTimes: DerivedAxiomInfo

    Axiom "<=* down".
       h()<=f()*g()<- (((ff()<=f() & f()<=F()) & (gg()<=g() & g()<=G())) & (h()<=ff()*gg() & h()<=ff()*G() & h()<=F()*gg() & h()<=F()*G()))
    End.
    Annotations
    @Axiom( x$2863 , x$2866 , x$2867 , x$2868 , x$2869 , x$2870 , x$2871 , x$2864 , x$2865 )
  320. lazy val intervalLBoth: DerivedAxiomInfo

    Axiom "< both".
       f()<g() <- ((f() <= F() & gg() <= g()) & F() < gg())
    End.
    Annotations
    @Axiom( x$2728 , x$2731 , x$2732 , x$2733 , x$2734 , x$2735 , x$2736 , x$2729 , x$2730 )
  321. lazy val intervalLEBoth: DerivedAxiomInfo

    Axiom "<= both".
       f()<=g() <- ((f() <= F() & gg() <= g()) & F() <= gg())
    End.
    Annotations
    @Axiom( x$2719 , x$2722 , x$2723 , x$2724 , x$2725 , x$2726 , x$2727 , x$2720 , x$2721 )
  322. lazy val intervalUp1Divide: DerivedAxiomInfo

    Axiom "1Div<= up".
       1/f()<=h() <- ((ff()<=f() & ff()*f()>0) & (1/ff()<=h()))
    End.
    Annotations
    @Axiom( "1/<=" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  323. lazy val intervalUpAbs: DerivedAxiomInfo

    Axiom "abs<= up".
       abs(f())<=h() <- ((ff()<=f() & f() <= F()) & (-ff()<=h() & F()<=h()))
    End.
    Annotations
    @Axiom( x$2746 , x$2749 , x$2750 , x$2751 , x$2752 , x$2753 , x$2754 , x$2747 , x$2748 )
  324. lazy val intervalUpMax: DerivedAxiomInfo

    Axiom "max<= up".
       max(f(),g())<=h() <- ((f()<=F() & g()<=G()) & (F() <= h() & G()<=h()))
    End.
    Annotations
    @Axiom( x$2755 , x$2758 , x$2759 , x$2760 , x$2761 , x$2762 , x$2763 , x$2756 , x$2757 )
  325. lazy val intervalUpMin: DerivedAxiomInfo

    Axiom "min<= up".
       min(f(),g())<=h() <- ((f()<=F() & g()<=G()) & (F()<=h() | G()<=h()))
    End.
    Annotations
    @Axiom( x$2764 , x$2767 , x$2768 , x$2769 , x$2770 , x$2771 , x$2772 , x$2765 , x$2766 )
  326. lazy val intervalUpMinus: DerivedAxiomInfo

    Axiom "-<= up".
       f()-g()<=h() <- ((f()<=F() & gg()<=g()) & F()-gg()<=h())
    End.
    Annotations
    @Axiom( x$2782 , x$2785 , x$2786 , x$2787 , x$2788 , x$2789 , x$2790 , x$2783 , x$2784 )
  327. lazy val intervalUpNeg: DerivedAxiomInfo

    Axiom "neg<= up".
       -f()<=h() <- (ff()<=f() & -ff() <= h())
    End.
    Annotations
    @Axiom( x$2737 , x$2740 , x$2741 , x$2742 , x$2743 , x$2744 , x$2745 , x$2738 , x$2739 )
  328. lazy val intervalUpPlus: DerivedAxiomInfo

    Axiom "+<= up".
       f()+g()<=h() <- ((f()<=F() & g()<=G()) & F()+G()<=h())
    End.
    Annotations
    @Axiom( x$2773 , x$2776 , x$2777 , x$2778 , x$2779 , x$2780 , x$2781 , x$2774 , x$2775 )
  329. lazy val intervalUpPower: DerivedAxiomInfo

    Axiom "pow<= up".
       f()^2<=h() <- ((ff()<=f() & f()<=F()) & (ff()^2<=h() & F()^2<=h()))
    End.
    Annotations
    @Axiom( x$2800 , x$2803 , x$2804 , x$2805 , x$2806 , x$2807 , x$2808 , x$2801 , x$2802 )
  330. lazy val intervalUpTimes: DerivedAxiomInfo

    Axiom "*<= up".
       f()*g()<=h() <- ((ff()<=f() & f()<=F() & gg()<=g() & g()<=G()) & (ff()*gg()<=h() & ff()*G()<=h() & F()*gg()<=h() & F()*G()<=h()))
    End.
    Annotations
    @Axiom( x$2791 , x$2794 , x$2795 , x$2796 , x$2797 , x$2798 , x$2799 , x$2792 , x$2793 )
  331. lazy val invtestd: DerivedAxiomInfo
    Annotations
    @Axiom( x$1369 , x$1373 , x$1374 , x$1375 , x$1372 , x$1376 , x$1377 , x$1370 , x$1371 )
  332. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  333. val iterateb: CoreAxiomInfo
  334. lazy val iterated: DerivedAxiomInfo

    Axiom "<*> iterate".
       <{a;}*>p(||) <-> (p(||) | <a;><{a;}*> p(||))
    End.
    Annotations
    @Axiom( x$1423 , x$1429 , x$1430 , x$1424 , x$1428 , x$1425 , x$1431 , x$1426 , x$1427 )
  335. lazy val iterateiterateb: DerivedAxiomInfo

    Axiom "[**] iterate iterate".
       [{a;}*;{a;}*]p(||) <-> [{a;}*]p(||)
    End.
    Annotations
    @Axiom( x$1495 , x$1500 , x$1501 , x$1496 , x$1499 , x$1502 , x$1503 , x$1497 , x$1498 )
    See also

    Lemma 7.6 of textbook

  336. lazy val iterateiterated: DerivedAxiomInfo

    Axiom "<**> iterate iterate".
       <{a;}*;{a;}*>p(||) <-> <{a;}*>p(||)
    End.
    Annotations
    @Axiom( x$1504 , x$1509 , x$1510 , x$1505 , x$1508 , x$1511 , x$1512 , x$1506 , x$1507 )
  337. lazy val leApprox: DerivedAxiomInfo

    Axiom "<= to <".
      f_()<=0 <- f_()<0
    End.
    Annotations
    @Axiom( x$2881 , x$2885 , x$2886 , x$2887 , x$2882 , x$2888 , x$2889 , x$2883 , x$2884 )
  338. lazy val leMaxNorm: DerivedAxiomInfo
    Annotations
    @Axiom( "leMaxNorm" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  339. lazy val leTimesMonoLemma: DerivedAxiomInfo
    Annotations
    @Axiom( "leTimesMonoLemma" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  340. lazy val leaveWithinClosed: DerivedAxiomInfo

    Axiom "leave within closed <=".
       (<{c&q}>p<=0 <-> <{c&q&p>=0}>p=0) <- p>=0
    End.
    Annotations
    @Axiom( x$2206 , x$2209 , x$2210 , x$2211 , x$2212 , x$2213 , x$2214 , x$2207 , x$2208 )
  341. lazy val less: DerivedAxiomInfo

    Axiom "<".
       f() < g() <-> 0 < g()-f()
    End.
    Annotations
    @Axiom( x$2638 , x$2640 , x$2641 , x$2642 , x$2639 , x$2643 , x$2644 , x$2645 , x$2646 )
  342. lazy val lessEqual: DerivedAxiomInfo

    Axiom "<=".
      (f()<=g()) <-> ((f()<g()) | (f()=g()))
    End.
    Annotations
    @Axiom( x$2251 , x$2253 , x$2254 , x$2255 , x$2252 , x$2256 , x$2257 , x$2258 , x$2259 )
  343. lazy val lessEqualRefl: DerivedAxiomInfo
    Annotations
    @Axiom( x$3034 , x$3038 , x$3039 , x$3040 , x$3035 , x$3041 , x$3042 , x$3036 , x$3037 )
  344. lazy val lessEqualTotal: DerivedAxiomInfo
    Annotations
    @Axiom( "lessEqualTotal" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  345. lazy val lessNotRefl: DerivedAxiomInfo
    Annotations
    @Axiom( x$2998 , x$3002 , x$3003 , x$3004 , x$2999 , x$3005 , x$3006 , x$3000 , x$3001 )
  346. lazy val lessNotSym: DerivedAxiomInfo
    Annotations
    @Axiom( "lessNotSym" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  347. lazy val logger: Logger
    Attributes
    protected
    Definition Classes
    LazyLogging → LoggerHolder
  348. final val loggerName: String
    Attributes
    protected
    Definition Classes
    LoggerHolder
  349. lazy val loopApproxb: DerivedAxiomInfo

    Axiom "[*] approx".
       [{a;}*]p(||) -> [a;]p(||)
    End.
    Annotations
    @Axiom( x$1450 , x$1455 , x$1456 , x$1451 , x$1454 , x$1457 , x$1458 , x$1452 , x$1453 )
  350. lazy val loopApproxd: DerivedAxiomInfo

    Axiom "<*> approx".
       <a;>p(||) -> <{a;}*>p(||)
    End.
    Annotations
    @Axiom( x$1441 , x$1446 , x$1447 , x$1442 , x$1445 , x$1448 , x$1449 , x$1443 , x$1444 )
  351. lazy val loopMergeb: DerivedAxiomInfo

    Axiom "[*] merge".
       [{a;}*][{a;}*]p(||) <-> [{a;}*]p(||)
    End.
    Annotations
    @Axiom( x$1477 , x$1482 , x$1483 , x$1478 , x$1484 , x$1479 , x$1485 , x$1480 , x$1481 )
  352. lazy val loopMerged: DerivedAxiomInfo

    Axiom "<*> merge".
       <{a;}*><{a;}*>p(||) <-> <{a;}*>p(||)
    End.
    Annotations
    @Axiom( x$1486 , x$1491 , x$1492 , x$1487 , x$1493 , x$1488 , x$1494 , x$1489 , x$1490 )
  353. lazy val loopStuck: DerivedAxiomInfo

    Axiom "<*> stuck".
       <{a;}*>p(||) <-> <{a;}*>p(||)
    End.
    Annotations
    @Axiom( x$2674 , x$2677 , x$2678 , x$2679 , x$2680 , x$2681 , x$2682 , x$2675 , x$2676 )
    Note

    Trivial reflexive stutter axiom, only used with a different recursor pattern in AxiomIndex.

  354. lazy val ltzImpNez: DerivedAxiomInfo
    Annotations
    @Axiom( "ltzImpNez" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  355. lazy val max: DerivedAxiomInfo

    Axiom "max".
       (max(f(), g()) = h()) <-> ((f()>=g() & h()=f()) | (f()<g() & h()=g()))
    End.
    Annotations
    @Axiom( "max" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  356. lazy val metricAndLe: DerivedAxiomInfo

    Axiom "metric <= & <=".
      f_()<=0 & g_()<=0 <-> max(f_(), g_())<=0
    End.
    Annotations
    @Axiom( x$2899 , x$2902 , x$2903 , x$2904 , x$2905 , x$2906 , x$2907 , x$2900 , x$2901 )
  357. lazy val metricAndLt: DerivedAxiomInfo

    Axiom "metric < & <".
      f_()<0 & g_()<0 <-> max(f_(), g_())<0
    End.
    Annotations
    @Axiom( x$2908 , x$2911 , x$2912 , x$2913 , x$2914 , x$2915 , x$2916 , x$2909 , x$2910 )
  358. lazy val metricLe: DerivedAxiomInfo

    Axiom "metric <=".
      f_()<=g_() <-> f_()-g_()<=0
    End.
    Annotations
    @Axiom( x$2386 , x$2389 , x$2390 , x$2391 , x$2392 , x$2393 , x$2394 , x$2387 , x$2388 )
  359. lazy val metricLt: DerivedAxiomInfo

    Axiom "metric <".
      f_()<g_() <-> f_()-g_()<0
    End.
    Annotations
    @Axiom( x$2890 , x$2893 , x$2894 , x$2895 , x$2896 , x$2897 , x$2898 , x$2891 , x$2892 )
  360. lazy val metricOrLe: DerivedAxiomInfo

    Axiom "metric <= | <=".
      f_()<=0 | g_()<=0 <-> min(f_(), g_())<=0
    End.
    Annotations
    @Axiom( x$2917 , x$2920 , x$2921 , x$2922 , x$2923 , x$2924 , x$2925 , x$2918 , x$2919 )
  361. lazy val metricOrLt: DerivedAxiomInfo

    Axiom "metric < | <".
      f_()<0 | g_()<0 <-> min(f_(), g_())<0
    End.
    Annotations
    @Axiom( x$2926 , x$2929 , x$2930 , x$2931 , x$2932 , x$2933 , x$2934 , x$2927 , x$2928 )
  362. lazy val min: DerivedAxiomInfo

    Axiom "min".
       (min(f(), g()) = h()) <-> ((f()<=g() & h()=f()) | (f()>g() & h()=g()))
    End.
    Annotations
    @Axiom( "min" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  363. lazy val minGeNorm: DerivedAxiomInfo
    Annotations
    @Axiom( "minGeNorm" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  364. lazy val minGtNorm: DerivedAxiomInfo
    Annotations
    @Axiom( "minGtNorm" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  365. lazy val minLeNorm: DerivedAxiomInfo
    Annotations
    @Axiom( "minLeNorm" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  366. lazy val minusBranch2: DerivedAxiomInfo
    Annotations
    @Axiom( "minusBranch2" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  367. lazy val minusBranch3: DerivedAxiomInfo
    Annotations
    @Axiom( "minusBranch3" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  368. lazy val minusEmpty: DerivedAxiomInfo
    Annotations
    @Axiom( "minusEmpty" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  369. lazy val minusNeg: DerivedAxiomInfo

    Axiom "minus neg".
       -(f()-g()) = g()-f()
    End.
    Annotations
    @Axiom( x$2944 , x$2948 , x$2949 , x$2950 , x$2945 , x$2951 , x$2952 , x$2946 , x$2947 )
  370. lazy val minusZero: DerivedAxiomInfo

    Axiom "-0".
       (f()-0) = f()
    End.
    Annotations
    @Axiom( x$2962 , x$2966 , x$2967 , x$2968 , x$2963 , x$2969 , x$2970 , x$2964 , x$2965 )
  371. lazy val monTimesBranch2: DerivedAxiomInfo
    Annotations
    @Axiom( "monTimesBranch2" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  372. lazy val monTimesBranch3: DerivedAxiomInfo
    Annotations
    @Axiom( "monTimesBranch3" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  373. lazy val monTimesZero: DerivedAxiomInfo
    Annotations
    @Axiom( "monTimesZero" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  374. lazy val monallrule: DerivedRuleInfo

    Rule "all generalization".

    Rule "all generalization". Premise p(||) |- q(||) Conclusion \forall x p(||) |- \forall x q(||) End.

    Annotations
    @ProofRule( x$703 , x$706 , x$707 , x$704 , x$705 , x$708 , x$709 , x$710 , x$711 )
  375. lazy val monb2: DerivedRuleInfo

    Rule "[] monotone 2".

    Rule "[] monotone 2". Premise q(||) ==> p(||) Conclusion [a;]q(||) ==> [a;]p(||) End.

    Annotations
    @ProofRule( x$892 , x$895 , x$896 , x$894 , x$893 , x$897 , x$898 , x$899 , x$900 )
    Note

    Renamed form of boxMonotone.

    See also

    "André Platzer. Differential Game Logic. ACM Trans. Comput. Log. 2015"

    "André Platzer. Differential Hybrid Games."

  376. lazy val monbaxiom: DerivedRuleInfo

    Rule "[] monotone".

    Rule "[] monotone". Premise p(||) ==> q(||) Conclusion [a;]p(||) ==> [a;]q(||) End.

    Annotations
    @ProofRule( x$694 , x$697 , x$698 , x$696 , x$695 , x$699 , x$700 , x$701 , x$702 )
    Note

    Notation changed to p instead of p_ just for the sake of the derivation.

    See also

    "André Platzer. Differential Game Logic. ACM Trans. Comput. Log. 2015"

    "André Platzer. Differential Hybrid Games."

  377. val mondrule: AxiomaticRuleInfo
  378. lazy val monomialTimesLemma: DerivedAxiomInfo
    Annotations
    @Axiom( "monomialTimesLemma" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  379. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  380. lazy val neNormalize: DerivedAxiomInfo
    Annotations
    @Axiom( x$3142 , x$3145 , x$3146 , x$3147 , x$3148 , x$3149 , x$3150 , x$3143 , x$3144 )
  381. lazy val negNeg: DerivedAxiomInfo

    Axiom "neg neg".
       -(-f()) = f()
    End.
    Annotations
    @Axiom( x$2953 , x$2957 , x$2958 , x$2959 , x$2954 , x$2960 , x$2961 , x$2955 , x$2956 )
  382. lazy val negOneTimes: DerivedAxiomInfo

    Axiom "-1*".
       (-1*f()) = -f()
    End.
    Annotations
    @Axiom( x$1945 , x$1947 , x$1948 , x$1949 , x$1946 , x$1950 , x$1951 , x$1952 , x$1953 )
  383. lazy val negTimes: DerivedAxiomInfo
    Annotations
    @Axiom( "negTimes" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  384. lazy val negateBranch2: DerivedAxiomInfo
    Annotations
    @Axiom( "negateBranch2" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  385. lazy val negateBranch3: DerivedAxiomInfo
    Annotations
    @Axiom( "negateBranch3" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  386. lazy val negateEmpty: DerivedAxiomInfo
    Annotations
    @Axiom( "negateEmpty" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  387. lazy val nonnegativeSquares: DerivedAxiomInfo

    Axiom "nonnegative squares".
      f()^2>=0
    End.
    Annotations
    @Axiom( x$2665 , x$2667 , x$2668 , x$2669 , x$2666 , x$2670 , x$2671 , x$2672 , x$2673 )
  388. lazy val normalizeBranch2: DerivedAxiomInfo
    Annotations
    @Axiom( "normalizeBranch2" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  389. lazy val normalizeBranch3: DerivedAxiomInfo
    Annotations
    @Axiom( "normalizeBranch3" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  390. lazy val normalizeCoeff0: DerivedAxiomInfo
    Annotations
    @Axiom( "normalizeCoeff0" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  391. lazy val normalizeCoeff1: DerivedAxiomInfo
    Annotations
    @Axiom( "normalizeCoeff1" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  392. lazy val normalizeMonom0: DerivedAxiomInfo
    Annotations
    @Axiom( "normalizeMonom0" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  393. lazy val normalizeMonomCS: DerivedAxiomInfo
    Annotations
    @Axiom( "normalizeMonomCS" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  394. lazy val normalizeMonomNCS: DerivedAxiomInfo
    Annotations
    @Axiom( "normalizeMonomNCS" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  395. lazy val normalizePowers1R: DerivedAxiomInfo
    Annotations
    @Axiom( "normalizePowers1R" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  396. lazy val normalizePowers1V: DerivedAxiomInfo
    Annotations
    @Axiom( "normalizePowers1V" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  397. lazy val normalizePowersC1: DerivedAxiomInfo
    Annotations
    @Axiom( "normalizePowersC1" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  398. lazy val normalizePowersCP: DerivedAxiomInfo
    Annotations
    @Axiom( "normalizePowersCP" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  399. lazy val normalizePowersCV: DerivedAxiomInfo
    Annotations
    @Axiom( "normalizePowersCV" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  400. lazy val normalizePowersRP: DerivedAxiomInfo
    Annotations
    @Axiom( "normalizePowersRP" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  401. lazy val normalizePowersRV: DerivedAxiomInfo
    Annotations
    @Axiom( "normalizePowersRV" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  402. lazy val notAll: DerivedAxiomInfo

    Axiom "!all".
      (!\forall x (p(||))) <-> \exists x (!p(||))
    End.
    Annotations
    @Axiom( x$1000 , x$1004 , x$1005 , x$1001 , x$1006 , x$1007 , x$1008 , x$1002 , x$1003 )
  403. lazy val notAnd: DerivedAxiomInfo

    Axiom "!& deMorgan".
       (!(p() & q())) <-> ((!p()) | (!q()))
    End.
    Annotations
    @Axiom( x$1180 , x$1185 , x$1186 , x$1181 , x$1182 , x$1187 , x$1188 , x$1183 , x$1184 )
  404. lazy val notBox: DerivedAxiomInfo

    Axiom "![]".
      ![a;]P <-> <a;>!P
    End.
    Annotations
    @Axiom( x$1009 , x$1014 , x$1015 , x$1010 , x$1013 , x$1016 , x$1017 , x$1011 , x$1012 )
  405. lazy val notDiamond: DerivedAxiomInfo

    Axiom "!<>".
      !<a;>p(x) <-> [a;]!p(x)
    End.
    Annotations
    @Axiom( x$1018 , x$1023 , x$1024 , x$1019 , x$1022 , x$1025 , x$1026 , x$1020 , x$1021 )
  406. lazy val notEqual: DerivedAxiomInfo

    Axiom "! =".
      !(f() = g()) <-> f() != g()
    End.
    Annotations
    @Axiom( x$2566 , x$2569 , x$2570 , x$2567 , x$2568 , x$2571 , x$2572 , x$2573 , x$2574 )
  407. lazy val notEqual2Or: DerivedAxiomInfo

    Axiom "!= to or".
      (f() != g()) <-> f() < g() | f() > g()
    End.
    Annotations
    @Axiom( x$1819 , x$1823 , x$1824 , x$1820 , x$1821 , x$1822 , x$1825 , x$1826 , x$1827 )
  408. lazy val notEqualExpand: DerivedAxiomInfo

    Axiom "!= expand".
      f_()!=g_() <-> f_()<g_()|g_()<f_()
    End.
    Annotations
    @Axiom( "notEqualExpand" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  409. lazy val notEqualNotRefl: DerivedAxiomInfo
    Annotations
    @Axiom( x$3016 , x$3020 , x$3021 , x$3022 , x$3017 , x$3023 , x$3024 , x$3018 , x$3019 )
  410. lazy val notEqualSym: DerivedAxiomInfo
    Annotations
    @Axiom( "notEqualSym" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  411. lazy val notEquiv: DerivedAxiomInfo

    Axiom "!<-> deMorgan".
       (!(p() <-> q())) <-> (((p()) & (!q())) | ((!p()) & (q())))
    End.
    Annotations
    @Axiom( x$1684 , x$1689 , x$1690 , x$1685 , x$1686 , x$1691 , x$1692 , x$1687 , x$1688 )
  412. lazy val notExists: DerivedAxiomInfo

    Axiom "!exists".
      (!\exists x (p(||))) <-> \forall x (!p(||))
    End.
    Annotations
    @Axiom( x$991 , x$995 , x$996 , x$992 , x$997 , x$998 , x$999 , x$993 , x$994 )
  413. lazy val notGreater: DerivedAxiomInfo

    Axiom "! >".
      (!(f() > g())) <-> (f() <= g())
    End.
    Annotations
    @Axiom( x$2269 , x$2272 , x$2273 , x$2270 , x$2271 , x$2274 , x$2275 , x$2276 , x$2277 )
  414. lazy val notGreaterEqual: DerivedAxiomInfo

    Axiom "! >=".
      (!(f() >= g())) <-> (f() < g())
    End.
    Annotations
    @Axiom( x$2593 , x$2594 , x$2596 , x$2597 , x$2595 , x$2598 , x$2599 , x$2600 , x$2601 )
  415. lazy val notImply: DerivedAxiomInfo

    Axiom "!-> deMorgan".
       (!(p() -> q())) <-> ((p()) & (!q()))
    End.
    Annotations
    @Axiom( x$1675 , x$1680 , x$1681 , x$1676 , x$1677 , x$1682 , x$1683 , x$1678 , x$1679 )
  416. lazy val notLess: DerivedAxiomInfo

    Axiom "! <".
      (!(f() < g())) <-> (f() >= g())
    End.
    Annotations
    @Axiom( x$2584 , x$2587 , x$2588 , x$2585 , x$2586 , x$2589 , x$2590 , x$2591 , x$2592 )
  417. lazy val notLessEqual: DerivedAxiomInfo

    Axiom "! <=".
      (!(f() <= g())) <-> (f() > g())
    End.
    Annotations
    @Axiom( x$2404 , x$2407 , x$2408 , x$2405 , x$2406 , x$2409 , x$2410 , x$2411 , x$2412 )
  418. lazy val notNotEqual: DerivedAxiomInfo

    Axiom "! !=".
      (!(f() != g())) <-> (f() = g())
    End.
    Annotations
    @Axiom( x$2278 , x$2281 , x$2282 , x$2279 , x$2280 , x$2283 , x$2284 , x$2285 , x$2286 )
  419. lazy val notOr: DerivedAxiomInfo

    Axiom "!| deMorgan".
       (!(p() | q())) <-> ((!p()) & (!q()))
    End.
    Annotations
    @Axiom( x$1171 , x$1176 , x$1177 , x$1172 , x$1173 , x$1178 , x$1179 , x$1174 , x$1175 )
  420. lazy val notStutter: DerivedAxiomInfo

    Axiom "not stutter".
       !P <-> !P
    End.
    Annotations
    @Axiom( x$3124 , x$3128 , x$3129 , x$3130 , x$3131 , x$3127 , x$3132 , x$3125 , x$3126 )
    Note

    Trivial reflexive stutter axiom, only used with a different recursor pattern in AxiomIndex.

  421. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  422. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  423. lazy val odeStuck: DerivedAxiomInfo

    Axiom "<'> stuck".
       <{c&q(||)}>p(||) <-> <{c&q(||)}>p(||)
    End.
    Annotations
    @Axiom( x$2692 , x$2695 , x$2696 , x$2697 , x$2698 , x$2699 , x$2700 , x$2693 , x$2694 )
    Note

    Trivial reflexive stutter axiom, only used with a different recursor pattern in AxiomIndex.

  424. lazy val oneGeZero: DerivedAxiomInfo
    Annotations
    @Axiom( "oneGeZero" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  425. lazy val oneGreaterZero: DerivedAxiomInfo

    Axiom "1>0".
      1>0
    End.
    Annotations
    @Axiom( x$2656 , x$2658 , x$2659 , x$2660 , x$2657 , x$2661 , x$2662 , x$2663 , x$2664 )
  426. lazy val openInvariantClosure: DerivedAxiomInfo

    Axiom "open invariant closure >".
       ([{c&q}]p>0 <-> [{c&q&p>=0}]p>0) <- p>=0
    End.
    Annotations
    @Axiom( x$2260 , x$2263 , x$2264 , x$2265 , x$2266 , x$2267 , x$2268 , x$2261 , x$2262 )
  427. lazy val orAssoc: DerivedAxiomInfo

    Axiom "| associative".
       ((p() | q()) | r()) <-> (p() | (q() | r()))
    End.
    Annotations
    @Axiom( x$1648 , x$1652 , x$1653 , x$1654 , x$1651 , x$1655 , x$1656 , x$1649 , x$1650 )
  428. lazy val orCommute: DerivedAxiomInfo

    Axiom "| commute".
       (p() | q()) <-> (q() | p())
    End.
    Annotations
    @Axiom( x$1630 , x$1634 , x$1635 , x$1636 , x$1633 , x$1637 , x$1638 , x$1631 , x$1632 )
  429. lazy val orDistAnd: DerivedAxiomInfo

    Axiom "| distributes over &".
     (p() & (q() | r())) <-> ((p() & q()) | (p() & r()))
    End.
    Annotations
    @Axiom( ("∨∧","|&") , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  430. lazy val orRecursor: DerivedAxiomInfo

    Axiom "| recursor".
       p() | q() <-> p() | q()
    End.
    Annotations
    @Axiom( x$2710 , x$2714 , x$2715 , x$2716 , x$2711 , x$2717 , x$2718 , x$2712 , x$2713 )
  431. lazy val orStutter: DerivedAxiomInfo

    Axiom "or stutter".
       P|Q <-> P|Q
    End.
    Annotations
    @Axiom( x$3097 , x$3101 , x$3102 , x$3103 , x$3104 , x$3100 , x$3105 , x$3098 , x$3099 )
    Note

    Trivial reflexive stutter axiom, only used with a different recursor pattern in AxiomIndex.

  432. lazy val orTrue: ProvableSig
  433. lazy val pVd: DerivedAxiomInfo

    Axiom "<> partial vacuous".
       <a;>p(||) & q() <-> <a;>(p(||)&q())
    End.
    Annotations
    @Axiom( x$1189 , x$1192 , x$1193 , x$1194 , x$1195 , x$1196 , x$1197 , x$1190 , x$1191 )
    Note

    unsound for hybrid games

  434. lazy val partition2: DerivedAxiomInfo
    Annotations
    @Axiom( "partition2" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  435. lazy val pexistsV: DerivedAxiomInfo

    Axiom "partial vacuous exists quantifier".
       (\exists x p(x) & q()) <-> (\exists x p(x)) & q()
    End.
    Annotations
    @Axiom( ("pV∃","pexistsV") , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  436. lazy val plusAssociative: DerivedAxiomInfo

    Axiom "+ associative".
       (f()+g()) + h() = f() + (g()+h())
    End.
    Annotations
    @Axiom( x$2602 , x$2604 , x$2605 , x$2606 , x$2603 , x$2607 , x$2608 , x$2609 , x$2610 )
  437. lazy val plusBranch2: DerivedAxiomInfo
    Annotations
    @Axiom( "plusBranch2" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  438. lazy val plusBranch3: DerivedAxiomInfo
    Annotations
    @Axiom( "plusBranch3" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  439. lazy val plusClosed: DerivedAxiomInfo

    Axiom "+ closed".
       0 < f() & 0 < g() -> 0 < f()+g()
    End.
    Annotations
    @Axiom( "+c" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  440. lazy val plusCommute: DerivedAxiomInfo

    Axiom "+ commute".
       f()+g() = g()+f()
    End.
    Annotations
    @Axiom( x$1972 , x$1974 , x$1975 , x$1976 , x$1973 , x$1977 , x$1978 , x$1979 , x$1980 )
  441. lazy val plusDiffRefl: DerivedAxiomInfo
    Annotations
    @Axiom( "plusDiffRefl" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  442. lazy val plusEmpty: DerivedAxiomInfo
    Annotations
    @Axiom( "plusEmpty" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  443. lazy val plusInverse: DerivedAxiomInfo

    Axiom "+ inverse".
       f() + (-f()) = 0
    End.
    Annotations
    @Axiom( x$2620 , x$2622 , x$2623 , x$2624 , x$2621 , x$2625 , x$2626 , x$2627 , x$2628 )
  444. lazy val plusMinus: DerivedAxiomInfo
    Annotations
    @Axiom( "plusMinus" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  445. lazy val plusTimes: DerivedAxiomInfo
    Annotations
    @Axiom( "plusTimes" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  446. lazy val plusZero: DerivedAxiomInfo

    Axiom "+0".
       (f()+0) = f()
    End.
    Annotations
    @Axiom( x$1963 , x$1965 , x$1966 , x$1967 , x$1964 , x$1968 , x$1969 , x$1970 , x$1971 )
  447. lazy val ponensAndPassthrough_Equiv: ProvableSig
  448. lazy val ponensAndPassthrough_Imply: ProvableSig
  449. lazy val ponensAndPassthrough_coEquiv: ProvableSig
  450. lazy val ponensAndPassthrough_coImply: ProvableSig
  451. lazy val positivity: DerivedAxiomInfo

    Axiom "positivity".
       f() < 0 | f() = 0 | 0 < f()
    End.
    Annotations
    @Axiom( "Pos" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  452. lazy val postWeaken: DerivedAxiomInfo

    Axiom "[] post weaken".
      [a;]p(||)  ->  [a;](q(||)->p(||))
    End.
    Annotations
    @Axiom( x$1621 , x$1624 , x$1625 , x$1626 , x$1627 , x$1628 , x$1629 , x$1622 , x$1623 )
  453. lazy val powOne: DerivedAxiomInfo
    Annotations
    @Axiom( x$2989 , x$2992 , x$2993 , x$2994 , x$2995 , x$2996 , x$2997 , x$2990 , x$2991 )
  454. lazy val powZero: DerivedAxiomInfo
    Annotations
    @Axiom( x$2980 , x$2983 , x$2984 , x$2985 , x$2986 , x$2987 , x$2988 , x$2981 , x$2982 )
  455. lazy val powerDivide0: DerivedAxiomInfo
    Annotations
    @Axiom( "powerDivide0" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  456. lazy val powerDivideEven: DerivedAxiomInfo
    Annotations
    @Axiom( "powerDivideEven" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  457. lazy val powerDivideOdd: DerivedAxiomInfo
    Annotations
    @Axiom( "powerDivideOdd" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  458. lazy val powerEven: DerivedAxiomInfo
    Annotations
    @Axiom( "powerEven" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  459. lazy val powerLemma: DerivedAxiomInfo
    Annotations
    @Axiom( "powerLemma" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  460. lazy val powerOdd: DerivedAxiomInfo
    Annotations
    @Axiom( "powerOdd" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  461. lazy val powerOne: DerivedAxiomInfo
    Annotations
    @Axiom( "powerOne" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  462. lazy val powerPoly: DerivedAxiomInfo
    Annotations
    @Axiom( "powerPoly" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  463. lazy val powerZero: DerivedAxiomInfo
    Annotations
    @Axiom( "powerZero" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  464. lazy val programStuck: DerivedAxiomInfo
    Annotations
    @Axiom( x$2683 , x$2686 , x$2687 , x$2688 , x$2689 , x$2690 , x$2691 , x$2684 , x$2685 )
  465. val randomb: CoreAxiomInfo
  466. lazy val randomd: DerivedAxiomInfo

    Axiom "<:*> assign nondet".
       <x:=*;>p(x) <-> (\exists x p(x))
    End.
    Annotations
    @Axiom( x$1342 , x$1348 , x$1349 , x$1343 , x$1346 , x$1347 , x$1350 , x$1344 , x$1345 )
  467. lazy val ratFormAdd: DerivedAxiomInfo
    Annotations
    @Axiom( "ratFormAdd" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  468. lazy val ratFormDivide: DerivedAxiomInfo
    Annotations
    @Axiom( "ratFormDivide" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  469. lazy val ratFormMinus: DerivedAxiomInfo
    Annotations
    @Axiom( "ratFormMinus" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  470. lazy val ratFormNeg: DerivedAxiomInfo
    Annotations
    @Axiom( "ratFormNeg" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  471. lazy val ratFormPower: DerivedAxiomInfo
    Annotations
    @Axiom( "ratFormPower" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  472. lazy val ratFormTimes: DerivedAxiomInfo
    Annotations
    @Axiom( "ratFormTimes" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  473. lazy val rationalLemma: DerivedAxiomInfo
    Annotations
    @Axiom( "rationalLemma" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  474. lazy val reassocLeft0RightConst: DerivedAxiomInfo
    Annotations
    @Axiom( "reassocLeft0RightConst" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  475. lazy val reassocRight0: DerivedAxiomInfo
    Annotations
    @Axiom( "reassocRight0" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  476. lazy val reassocRightConst: DerivedAxiomInfo
    Annotations
    @Axiom( "reassocRightConst" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  477. lazy val reassocRightPlus: DerivedAxiomInfo
    Annotations
    @Axiom( "reassocRightPlus" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  478. lazy val refineConjunction: DerivedAxiomInfo
    Annotations
    @Axiom( "refineConjunction" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  479. lazy val refineLe1: DerivedAxiomInfo
    Annotations
    @Axiom( "refineLe1" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  480. lazy val refineLe2: DerivedAxiomInfo
    Annotations
    @Axiom( "refineLe2" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  481. lazy val refineTmExists: DerivedAxiomInfo
    Annotations
    @Axiom( "refineTmExists" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  482. lazy val sameImpliesImplies: ProvableSig
  483. val selfassignb: CoreAxiomInfo
  484. lazy val selfassignby: DerivedAxiomInfo

    Semantically renamed

    Semantically renamed

    Axiom "[:=] self assign y"
      [y_:=y_;]p(||) <-> p(||)
    End.
    Annotations
    @Axiom( x$559 , x$561 , x$562 , x$563 , x$564 , x$560 , x$565 , x$566 , x$567 )
    Note

    needs semantic renaming

  485. lazy val selfassignd: DerivedAxiomInfo

    Axiom "<:=> self assign".
       <x_:=x_;>p(||) <-> p(||)
    End.
    Annotations
    @Axiom( "<:=>" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  486. lazy val splitBranch2: DerivedAxiomInfo
    Annotations
    @Axiom( "splitBranch2 " , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  487. lazy val splitBranch3: DerivedAxiomInfo
    Annotations
    @Axiom( "splitBranch3 " , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  488. lazy val splitCoefficient: DerivedAxiomInfo
    Annotations
    @Axiom( "splitCoefficient" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  489. def splitCoefficientNumericCondition(n: Term, d: Term, n1: Term, d1: Term, n2: Term, d2: Term): Formula
    Annotations
    @inline()
  490. lazy val splitEmpty: DerivedAxiomInfo
    Annotations
    @Axiom( "splitEmpty " , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  491. lazy val splitMonomial: DerivedAxiomInfo
    Annotations
    @Axiom( "splitMonomial" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  492. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  493. lazy val taylorModelApproxPrv: DerivedAxiomInfo
    Annotations
    @Axiom( "taylorModelApproxPrv" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  494. lazy val taylorModelCollectPrv: DerivedAxiomInfo
    Annotations
    @Axiom( "taylorModelCollectPrv" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  495. lazy val taylorModelDivideExactPrv: DerivedAxiomInfo
    Annotations
    @Axiom( "taylorModelDivideExactPrv" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  496. lazy val taylorModelEmptyIntervalPrv: DerivedAxiomInfo
    Annotations
    @Axiom( "taylorModelEmptyIntervalPrv" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  497. lazy val taylorModelEvalPrv: DerivedAxiomInfo
    Annotations
    @Axiom( "taylorModelEvalPrv" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  498. lazy val taylorModelExactPrv: DerivedAxiomInfo
    Annotations
    @Axiom( "taylorModelExactPrv" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  499. lazy val taylorModelIntervalGe: DerivedAxiomInfo
    Annotations
    @Axiom( "taylorModelIntervalGe" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  500. lazy val taylorModelIntervalGt: DerivedAxiomInfo
    Annotations
    @Axiom( "taylorModelIntervalGt" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  501. lazy val taylorModelIntervalLe: DerivedAxiomInfo
    Annotations
    @Axiom( "taylorModelIntervalLe" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  502. lazy val taylorModelIntervalLt: DerivedAxiomInfo
    Annotations
    @Axiom( "taylorModelIntervalLt" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  503. lazy val taylorModelIntervalPrv: DerivedAxiomInfo
    Annotations
    @Axiom( "taylorModelIntervalPrv" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  504. lazy val taylorModelMinusPrv: DerivedAxiomInfo
    Annotations
    @Axiom( "taylorModelMinusPrv" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  505. lazy val taylorModelNegPrv: DerivedAxiomInfo
    Annotations
    @Axiom( "taylorModelNegPrv" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  506. lazy val taylorModelPartitionPrv1: DerivedAxiomInfo
    Annotations
    @Axiom( "taylorModelPartitionPrv1" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  507. lazy val taylorModelPartitionPrv2: DerivedAxiomInfo
    Annotations
    @Axiom( "taylorModelPartitionPrv2" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  508. lazy val taylorModelPlusPrv: DerivedAxiomInfo

    Taylor Model Arithmetic edu.cmu.cs.ls.keymaerax.btactics.TaylorModelArith

    Annotations
    @Axiom( "taylorModelPlusPrv" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  509. lazy val taylorModelPowerEven: DerivedAxiomInfo
    Annotations
    @Axiom( "taylorModelPowerEven" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  510. lazy val taylorModelPowerOdd: DerivedAxiomInfo
    Annotations
    @Axiom( "taylorModelPowerOdd" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  511. lazy val taylorModelPowerOne: DerivedAxiomInfo
    Annotations
    @Axiom( "taylorModelPowerOne" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  512. lazy val taylorModelSquarePrv: DerivedAxiomInfo
    Annotations
    @Axiom( "taylorModelSquarePrv" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  513. lazy val taylorModelTimesPrv: DerivedAxiomInfo
    Annotations
    @Axiom( "taylorModelTimesPrv" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  514. lazy val taylorModelTransElem: DerivedAxiomInfo
    Annotations
    @Axiom( "taylorModelTransElem" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  515. val testb: CoreAxiomInfo
  516. lazy val testd: DerivedAxiomInfo

    Axiom " test".
       <?q();>p() <-> (q() & p())
    End.
    Annotations
    @Axiom( x$1351 , x$1357 , x$1358 , x$1352 , x$1355 , x$1356 , x$1359 , x$1353 , x$1354 )
  517. lazy val testdcombine: DerivedAxiomInfo
    Annotations
    @Axiom( x$1378 , x$1382 , x$1383 , x$1384 , x$1381 , x$1385 , x$1386 , x$1379 , x$1380 )
  518. lazy val timeCond: DerivedAxiomInfo
    Annotations
    @Axiom( "timeCond" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  519. lazy val timeStep: DerivedAxiomInfo
    Annotations
    @Axiom( x$2422 , x$2425 , x$2426 , x$2427 , x$2424 , x$2428 , x$2429 , x$2423 , x$2430 )
  520. lazy val timesAssociative: DerivedAxiomInfo

    Axiom "* associative".
       (f()*g()) * h() = f() * (g()*h())
    End.
    Annotations
    @Axiom( x$2611 , x$2613 , x$2614 , x$2615 , x$2612 , x$2616 , x$2617 , x$2618 , x$2619 )
  521. lazy val timesBranch2: DerivedAxiomInfo
    Annotations
    @Axiom( "timesBranch2" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  522. lazy val timesBranch3: DerivedAxiomInfo
    Annotations
    @Axiom( "timesBranch3" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  523. lazy val timesClosed: DerivedAxiomInfo

    Axiom "* closed".
       0 < f() & 0 < g() -> 0 < f()*g()
    End.
    Annotations
    @Axiom( "*c" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  524. lazy val timesCommute: DerivedAxiomInfo

    Axiom "* commute".
       f()*g() = g()*f()
    End.
    Annotations
    @Axiom( x$1936 , x$1938 , x$1939 , x$1940 , x$1937 , x$1941 , x$1942 , x$1943 , x$1944 )
  525. lazy val timesEmpty: DerivedAxiomInfo
    Annotations
    @Axiom( "timesEmpty" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  526. lazy val timesIdentity: DerivedAxiomInfo

    Axiom "* identity".
       f()*1 = f()
    End.
    Annotations
    @Axiom( "*I" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  527. lazy val timesIdentityNeg: DerivedAxiomInfo

    Axiom "* identity neg".
       f()*-1 = -f()
    End.
    Annotations
    @Axiom( x$2935 , x$2938 , x$2939 , x$2940 , x$2941 , x$2942 , x$2943 , x$2936 , x$2937 )
  528. lazy val timesInverse: DerivedAxiomInfo

    Axiom "* inverse".
       f() != 0 -> f()*(f()^-1) = 1
    End.
    Annotations
    @Axiom( x$2629 , x$2631 , x$2632 , x$2633 , x$2630 , x$2634 , x$2635 , x$2636 , x$2637 )
  529. lazy val timesLeMonoLemma: DerivedAxiomInfo
    Annotations
    @Axiom( "timesLeMonoLemma" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$default$4 , macros.this.Axiom.<init>$default$5 , macros.this.Axiom.<init>$default$6 , macros.this.Axiom.<init>$default$7 , macros.this.Axiom.<init>$default$8 , macros.this.Axiom.<init>$default$9 )
  530. lazy val timesPowers1Left: DerivedAxiomInfo
    Annotations
    @Axiom( "timesPowers1Left" , macros.this.Axiom.<init>$default$2 , macros.this.Axiom.<init>$default$3 , macros.this.Axiom.<init>$de