test.maude revision 0f35e410ce3d3202f6769e9d139ad26d1de69b8e
af84459fbf938e508fd10b01cb8d699c79083813takashifth FREENESS is
af84459fbf938e508fd10b01cb8d699c79083813takashi eq true and true = true .
af84459fbf938e508fd10b01cb8d699c79083813takashiview Freeness from FREENESS to BOOL is
af84459fbf938e508fd10b01cb8d699c79083813takashi sort Foo to Bool .
af84459fbf938e508fd10b01cb8d699c79083813takashimod TALK_TEST is
af84459fbf938e508fd10b01cb8d699c79083813takashi sorts A B C D E .
af84459fbf938e508fd10b01cb8d699c79083813takashi subsort A < B .
af84459fbf938e508fd10b01cb8d699c79083813takashi subsort A < C .
af84459fbf938e508fd10b01cb8d699c79083813takashi subsort D < E .
af84459fbf938e508fd10b01cb8d699c79083813takashi op f : A B -> C [comm assoc] .
af84459fbf938e508fd10b01cb8d699c79083813takashi op a : -> A [ctor] .
af84459fbf938e508fd10b01cb8d699c79083813takashi op b : -> B [ctor] .
af84459fbf938e508fd10b01cb8d699c79083813takashi op c : -> C [ctor] .
af84459fbf938e508fd10b01cb8d699c79083813takashi op d : -> D [ctor] .
af84459fbf938e508fd10b01cb8d699c79083813takashi op e : -> E [ctor] .
3c13a815670b54d1c17bf02954f7d2b066cde95cnd vars X Y : B .
af84459fbf938e508fd10b01cb8d699c79083813takashi ceq f(X, Y) = X if X = Y .
af84459fbf938e508fd10b01cb8d699c79083813takashi rl [d] : d => e .
af84459fbf938e508fd10b01cb8d699c79083813takashi rl f(X, Y) => Y .
af84459fbf938e508fd10b01cb8d699c79083813takashifth ALPHA_ASSOC is
af84459fbf938e508fd10b01cb8d699c79083813takashi op f : Foo Foo -> Foo [ctor assoc] .
af84459fbf938e508fd10b01cb8d699c79083813takashifmod OTHER_ALPHA_ASSOC is
af84459fbf938e508fd10b01cb8d699c79083813takashi op g : Elt Elt -> Elt [ctor] .
af84459fbf938e508fd10b01cb8d699c79083813takashi vars E1 E2 E3 : Elt .
af84459fbf938e508fd10b01cb8d699c79083813takashi eq g(E1, g(E2, E3)) = g(g(E1, E2), E3) [nonexec] .
af84459fbf938e508fd10b01cb8d699c79083813takashifth LAST_FREENESS_THEORY is
cd6c8de3bedcc401ee230159b0439fa20f44488etakashifmod LAST_FREENESS_TEST{X :: LAST_FREENESS_THEORY} is
78f97ce162b66a0dbfd7af4dcd9984f162569b04minfrin sort List .
af84459fbf938e508fd10b01cb8d699c79083813takashi subsort X$Elt < List .
af84459fbf938e508fd10b01cb8d699c79083813takashi op nil : -> List [ctor] .
af84459fbf938e508fd10b01cb8d699c79083813takashi op __ : List List -> List [ctor assoc id: nil] .
af84459fbf938e508fd10b01cb8d699c79083813takashiview VALPHA from ALPHA_ASSOC to OTHER_ALPHA_ASSOC is
af84459fbf938e508fd10b01cb8d699c79083813takashi sort Foo to Elt .
af84459fbf938e508fd10b01cb8d699c79083813takashi op f to g .
af84459fbf938e508fd10b01cb8d699c79083813takashifmod MY_LIST is
af84459fbf938e508fd10b01cb8d699c79083813takashi sorts List .
af84459fbf938e508fd10b01cb8d699c79083813takashi subsort Nat < List .
3c13a815670b54d1c17bf02954f7d2b066cde95cnd op nil : -> List [ctor] .
3c13a815670b54d1c17bf02954f7d2b066cde95cnd op __ : List List -> List [ctor assoc id: nil] .
af84459fbf938e508fd10b01cb8d699c79083813takashi var L : List .
af84459fbf938e508fd10b01cb8d699c79083813takashi var E : Nat .
af84459fbf938e508fd10b01cb8d699c79083813takashi op reverse : List -> List .
af84459fbf938e508fd10b01cb8d699c79083813takashi eq reverse(nil) = nil .
0cf3cdbaa1dad11cbf1ce32e48f1b4ec88cf779fnilgun eq reverse(E L) = reverse(L) E .
af84459fbf938e508fd10b01cb8d699c79083813takashifth TLIST is
af84459fbf938e508fd10b01cb8d699c79083813takashi sorts List2 .
af84459fbf938e508fd10b01cb8d699c79083813takashi subsort Nat < List2 .
af84459fbf938e508fd10b01cb8d699c79083813takashi op nil : -> List2 [ctor] .
af84459fbf938e508fd10b01cb8d699c79083813takashi op __ : List2 List2 -> List2 [ctor assoc id: nil] .
af84459fbf938e508fd10b01cb8d699c79083813takashi var L : List2 .
af84459fbf938e508fd10b01cb8d699c79083813takashi var E : Nat .
af84459fbf938e508fd10b01cb8d699c79083813takashi op reverse : List2 -> List2 .
af84459fbf938e508fd10b01cb8d699c79083813takashi eq reverse(reverse(L)) = L .
af84459fbf938e508fd10b01cb8d699c79083813takashiview V22 from TLIST to MY_LIST is
af84459fbf938e508fd10b01cb8d699c79083813takashi sort List2 to List .
af84459fbf938e508fd10b01cb8d699c79083813takashifmod MY_LIST_OPS is
af84459fbf938e508fd10b01cb8d699c79083813takashi pr MY_LIST .
af84459fbf938e508fd10b01cb8d699c79083813takashifth ASSOC-OP is
af84459fbf938e508fd10b01cb8d699c79083813takashi op __ : Elt Elt -> Elt [ctor assoc] .
af84459fbf938e508fd10b01cb8d699c79083813takashifth ANOTHER-ASSOC-OP is
af84459fbf938e508fd10b01cb8d699c79083813takashi op _._ : Foo Foo -> Foo [ctor] .
af84459fbf938e508fd10b01cb8d699c79083813takashi vars F1 F2 F3 : Foo .
af84459fbf938e508fd10b01cb8d699c79083813takashi eq F1 . (F2 . F3) = (F1 . F2) . F3 .
af84459fbf938e508fd10b01cb8d699c79083813takashiview ASSOC from ASSOC-OP to ANOTHER-ASSOC-OP is
af84459fbf938e508fd10b01cb8d699c79083813takashi sort Elt to Foo .
af84459fbf938e508fd10b01cb8d699c79083813takashi op __ to _._ .
af84459fbf938e508fd10b01cb8d699c79083813takashifmod TEST is
af84459fbf938e508fd10b01cb8d699c79083813takashi sorts A B C .
af84459fbf938e508fd10b01cb8d699c79083813takashi subsort A < B .
af84459fbf938e508fd10b01cb8d699c79083813takashi sorts D E F .
af84459fbf938e508fd10b01cb8d699c79083813takashi subsort D < F .
af84459fbf938e508fd10b01cb8d699c79083813takashi subsort D < E .
af84459fbf938e508fd10b01cb8d699c79083813takashi op a : -> A .
af84459fbf938e508fd10b01cb8d699c79083813takashi op b : -> B .
af84459fbf938e508fd10b01cb8d699c79083813takashi op c : -> B .
af84459fbf938e508fd10b01cb8d699c79083813takashi op f : A -> B .
af84459fbf938e508fd10b01cb8d699c79083813takashi op g : A A -> B .
af84459fbf938e508fd10b01cb8d699c79083813takashi op h : A A -> A [assoc comm id: a] .
af84459fbf938e508fd10b01cb8d699c79083813takashi vars X Y : A .
af84459fbf938e508fd10b01cb8d699c79083813takashi eq f(a) = b .
af84459fbf938e508fd10b01cb8d699c79083813takashi eq f(X) = c [owise] .
af84459fbf938e508fd10b01cb8d699c79083813takashi eq g(a,X) = b .
af84459fbf938e508fd10b01cb8d699c79083813takashi eq g(X, Y) = c [owise] .
af84459fbf938e508fd10b01cb8d699c79083813takashi ceq h(a, a) = a
af84459fbf938e508fd10b01cb8d699c79083813takashi if true /\ not false .
af84459fbf938e508fd10b01cb8d699c79083813takashifmod TEST2 is
af84459fbf938e508fd10b01cb8d699c79083813takashi sorts C D .
af84459fbf938e508fd10b01cb8d699c79083813takashi subsort C < D .
af84459fbf938e508fd10b01cb8d699c79083813takashi op c : -> C .
af84459fbf938e508fd10b01cb8d699c79083813takashi op d : -> D .
af84459fbf938e508fd10b01cb8d699c79083813takashi op {_} : C -> C .
af84459fbf938e508fd10b01cb8d699c79083813takashi op g : C -> D .
af84459fbf938e508fd10b01cb8d699c79083813takashi eq g(c) = d .
af84459fbf938e508fd10b01cb8d699c79083813takashifmod TEST3 is
af84459fbf938e508fd10b01cb8d699c79083813takashi pr TEST + (TEST2 * (sort C to CC, sort D to DD, op g to gg)) .
af84459fbf938e508fd10b01cb8d699c79083813takashi op x : -> CC .
af84459fbf938e508fd10b01cb8d699c79083813takashifth TEST4 is
af84459fbf938e508fd10b01cb8d699c79083813takashi ops a b : -> Foo .
af84459fbf938e508fd10b01cb8d699c79083813takashi op f : Foo -> Foo .
af84459fbf938e508fd10b01cb8d699c79083813takashifmod TEST5{X :: TEST4 * (sort Foo to Faa)} is
af84459fbf938e508fd10b01cb8d699c79083813takashi sort Test5 .
af84459fbf938e508fd10b01cb8d699c79083813takashi op c : -> Test5 .
af84459fbf938e508fd10b01cb8d699c79083813takashiview VNat from TRIV * (sort Elt to Elt2) to NAT * (sort Nat to Naaaaat) is
af84459fbf938e508fd10b01cb8d699c79083813takashi sort Elt2 to Naaaaat .
af84459fbf938e508fd10b01cb8d699c79083813takashiview V1 from TRIV to BOOL is
af84459fbf938e508fd10b01cb8d699c79083813takashi sort Elt to Bool .
af84459fbf938e508fd10b01cb8d699c79083813takashifmod TEST6{X :: TRIV} is
af84459fbf938e508fd10b01cb8d699c79083813takashi sort Foo6 .
af84459fbf938e508fd10b01cb8d699c79083813takashifmod TEST7 is
af84459fbf938e508fd10b01cb8d699c79083813takashi pr (TEST6 * (sort Foo6 to Fooooo6)){V1} .
af84459fbf938e508fd10b01cb8d699c79083813takashifth TEST8 is
af84459fbf938e508fd10b01cb8d699c79083813takashi sorts Foo Faa .
af84459fbf938e508fd10b01cb8d699c79083813takashi op update : Foo -> Faa .
af84459fbf938e508fd10b01cb8d699c79083813takashiview V2 from TEST8 to BOOL is
af84459fbf938e508fd10b01cb8d699c79083813takashi sort Foo to Bool .
af84459fbf938e508fd10b01cb8d699c79083813takashi sort Faa to Bool .
af84459fbf938e508fd10b01cb8d699c79083813takashi op update(X:Foo) to term _or_(true, X:Bool) .
af84459fbf938e508fd10b01cb8d699c79083813takashifmod MYLIST is
af84459fbf938e508fd10b01cb8d699c79083813takashi sorts List .
af84459fbf938e508fd10b01cb8d699c79083813takashi subsort Nat < List .
af84459fbf938e508fd10b01cb8d699c79083813takashi op nil : -> List [ctor] .
af84459fbf938e508fd10b01cb8d699c79083813takashi op __ : List List -> List [ctor assoc id: nil] .
af84459fbf938e508fd10b01cb8d699c79083813takashi var L : List .
78f97ce162b66a0dbfd7af4dcd9984f162569b04minfrin var E : Nat .
af84459fbf938e508fd10b01cb8d699c79083813takashi op reverse : List -> List .
af84459fbf938e508fd10b01cb8d699c79083813takashi eq reverse(nil) = nil .
af84459fbf938e508fd10b01cb8d699c79083813takashi eq reverse(E L) = reverse(L) E .
3c13a815670b54d1c17bf02954f7d2b066cde95cnd sorts List .
af84459fbf938e508fd10b01cb8d699c79083813takashi subsort Nat < List .
af84459fbf938e508fd10b01cb8d699c79083813takashi op nil : -> List [ctor] .
af84459fbf938e508fd10b01cb8d699c79083813takashi op __ : List List -> List [ctor assoc id: nil] .
af84459fbf938e508fd10b01cb8d699c79083813takashi var L : List .
af84459fbf938e508fd10b01cb8d699c79083813takashi var E : Nat .
af84459fbf938e508fd10b01cb8d699c79083813takashi op reverse : List -> List .
af84459fbf938e508fd10b01cb8d699c79083813takashi eq reverse(reverse(L)) = L .
af84459fbf938e508fd10b01cb8d699c79083813takashiview IDEM from TH to MYLIST is
af84459fbf938e508fd10b01cb8d699c79083813takashi sort List to List .
af84459fbf938e508fd10b01cb8d699c79083813takashi op nil to nil .
af84459fbf938e508fd10b01cb8d699c79083813takashi op __ to __ .
af84459fbf938e508fd10b01cb8d699c79083813takashi op reverse to reverse .