kore: getReturnSort: Case of \mu, \or, \and

prover/lang/kore-lang.md

@@ -317,6 +317,28 @@ module KORE-HELPERS
   rule [[ getReturnSort( R ( ARGS ) )  => S ]]
        <declaration> symbol R ( _ ) : S </declaration>
 
+  rule getReturnSort(\mu _ . Phi) => getReturnSort(Phi)
+  rule getReturnSort(\or(P, Ps)) => unionSort(getReturnSort(P), getReturnSort(\or(Ps)))
+  rule getReturnSort(\or(.Patterns)) => BottomSort
+  rule getReturnSort(\and(P, Ps)) => intersectSort(getReturnSort(P), getReturnSort(\and(Ps)))
+  rule getReturnSort(\and(.Patterns)) => TopSort
+  rule getReturnSort(_:SetVariable) => TopSort
+
+  syntax Sort ::= "TopSort"         [token]
+                | "BottomSort"      [token]
+
+  syntax Sort ::= unionSort(Sort, Sort) [function]
+  rule unionSort(TopSort, S) => TopSort
+  rule unionSort(S, TopSort) => TopSort
+  rule unionSort(BottomSort, S) => S
+  rule unionSort(S, BottomSort) => S
+
+  syntax Sort ::= intersectSort(Sort, Sort) [function]
+  rule intersectSort(TopSort, S) => S
+  rule intersectSort(S, TopSort) => S
+  rule intersectSort(BottomSort, S) => BottomSort
+  rule intersectSort(S, BottomSort) => BottomSort
+
   syntax Bool ::= isUnfoldable(Symbol) [function]
   rule [[ isUnfoldable(S:Symbol) => true ]]
        <declaration> axiom _ : \forall {_} \iff-lfp(S(_), _) </declaration>

prover/t/ltl/until-implies-eventually.kore

@@ -1,4 +1,4 @@
-symbol next(State) : State
+symbol next(TopSort) : TopSort
 
 // there is always a next state
 axiom inf: next(\top())
@@ -7,8 +7,8 @@ axiom inf: next(\top())
 axiom lin: \implies(next(#X), \not(next(\not(#X))))
 
 // phi1 U phi2 => []phi2
-claim \implies( \mu #X . \or(PHI2, \and(PHI1, next(#X)))
-              , \mu #X . \or(PHI2, next(#X))
+claim \implies( \mu #X . \or(#PHI2, \and(#PHI1, next(#X)))
+              , \mu #X . \or(#PHI2, next(#X))
               )
 
 /*