search

andreinaku / SpyType

MIT License
0 stars 0 forks source link

transitivity over maude operations #29

Closed andreinaku closed 2 months ago

andreinaku commented 3 months ago 
((a:T1) ^ (T1 <= list< T3 > /\ T1 <= T4 /\ T4 <= list< T3 >))

we get

(a:T1) ^ ((T4 <= list< T3 >) /\ (T1 <= bot))