final def !=(arg0: Any): Boolean

Definition Classes: AnyRef → Any

final def ##(): Int

Definition Classes: AnyRef → Any

final def ==(arg0: Any): Boolean

Definition Classes: AnyRef → Any

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 )

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 )

val CErule: AxiomaticRuleInfo

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 )

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 )

val CQrule: AxiomaticRuleInfo

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 )

val Cont: CoreAxiomInfo

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

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

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

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

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

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

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

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 )

val DCC: CoreAxiomInfo

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 )

val DE: CoreAxiomInfo

val DEs: CoreAxiomInfo

lazy val DEsysy: DerivedAxiomInfo

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

val DGC: CoreAxiomInfo

val DGCa: CoreAxiomInfo

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 )

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 )

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 )

val DGa: CoreAxiomInfo

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 )

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 )

val DGi: CoreAxiomInfo

val DGpp: CoreAxiomInfo

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 )

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 )

val DIequiv: CoreAxiomInfo

val DIogreater: CoreAxiomInfo

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 )

val DMP: CoreAxiomInfo

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 )

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 )

val DS: CoreAxiomInfo

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 )

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&

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&

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."

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 )

val DWbase: CoreAxiomInfo

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 )

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 )

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 )

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 )

val DX: CoreAxiomInfo

val Dand: CoreAxiomInfo

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 )

val Dassignb: CoreAxiomInfo

val Dassignbeq: CoreAxiomInfo

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 )

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 )

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 )

lazy val DassigndAxiom: DerivedAxiomInfo

Annotations: @Axiom( x$1243 , x$1248 , x$1249 , x$1244 , x$1247 , x$1250 , x$1251 , x$1245 , x$1246 )

lazy val DassigndEqualityAxiom: DerivedAxiomInfo

Annotations: @Axiom( x$1261 , x$1266 , x$1267 , x$1262 , x$1268 , x$1263 , x$1269 , x$1264 , x$1265 )

val Dcomp: CoreAxiomInfo

val Dcompose: CoreAxiomInfo

val Dconst: CoreAxiomInfo

val Dequal: DerivedAxiomInfo

val Dexists: CoreAxiomInfo

val Dforall: CoreAxiomInfo

val Dgreater: CoreAxiomInfo

val Dgreaterequal: CoreAxiomInfo

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 )

val Dless: DerivedAxiomInfo

Axiom "<' derive <"
   (f(||) < g(||))' <-> ((f(||))' <= (g(||))')
   // sic(!) easier
End.

val Dlessequal: DerivedAxiomInfo

Axiom "<=' derive <=".
   (f(||) <= g(||))' <-> ((f(||))' <= (g(||))')
End.

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 )

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 )

val Dminus: CoreAxiomInfo

val Dneg: CoreAxiomInfo

val Dnotequal: DerivedAxiomInfo

Axiom "!=' derive !="
   (f(||) != g(||))' <-> ((f(||))' = (g(||))')
   // sic!
End.

val Dor: CoreAxiomInfo

val Dplus: CoreAxiomInfo

val Dpower: CoreAxiomInfo

val Dquotient: CoreAxiomInfo

val Dselfassignb: CoreAxiomInfo

val Dtimes: CoreAxiomInfo

val DvarAxiom: CoreAxiomInfo

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 )

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 )

val FPrule: AxiomaticRuleInfo

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

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

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 )

val IVT: CoreAxiomInfo

val Iind: CoreAxiomInfo

val K: CoreAxiomInfo

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

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

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 )

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 )

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

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

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

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

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

val RI: CoreAxiomInfo

val RIclosedgeq: CoreAxiomInfo

lazy val TExge: DerivedAxiomInfo

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 )

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 )

val Uniq: CoreAxiomInfo

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 )

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

val VK: CoreAxiomInfo

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 )

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 )

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 )

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

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 [:=]

lazy val allInstPrime: DerivedAxiomInfo

Annotations: @Axiom( x$775 , x$779 , x$780 , x$776 , x$781 , x$782 , x$783 , x$777 , x$778 )

val allPd: CoreAxiomInfo

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.

lazy val allStutterPrime: DerivedAxiomInfo

Annotations: @Axiom( x$3061 , x$3065 , x$3066 , x$3067 , x$3068 , x$3064 , x$3069 , x$3062 , x$3063 )

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 )

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

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

val alld: CoreAxiomInfo

all dual

lazy val alldt: DerivedAxiomInfo

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

lazy val alldy: DerivedAxiomInfo

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

val alle: CoreAxiomInfo

all eliminate

val alleprime: CoreAxiomInfo

lazy val ally: DerivedAxiomInfo

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

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 )

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 )

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 )

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 )

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 )

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 )

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.

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 )

lazy val andTrueInv: DerivedAxiomInfo

Annotations: @Axiom( x$1891 , x$1894 , x$1895 , x$1896 , x$1897 , x$1898 , x$1899 , x$1892 , x$1893 )

final def asInstanceOf[T0]: T0

Definition Classes: Any

lazy val assignDAxiomb: ProvableSig

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

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

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

val assignbAxiom: CoreAxiomInfo

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 )

val assignbeq: CoreAxiomInfo

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

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 )

lazy val assignbeqy: DerivedAxiomInfo

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

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 )

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.

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 )

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 )

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 )

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.

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

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

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

val barcan: CoreAxiomInfo

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"

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

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

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

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

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 )

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 )

val boxTrueAxiom: CoreAxiomInfo

lazy val boxTrueTrue: ProvableSig

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

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

val choiceb: CoreAxiomInfo

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

def clone(): AnyRef

Attributes: protected[java.lang]
Definition Classes: AnyRef
Annotations: @native() @throws( ... )

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 )

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 )

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 )

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 )

val commaCommute: CoreAxiomInfo

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 )

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 )

val commaSort: CoreAxiomInfo

val composeb: CoreAxiomInfo

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 )

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 )

val conrule: AxiomaticRuleInfo

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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

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

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

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

def derivedRule(name: String, fact: ProvableSig, codeNameOpt: Option[String]): DerivedRuleInfo

val diamond: CoreAxiomInfo

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

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

lazy val dualIVT: DerivedAxiomInfo

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 )

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 )

val duald: CoreAxiomInfo

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 )

final def eq(arg0: AnyRef): Boolean

Definition Classes: AnyRef

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 )

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 )

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 )

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 )

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 )

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

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

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 )

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 )

def equals(arg0: Any): Boolean

Definition Classes: AnyRef → Any

lazy val equivExpand: DerivedAxiomInfo

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 )

lazy val equivExpandAnd: DerivedAxiomInfo

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 )

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

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.

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 )

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 )

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 )

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 )

lazy val existsDualy: DerivedAxiomInfo

Annotations: @Axiom( x$982 , x$984 , x$985 , x$986 , x$987 , x$983 , x$988 , x$989 , x$990 )

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 )

lazy val existsGeneralizey: DerivedAxiomInfo

Annotations: @Axiom( x$1549 , x$1551 , x$1552 , x$1553 , x$1554 , x$1550 , x$1555 , x$1556 , x$1557 )

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 )

lazy val existsPDual: DerivedAxiomInfo

Annotations: @Axiom( x$964 , x$967 , x$968 , x$969 , x$970 , x$971 , x$972 , x$965 , x$966 )

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.

lazy val existsStutterPrime: DerivedAxiomInfo

Annotations: @Axiom( x$3079 , x$3083 , x$3084 , x$3085 , x$3086 , x$3082 , x$3087 , x$3080 , x$3081 )

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 )

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 )

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 )

lazy val factorAndLeft: ProvableSig

lazy val factorAndRight: ProvableSig

lazy val factorImpliesOrLeft: ProvableSig

lazy val factorImpliesOrRight: ProvableSig

lazy val factorOrLeft: ProvableSig

lazy val factorOrRight: ProvableSig

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 )

def finalize(): Unit

Attributes: protected[java.lang]
Definition Classes: AnyRef
Annotations: @throws( classOf[java.lang.Throwable] )

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 )

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 )

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 )

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 )

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 )

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 )

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

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 )

lazy val geNormalize: DerivedAxiomInfo

Annotations: @Axiom( x$2368 , x$2371 , x$2372 , x$2373 , x$2374 , x$2375 , x$2376 , x$2369 , x$2370 )

final def getClass(): Class[_]

Definition Classes: AnyRef → Any
Annotations: @native()

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 )

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 )

lazy val greaterEqualRefl: DerivedAxiomInfo

Annotations: @Axiom( x$3043 , x$3047 , x$3048 , x$3049 , x$3044 , x$3050 , x$3051 , x$3045 , x$3046 )

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 )

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 )

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 )

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 )

lazy val greaterNotRefl: DerivedAxiomInfo

Annotations: @Axiom( x$3007 , x$3011 , x$3012 , x$3013 , x$3008 , x$3014 , x$3015 , x$3009 , x$3010 )

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 )

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 )

lazy val gtNormalize: DerivedAxiomInfo

Annotations: @Axiom( x$3151 , x$3154 , x$3155 , x$3156 , x$3157 , x$3158 , x$3159 , x$3152 , x$3153 )

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 )

def hashCode(): Int

Definition Classes: AnyRef → Any
Annotations: @native()

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 )

lazy val impliesMonAndLeft: ProvableSig

lazy val impliesMonAndRight: ProvableSig

lazy val impliesRightAnd: ProvableSig

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 )

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 )

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 )

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 )

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.

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 )

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 )

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 )

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.

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

lazy val invtestd: DerivedAxiomInfo

Annotations: @Axiom( x$1369 , x$1373 , x$1374 , x$1375 , x$1372 , x$1376 , x$1377 , x$1370 , x$1371 )

final def isInstanceOf[T0]: Boolean

Definition Classes: Any

val iterateb: CoreAxiomInfo

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 )

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

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 )

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 )

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 )

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 )

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 )

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 )

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 )

lazy val lessEqualRefl: DerivedAxiomInfo

Annotations: @Axiom( x$3034 , x$3038 , x$3039 , x$3040 , x$3035 , x$3041 , x$3042 , x$3036 , x$3037 )

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 )

lazy val lessNotRefl: DerivedAxiomInfo

Annotations: @Axiom( x$2998 , x$3002 , x$3003 , x$3004 , x$2999 , x$3005 , x$3006 , x$3000 , x$3001 )

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 )

lazy val logger: Logger

Attributes: protected
Definition Classes: LazyLogging → LoggerHolder

final val loggerName: String

Attributes: protected
Definition Classes: LoggerHolder

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 )

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 )

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 )

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 )

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.

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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."

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."

val mondrule: AxiomaticRuleInfo

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 )

final def ne(arg0: AnyRef): Boolean

Definition Classes: AnyRef

lazy val neNormalize: DerivedAxiomInfo

Annotations: @Axiom( x$3142 , x$3145 , x$3146 , x$3147 , x$3148 , x$3149 , x$3150 , x$3143 , x$3144 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

lazy val notEqualNotRefl: DerivedAxiomInfo

Annotations: @Axiom( x$3016 , x$3020 , x$3021 , x$3022 , x$3017 , x$3023 , x$3024 , x$3018 , x$3019 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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.

final def notify(): Unit

Definition Classes: AnyRef
Annotations: @native()

final def notifyAll(): Unit

Definition Classes: AnyRef
Annotations: @native()

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.

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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.

lazy val orTrue: ProvableSig

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

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

lazy val ponensAndPassthrough_Equiv: ProvableSig

lazy val ponensAndPassthrough_Imply: ProvableSig

lazy val ponensAndPassthrough_coEquiv: ProvableSig

lazy val ponensAndPassthrough_coImply: ProvableSig

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 )

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 )

lazy val powOne: DerivedAxiomInfo

Annotations: @Axiom( x$2989 , x$2992 , x$2993 , x$2994 , x$2995 , x$2996 , x$2997 , x$2990 , x$2991 )

lazy val powZero: DerivedAxiomInfo

Annotations: @Axiom( x$2980 , x$2983 , x$2984 , x$2985 , x$2986 , x$2987 , x$2988 , x$2981 , x$2982 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

lazy val programStuck: DerivedAxiomInfo

Annotations: @Axiom( x$2683 , x$2686 , x$2687 , x$2688 , x$2689 , x$2690 , x$2691 , x$2684 , x$2685 )

val randomb: CoreAxiomInfo

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

lazy val sameImpliesImplies: ProvableSig

val selfassignb: CoreAxiomInfo

lazy val selfassignby: DerivedAxiomInfo

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

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 )

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 )

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 )

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 )

def splitCoefficientNumericCondition(n: Term, d: Term, n1: Term, d1: Term, n2: Term, d2: Term): Formula

Annotations: @inline()

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 )

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 )

final def synchronized[T0](arg0: ⇒ T0): T0

Definition Classes: AnyRef

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

val testb: CoreAxiomInfo

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 )

lazy val testdcombine: DerivedAxiomInfo

Annotations: @Axiom( x$1378 , x$1382 , x$1383 , x$1384 , x$1381 , x$1385 , x$1386 , x$1379 , x$1380 )

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 )

lazy val timeStep: DerivedAxiomInfo

Annotations: @Axiom( x$2422 , x$2425 , x$2426 , x$2427 , x$2424 , x$2428 , x$2429 , x$2423 , x$2430 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

lazy val timesPowers1Left: DerivedAxiomInfo

Annotations: @Axiom( "timesPowers1Left" , 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 )

lazy val timesPowers1Right: DerivedAxiomInfo

Annotations: @Axiom( "timesPowers1Right" , 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 )

lazy val timesPowersBoth: DerivedAxiomInfo

Annotations: @Axiom( "timesPowersBoth" , 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 )

lazy val timesPowersLeft: DerivedAxiomInfo

Annotations: @Axiom( "timesPowersLeft" , 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 )

lazy val timesPowersRight: DerivedAxiomInfo

Annotations: @Axiom( "timesPowersRight" , 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 )

lazy val timesZero: DerivedAxiomInfo

Axiom "*0".
   (f()*0) = 0
End.

Annotations: @Axiom( x$1927 , x$1929 , x$1930 , x$1931 , x$1928 , x$1932 , x$1933 , x$1934 , x$1935 )

def toString(): String

Definition Classes: AnyRef → Any

lazy val trivialInequality: DerivedAxiomInfo

Annotations: @Axiom( "trivialInequality" , 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 )

lazy val trivialRefineGeLe: DerivedAxiomInfo

Annotations: @Axiom( "trivialRefineGeLe" , 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 )

lazy val trivialRefineLtGt: DerivedAxiomInfo

Annotations: @Axiom( "trivialRefineLtGt" , 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 )

lazy val trueAnd: DerivedAxiomInfo

Axiom "true&".
   (true&p()) <-> p()
End.

Annotations: @Axiom( x$1900 , x$1903 , x$1904 , x$1901 , x$1902 , x$1905 , x$1906 , x$1907 , x$1908 )

lazy val trueImply: DerivedAxiomInfo

Axiom "true->".
   (true->p()) <-> p()
End.

Annotations: @Axiom( x$1873 , x$1876 , x$1877 , x$1874 , x$1875 , x$1878 , x$1879 , x$1880 , x$1881 )

lazy val trueOr: ProvableSig

lazy val unfoldExistsLemma: DerivedAxiomInfo

Taylor Model edu.cmu.cs.ls.keymaerax.btactics.TaylorModelTactics

Annotations: @Axiom( "unfoldExistsLemma" , 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 )

lazy val vacuousAssignb: DerivedAxiomInfo

Axiom "[:=] vacuous assign".
   [v:=t();]p() <-> p()
End.

Annotations: @Axiom( "V[:=]" , 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 )

lazy val vacuousAssignd: DerivedAxiomInfo

Axiom "<:=> vacuous assign".
   <v:=t();>p() <-> p()
End.

Annotations: @Axiom( "V<:=>" , 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 )

lazy val vacuousBoxAssignNondet: DerivedAxiomInfo

Axiom "V[:*] vacuous assign nondet".
   [x:=*;]p() <-> p()
End.
@todo reorient
@Derived

Annotations: @Axiom( x$1594 , x$1598 , x$1599 , x$1595 , x$1600 , x$1601 , x$1602 , x$1596 , x$1597 )

lazy val vacuousDiamondAssignNondet: DerivedAxiomInfo

Axiom "V<:*> vacuous assign nondet".
   <x:=*;>p() <-> p()
End.

Annotations: @Axiom( x$1603 , x$1607 , x$1608 , x$1604 , x$1609 , x$1610 , x$1611 , x$1605 , x$1606 )
To do: reorient

lazy val varLemma: DerivedAxiomInfo

Annotations: @Axiom( "varLemma" , 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 )

lazy val varPowerLemma: DerivedAxiomInfo

Annotations: @Axiom( "varPowerLemma" , 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 )

final def wait(): Unit

Definition Classes: AnyRef
Annotations: @throws( ... )

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

Definition Classes: AnyRef
Annotations: @throws( ... )

final def wait(arg0: Long): Unit

Definition Classes: AnyRef
Annotations: @native() @throws( ... )

lazy val zeroDivNez: DerivedAxiomInfo

Annotations: @Axiom( "zeroDivNez" , 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 )

lazy val zeroMinus: DerivedAxiomInfo

Axiom "0-".
   (0-f()) = -f()
End.

Annotations: @Axiom( x$2971 , x$2975 , x$2976 , x$2977 , x$2972 , x$2978 , x$2979 , x$2973 , x$2974 )

lazy val zeroPlus: DerivedAxiomInfo

Axiom "0+".
   (0+f()) = f()
End.

Annotations: @Axiom( x$1954 , x$1956 , x$1957 , x$1958 , x$1955 , x$1959 , x$1960 , x$1961 , x$1962 )

lazy val zeroTimes: DerivedAxiomInfo

Axiom "0*".
   (0*f()) = 0
End.

Annotations: @Axiom( x$1918 , x$1920 , x$1921 , x$1922 , x$1919 , x$1923 , x$1924 , x$1925 , x$1926 )

lazy val zez: DerivedAxiomInfo

Annotations: @Axiom( "zez" , 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 )

Packages

KeYmaera X: An aXiomatic Tactical Theorem Prover

Package Structure

Entry Points

References

Proof Styles

Explicit Proof Certificates

Explicit Proofs

Proof by Search

Proof by Pointing

Proof by Congruence

Proof by Chase

Additional Mechanisms

Ax

object Ax extends Logging

Using Axioms and Axiomatic Rules

Adding Derived Axioms and Derived Axiomatic Rules

Type Members

Value Members

Inherited from Logging

Inherited from LazyLogging

Inherited from LoggerHolder

Inherited from AnyRef

Inherited from Any

Ungrouped

Packages

KeYmaera X: An aXiomatic Tactical Theorem Prover

Package Structure

Entry Points

References

Proof Styles

Explicit Proof Certificates

Explicit Proofs

Proof by Search

Proof by Pointing

Proof by Congruence

Proof by Chase

Additional Mechanisms

Ax 

object Ax extends Logging

Using Axioms and Axiomatic Rules

Adding Derived Axioms and Derived Axiomatic Rules

Type Members

Value Members

Inherited from Logging

Inherited from LazyLogging

Inherited from LoggerHolder

Inherited from AnyRef

Inherited from Any

Ungrouped

Ax