c

# Sequent 

#### final case class Sequent(ante: IndexedSeq[Formula], succ: IndexedSeq[Formula]) extends Product with Serializable

Sequent ante |- succ with antecedent ante and succedent succ.

ante(0),ante(1),...,ante(n) |- succ(0),succ(1),...,succ(m)

This sequent is often pretty-printed with signed line numbers:

    -1: ante(0)
-2: ante(1)
...
-(n+1): ante(n)
==> 1: succ(0)
2: succ(1)
...
(m+1): succ(m)

The semantics of sequent ante |- succ is the conjunction of the formulas in ante implying the disjunction of the formulas in succ.

ante

The ordered list of antecedents of this sequent whose conjunction is assumed.

succ

The orderd list of succedents of this sequent whose disjunction needs to be shown.

Andre Platzer. Differential dynamic logic for hybrid systems. Journal of Automated Reasoning, 41(2), pages 143-189, 2008.

Linear Supertypes
Serializable, Serializable, Product, Equals, AnyRef, Any
Ordering
1. Alphabetic
2. By Inheritance
Inherited
1. Sequent
2. Serializable
3. Serializable
4. Product
5. Equals
6. AnyRef
7. Any
1. Hide All
2. Show All
Visibility
1. Public
2. All

### Instance Constructors

1. new Sequent(ante: IndexedSeq[Formula], succ: IndexedSeq[Formula])

ante

The ordered list of antecedents of this sequent whose conjunction is assumed.

succ

The orderd list of succedents of this sequent whose disjunction needs to be shown.

### Value Members

1. final def !=(arg0: Any): Boolean
Definition Classes
AnyRef → Any
2. final def ##(): Int
Definition Classes
AnyRef → Any
3. final def ==(arg0: Any): Boolean
Definition Classes
AnyRef → Any
4. val ante: IndexedSeq[Formula]
5. def apply(pos: SuccPos)

Retrieves the formula in sequent at a given antecedent position.

Retrieves the formula in sequent at a given antecedent position.

pos

the antecedent position of the formula

returns

the formula at the given position from the antecedent

Note

slightly faster version with the same result as Sequent.apply(SeqPos)

6. def apply(pos: AntePos)

Retrieves the formula in sequent at a given succedent position.

Retrieves the formula in sequent at a given succedent position.

pos

the succedent position of the formula

returns

the formula at the given position from the succedent

Note

slightly faster version with the same result as Sequent.apply(SeqPos)

7. def apply(pos: SeqPos)

Retrieves the formula in sequent at a given position.

Retrieves the formula in sequent at a given position.

pos

the position of the formula

returns

the formula at the given position either from the antecedent or the succedent

8. final def asInstanceOf[T0]: T0
Definition Classes
Any
9. def clone(): AnyRef
Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@native() @throws( ... )
10. final def eq(arg0: AnyRef): Boolean
Definition Classes
AnyRef
11. def finalize(): scala.Unit
Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@throws( classOf[java.lang.Throwable] )
12. final def getClass(): Class[_]
Definition Classes
AnyRef → Any
Annotations
@native()
13. def glue(s: Sequent)

A copy of this sequent concatenated with given sequent s.

A copy of this sequent concatenated with given sequent s. Sequent(A,S) glue Sequent(B,T) == Sequent(A++B, S++T)

s

the sequent whose antecedent to append to ours and whose succedent to append to ours.

returns

a copy of this sequent concatenated with s. Results in a least upper bound with respect to subsets of this and s.

14. final def isInstanceOf[T0]: Boolean
Definition Classes
Any
15. final def ne(arg0: AnyRef): Boolean
Definition Classes
AnyRef
16. final def notify(): scala.Unit
Definition Classes
AnyRef
Annotations
@native()
17. final def notifyAll(): scala.Unit
Definition Classes
AnyRef
Annotations
@native()
18. def prettyString: String

Pretty-print sequent

19. def sameSequentAs(r: Sequent): Boolean

Check whether this sequent is the same as the given sequent r (considered as sets)

Check whether this sequent is the same as the given sequent r (considered as sets)

Note

Used for contracts in the core.

20. def subsequentOf(r: Sequent): Boolean

Check whether this sequent is a subsequent of the given sequent r (considered as sets)

Check whether this sequent is a subsequent of the given sequent r (considered as sets)

Note

Used for contracts in the core.

21. val succ: IndexedSeq[Formula]
22. final def synchronized[T0](arg0: ⇒ T0): T0
Definition Classes
AnyRef
23. def toString(): String
Definition Classes
Sequent → AnyRef → Any
24. def updated(p: SuccPos, s: Sequent)
25. def updated(p: AntePos, s: Sequent)
26. def updated(p: SeqPos, s: Sequent)

A copy of this sequent with the indicated position replaced by gluing the sequent s.

A copy of this sequent with the indicated position replaced by gluing the sequent s.

p

the position of the replacement

s

the sequent glued / concatenated to this sequent after dropping p.

returns

a copy of this sequent with the formula at position p removed and the sequent s appended.

Sequent.glue(Sequent)

Sequent.updated(Position,Formula)

27. def updated(p: SuccPos, f: Formula)
28. def updated(p: AntePos, f: Formula)
29. def updated(p: SeqPos, f: Formula)

A copy of this sequent with the indicated position replaced by the formula f.

A copy of this sequent with the indicated position replaced by the formula f.

p

the position of the replacement

f

the replacing formula

returns

a copy of this sequent with the formula at position p replaced by f.

30. final def wait(): scala.Unit
Definition Classes
AnyRef
Annotations
@throws( ... )
31. final def wait(arg0: Long, arg1: Int): scala.Unit
Definition Classes
AnyRef
Annotations
@throws( ... )
32. final def wait(arg0: Long): scala.Unit
Definition Classes
AnyRef
Annotations
@native() @throws( ... )