[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Theorem base for Specification 2-way-sort

This is a listing of all goals defined over the current specification. Axioms are yellow, proof obligations purple and theorems green. Click on individual names to get more information on the proof.

Name:	Sequent:	Type:
two_way_sort-decl		An Axiom
swap-decl		An Axiom
two_way_sort-corr-term	ar = ar0 ⊦ ⟪two_way_sort#(; ar)⟫ (issorted(ar) ∧ isperm(ar, ar0))	A User Theorem