Require Import ADPUnif. Require Import ADecomp. Require Import ADuplicateSymb. Require Import AGraph. Require Import APolyInt_MA. Require Import ATrs. Require Import List. Require Import LogicUtil. Require Import MonotonePolynom. Require Import Polynom. Require Import SN. Require Import VecUtil. Open Scope nat_scope. (* termination problem *) Module M. Inductive symb : Type := | F : symb | T : symb | _0_1 : symb | _if_2 : symb | a : symb | and : symb | andt : symb | append : symb | calls : symb | case0 : symb | case1 : symb | case2 : symb | case4 : symb | case5 : symb | case6 : symb | case8 : symb | case9 : symb | cons : symb | delete : symb | element : symb | empty : symb | eq : symb | eqc : symb | eqs : symb | eqt : symb | equal : symb | excl : symb | excllock : symb | false : symb | gen_modtageq : symb | gen_tag : symb | imp : symb | int : symb | istops : symb | lock : symb | locker : symb | locker2_add_pending : symb | locker2_adduniq : symb | locker2_check_available : symb | locker2_check_availables : symb | locker2_claim_lock : symb | locker2_map_add_pending : symb | locker2_map_claim_lock : symb | locker2_map_promote_pending : symb | locker2_obtainable : symb | locker2_obtainables : symb | locker2_promote_pending : symb | locker2_release_lock : symb | locker2_remove_pending : symb | mcrlrecord : symb | member : symb | nil : symb | nocalls : symb | not : symb | ok : symb | or : symb | pending : symb | pid : symb | pops : symb | push : symb | push1 : symb | pushs : symb | record_extract : symb | record_new : symb | record_update : symb | record_updates : symb | release : symb | request : symb | resource : symb | s : symb | stack : symb | subtract : symb | tag : symb | tops : symb | true : symb | tuple : symb | tuplenil : symb | undefined : symb. End M. Lemma eq_symb_dec : forall f g : M.symb, {f=g}+{~f=g}. Proof. decide equality. Defined. Open Scope nat_scope. Definition ar (s : M.symb) : nat := match s with | M.F => 0 | M.T => 0 | M._0_1 => 0 | M._if_2 => 3 | M.a => 0 | M.and => 2 | M.andt => 2 | M.append => 2 | M.calls => 3 | M.case0 => 3 | M.case1 => 4 | M.case2 => 3 | M.case4 => 3 | M.case5 => 4 | M.case6 => 4 | M.case8 => 4 | M.case9 => 4 | M.cons => 2 | M.delete => 2 | M.element => 2 | M.empty => 0 | M.eq => 2 | M.eqc => 2 | M.eqs => 2 | M.eqt => 2 | M.equal => 2 | M.excl => 0 | M.excllock => 0 | M.false => 0 | M.gen_modtageq => 2 | M.gen_tag => 1 | M.imp => 2 | M.int => 1 | M.istops => 2 | M.lock => 0 | M.locker => 0 | M.locker2_add_pending => 3 | M.locker2_adduniq => 2 | M.locker2_check_available => 2 | M.locker2_check_availables => 2 | M.locker2_claim_lock => 3 | M.locker2_map_add_pending => 3 | M.locker2_map_claim_lock => 3 | M.locker2_map_promote_pending => 2 | M.locker2_obtainable => 2 | M.locker2_obtainables => 2 | M.locker2_promote_pending => 2 | M.locker2_release_lock => 2 | M.locker2_remove_pending => 2 | M.mcrlrecord => 0 | M.member => 2 | M.nil => 0 | M.nocalls => 0 | M.not => 1 | M.ok => 0 | M.or => 2 | M.pending => 0 | M.pid => 1 | M.pops => 1 | M.push => 3 | M.push1 => 6 | M.pushs => 2 | M.record_extract => 3 | M.record_new => 1 | M.record_update => 4 | M.record_updates => 3 | M.release => 0 | M.request => 0 | M.resource => 0 | M.s => 1 | M.stack => 2 | M.subtract => 2 | M.tag => 0 | M.tops => 1 | M.true => 0 | M.tuple => 2 | M.tuplenil => 1 | M.undefined => 0 end. Definition s0 := ASignature.mkSignature ar eq_symb_dec. Definition s0_p := s0. Definition V0 := @ATerm.Var s0. Definition F0 := @ATerm.Fun s0. Definition R0 := @ATrs.mkRule s0. Module S0. Definition F := F0 M.F Vnil. Definition T := F0 M.T Vnil. Definition _0_1 := F0 M._0_1 Vnil. Definition _if_2 x3 x2 x1 := F0 M._if_2 (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition a := F0 M.a Vnil. Definition and x2 x1 := F0 M.and (Vcons x2 (Vcons x1 Vnil)). Definition andt x2 x1 := F0 M.andt (Vcons x2 (Vcons x1 Vnil)). Definition append x2 x1 := F0 M.append (Vcons x2 (Vcons x1 Vnil)). Definition calls x3 x2 x1 := F0 M.calls (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition case0 x3 x2 x1 := F0 M.case0 (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition case1 x4 x3 x2 x1 := F0 M.case1 (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil)))). Definition case2 x3 x2 x1 := F0 M.case2 (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition case4 x3 x2 x1 := F0 M.case4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition case5 x4 x3 x2 x1 := F0 M.case5 (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil)))). Definition case6 x4 x3 x2 x1 := F0 M.case6 (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil)))). Definition case8 x4 x3 x2 x1 := F0 M.case8 (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil)))). Definition case9 x4 x3 x2 x1 := F0 M.case9 (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil)))). Definition cons x2 x1 := F0 M.cons (Vcons x2 (Vcons x1 Vnil)). Definition delete x2 x1 := F0 M.delete (Vcons x2 (Vcons x1 Vnil)). Definition element x2 x1 := F0 M.element (Vcons x2 (Vcons x1 Vnil)). Definition empty := F0 M.empty Vnil. Definition eq x2 x1 := F0 M.eq (Vcons x2 (Vcons x1 Vnil)). Definition eqc x2 x1 := F0 M.eqc (Vcons x2 (Vcons x1 Vnil)). Definition eqs x2 x1 := F0 M.eqs (Vcons x2 (Vcons x1 Vnil)). Definition eqt x2 x1 := F0 M.eqt (Vcons x2 (Vcons x1 Vnil)). Definition equal x2 x1 := F0 M.equal (Vcons x2 (Vcons x1 Vnil)). Definition excl := F0 M.excl Vnil. Definition excllock := F0 M.excllock Vnil. Definition false := F0 M.false Vnil. Definition gen_modtageq x2 x1 := F0 M.gen_modtageq (Vcons x2 (Vcons x1 Vnil)). Definition gen_tag x1 := F0 M.gen_tag (Vcons x1 Vnil). Definition imp x2 x1 := F0 M.imp (Vcons x2 (Vcons x1 Vnil)). Definition int x1 := F0 M.int (Vcons x1 Vnil). Definition istops x2 x1 := F0 M.istops (Vcons x2 (Vcons x1 Vnil)). Definition lock := F0 M.lock Vnil. Definition locker := F0 M.locker Vnil. Definition locker2_add_pending x3 x2 x1 := F0 M.locker2_add_pending (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition locker2_adduniq x2 x1 := F0 M.locker2_adduniq (Vcons x2 (Vcons x1 Vnil)). Definition locker2_check_available x2 x1 := F0 M.locker2_check_available (Vcons x2 (Vcons x1 Vnil)). Definition locker2_check_availables x2 x1 := F0 M.locker2_check_availables (Vcons x2 (Vcons x1 Vnil)). Definition locker2_claim_lock x3 x2 x1 := F0 M.locker2_claim_lock (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition locker2_map_add_pending x3 x2 x1 := F0 M.locker2_map_add_pending (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition locker2_map_claim_lock x3 x2 x1 := F0 M.locker2_map_claim_lock (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition locker2_map_promote_pending x2 x1 := F0 M.locker2_map_promote_pending (Vcons x2 (Vcons x1 Vnil)). Definition locker2_obtainable x2 x1 := F0 M.locker2_obtainable (Vcons x2 (Vcons x1 Vnil)). Definition locker2_obtainables x2 x1 := F0 M.locker2_obtainables (Vcons x2 (Vcons x1 Vnil)). Definition locker2_promote_pending x2 x1 := F0 M.locker2_promote_pending (Vcons x2 (Vcons x1 Vnil)). Definition locker2_release_lock x2 x1 := F0 M.locker2_release_lock (Vcons x2 (Vcons x1 Vnil)). Definition locker2_remove_pending x2 x1 := F0 M.locker2_remove_pending (Vcons x2 (Vcons x1 Vnil)). Definition mcrlrecord := F0 M.mcrlrecord Vnil. Definition member x2 x1 := F0 M.member (Vcons x2 (Vcons x1 Vnil)). Definition nil := F0 M.nil Vnil. Definition nocalls := F0 M.nocalls Vnil. Definition not x1 := F0 M.not (Vcons x1 Vnil). Definition ok := F0 M.ok Vnil. Definition or x2 x1 := F0 M.or (Vcons x2 (Vcons x1 Vnil)). Definition pending := F0 M.pending Vnil. Definition pid x1 := F0 M.pid (Vcons x1 Vnil). Definition pops x1 := F0 M.pops (Vcons x1 Vnil). Definition push x3 x2 x1 := F0 M.push (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition push1 x6 x5 x4 x3 x2 x1 := F0 M.push1 (Vcons x6 (Vcons x5 (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil)))))). Definition pushs x2 x1 := F0 M.pushs (Vcons x2 (Vcons x1 Vnil)). Definition record_extract x3 x2 x1 := F0 M.record_extract (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition record_new x1 := F0 M.record_new (Vcons x1 Vnil). Definition record_update x4 x3 x2 x1 := F0 M.record_update (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil)))). Definition record_updates x3 x2 x1 := F0 M.record_updates (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition release := F0 M.release Vnil. Definition request := F0 M.request Vnil. Definition resource := F0 M.resource Vnil. Definition s x1 := F0 M.s (Vcons x1 Vnil). Definition stack x2 x1 := F0 M.stack (Vcons x2 (Vcons x1 Vnil)). Definition subtract x2 x1 := F0 M.subtract (Vcons x2 (Vcons x1 Vnil)). Definition tag := F0 M.tag Vnil. Definition tops x1 := F0 M.tops (Vcons x1 Vnil). Definition true := F0 M.true Vnil. Definition tuple x2 x1 := F0 M.tuple (Vcons x2 (Vcons x1 Vnil)). Definition tuplenil x1 := F0 M.tuplenil (Vcons x1 Vnil). Definition undefined := F0 M.undefined Vnil. End S0. Definition E := @nil (@ATrs.rule s0). Definition R := R0 (S0.or S0.T S0.T) S0.T :: R0 (S0.or S0.F S0.T) S0.T :: R0 (S0.or S0.T S0.F) S0.T :: R0 (S0.or S0.F S0.F) S0.F :: R0 (S0.and S0.T (V0 0)) (V0 0) :: R0 (S0.and (V0 0) S0.T) (V0 0) :: R0 (S0.and S0.F (V0 0)) S0.F :: R0 (S0.and (V0 0) S0.F) S0.F :: R0 (S0.imp S0.T (V0 0)) (V0 0) :: R0 (S0.imp S0.F (V0 0)) S0.T :: R0 (S0.not S0.T) S0.F :: R0 (S0.not S0.F) S0.T :: R0 (S0._if_2 S0.T (V0 0) (V0 1)) (V0 0) :: R0 (S0._if_2 S0.F (V0 0) (V0 1)) (V0 1) :: R0 (S0.eq S0.T S0.T) S0.T :: R0 (S0.eq S0.F S0.F) S0.T :: R0 (S0.eq S0.T S0.F) S0.F :: R0 (S0.eq S0.F S0.T) S0.F :: R0 (S0.eqt S0.nil S0.undefined) S0.F :: R0 (S0.eqt S0.nil (S0.pid (V0 0))) S0.F :: R0 (S0.eqt S0.nil (S0.int (V0 0))) S0.F :: R0 (S0.eqt S0.nil (S0.cons (V0 0) (V0 1))) S0.F :: R0 (S0.eqt S0.nil (S0.tuple (V0 0) (V0 1))) S0.F :: R0 (S0.eqt S0.nil (S0.tuplenil (V0 0))) S0.F :: R0 (S0.eqt S0.a S0.nil) S0.F :: R0 (S0.eqt S0.a S0.a) S0.T :: R0 (S0.eqt S0.a S0.excl) S0.F :: R0 (S0.eqt S0.a S0.false) S0.F :: R0 (S0.eqt S0.a S0.lock) S0.F :: R0 (S0.eqt S0.a S0.locker) S0.F :: R0 (S0.eqt S0.a S0.mcrlrecord) S0.F :: R0 (S0.eqt S0.a S0.ok) S0.F :: R0 (S0.eqt S0.a S0.pending) S0.F :: R0 (S0.eqt S0.a S0.release) S0.F :: R0 (S0.eqt S0.a S0.request) S0.F :: R0 (S0.eqt S0.a S0.resource) S0.F :: R0 (S0.eqt S0.a S0.tag) S0.F :: R0 (S0.eqt S0.a S0.true) S0.F :: R0 (S0.eqt S0.a S0.undefined) S0.F :: R0 (S0.eqt S0.a (S0.pid (V0 0))) S0.F :: R0 (S0.eqt S0.a (S0.int (V0 0))) S0.F :: R0 (S0.eqt S0.a (S0.cons (V0 0) (V0 1))) S0.F :: R0 (S0.eqt S0.a (S0.tuple (V0 0) (V0 1))) S0.F :: R0 (S0.eqt S0.a (S0.tuplenil (V0 0))) S0.F :: R0 (S0.eqt S0.excl S0.nil) S0.F :: R0 (S0.eqt S0.excl S0.a) S0.F :: R0 (S0.eqt S0.excl S0.excl) S0.T :: R0 (S0.eqt S0.excl S0.false) S0.F :: R0 (S0.eqt S0.excl S0.lock) S0.F :: R0 (S0.eqt S0.excl S0.locker) S0.F :: R0 (S0.eqt S0.excl S0.mcrlrecord) S0.F :: R0 (S0.eqt S0.excl S0.ok) S0.F :: R0 (S0.eqt S0.excl S0.pending) S0.F :: R0 (S0.eqt S0.excl S0.release) S0.F :: R0 (S0.eqt S0.excl S0.request) S0.F :: R0 (S0.eqt S0.excl S0.resource) S0.F :: R0 (S0.eqt S0.excl S0.tag) S0.F :: R0 (S0.eqt S0.excl S0.true) S0.F :: R0 (S0.eqt S0.excl S0.undefined) S0.F :: R0 (S0.eqt S0.excl (S0.pid (V0 0))) S0.F :: R0 (S0.eqt S0.excl (S0.eqt S0.false (S0.int (V0 0)))) S0.F :: R0 (S0.eqt S0.false (S0.cons (V0 0) (V0 1))) S0.F :: R0 (S0.eqt S0.false (S0.tuple (V0 0) (V0 1))) S0.F :: R0 (S0.eqt S0.false (S0.tuplenil (V0 0))) S0.F :: R0 (S0.eqt S0.lock S0.nil) S0.F :: R0 (S0.eqt S0.lock S0.a) S0.F :: R0 (S0.eqt S0.lock S0.excl) S0.F :: R0 (S0.eqt S0.lock S0.false) S0.F :: R0 (S0.eqt S0.lock S0.lock) S0.T :: R0 (S0.eqt S0.lock S0.locker) S0.F :: R0 (S0.eqt S0.lock S0.mcrlrecord) S0.F :: R0 (S0.eqt S0.lock S0.ok) S0.F :: R0 (S0.eqt S0.lock S0.pending) S0.F :: R0 (S0.eqt S0.lock S0.release) S0.F :: R0 (S0.eqt S0.lock S0.request) S0.F :: R0 (S0.eqt S0.lock S0.resource) S0.F :: R0 (S0.eqt S0.lock S0.tag) S0.F :: R0 (S0.eqt S0.lock S0.true) S0.F :: R0 (S0.eqt S0.lock S0.undefined) S0.F :: R0 (S0.eqt S0.lock (S0.pid (V0 0))) S0.F :: R0 (S0.eqt S0.lock (S0.int (V0 0))) S0.F :: R0 (S0.eqt S0.lock (S0.cons (V0 0) (V0 1))) S0.F :: R0 (S0.eqt S0.lock (S0.tuple (V0 0) (V0 1))) S0.F :: R0 (S0.eqt S0.lock (S0.tuplenil (V0 0))) S0.F :: R0 (S0.eqt S0.locker S0.nil) S0.F :: R0 (S0.eqt S0.locker S0.a) S0.F :: R0 (S0.eqt S0.locker S0.excl) S0.F :: R0 (S0.eqt S0.locker S0.false) S0.F :: R0 (S0.eqt S0.locker S0.lock) S0.F :: R0 (S0.eqt S0.locker S0.locker) S0.T :: R0 (S0.eqt S0.locker S0.mcrlrecord) S0.F :: R0 (S0.eqt S0.locker S0.ok) S0.F :: R0 (S0.eqt S0.locker S0.pending) S0.F :: R0 (S0.eqt S0.locker S0.release) S0.F :: R0 (S0.eqt S0.locker S0.request) S0.F :: R0 (S0.eqt S0.locker S0.resource) S0.F :: R0 (S0.eqt S0.locker S0.tag) S0.F :: R0 (S0.eqt S0.locker S0.true) S0.F :: R0 (S0.eqt S0.locker S0.undefined) S0.F :: R0 (S0.eqt S0.locker (S0.pid (V0 0))) S0.F :: R0 (S0.eqt S0.locker (S0.int (V0 0))) S0.F :: R0 (S0.eqt S0.locker (S0.cons (V0 0) (V0 1))) S0.F :: R0 (S0.eqt S0.locker (S0.tuple (V0 0) (V0 1))) S0.F :: R0 (S0.eqt S0.locker (S0.tuplenil (V0 0))) S0.F :: R0 (S0.eqt S0.mcrlrecord S0.nil) S0.F :: R0 (S0.eqt S0.mcrlrecord S0.a) S0.F :: R0 (S0.eqt S0.mcrlrecord S0.excl) S0.F :: R0 (S0.eqt S0.mcrlrecord S0.false) S0.F :: R0 (S0.eqt S0.mcrlrecord S0.lock) S0.F :: R0 (S0.eqt S0.mcrlrecord S0.locker) S0.F :: R0 (S0.eqt S0.mcrlrecord S0.mcrlrecord) S0.T :: R0 (S0.eqt S0.mcrlrecord S0.ok) S0.F :: R0 (S0.eqt S0.mcrlrecord S0.pending) S0.F :: R0 (S0.eqt S0.mcrlrecord S0.release) S0.F :: R0 (S0.eqt S0.mcrlrecord S0.request) S0.F :: R0 (S0.eqt S0.mcrlrecord S0.resource) S0.F :: R0 (S0.eqt S0.ok S0.resource) S0.F :: R0 (S0.eqt S0.ok S0.tag) S0.F :: R0 (S0.eqt S0.ok S0.true) S0.F :: R0 (S0.eqt S0.ok S0.undefined) S0.F :: R0 (S0.eqt S0.ok (S0.pid (V0 0))) S0.F :: R0 (S0.eqt S0.ok (S0.int (V0 0))) S0.F :: R0 (S0.eqt S0.ok (S0.cons (V0 0) (V0 1))) S0.F :: R0 (S0.eqt S0.ok (S0.tuple (V0 0) (V0 1))) S0.F :: R0 (S0.eqt S0.ok (S0.tuplenil (V0 0))) S0.F :: R0 (S0.eqt S0.pending S0.nil) S0.F :: R0 (S0.eqt S0.pending S0.a) S0.F :: R0 (S0.eqt S0.pending S0.excl) S0.F :: R0 (S0.eqt S0.pending S0.false) S0.F :: R0 (S0.eqt S0.pending S0.lock) S0.F :: R0 (S0.eqt S0.pending S0.locker) S0.F :: R0 (S0.eqt S0.pending S0.mcrlrecord) S0.F :: R0 (S0.eqt S0.pending S0.ok) S0.F :: R0 (S0.eqt S0.pending S0.pending) S0.T :: R0 (S0.eqt S0.pending S0.release) S0.F :: R0 (S0.eqt S0.pending S0.request) S0.F :: R0 (S0.eqt S0.pending S0.resource) S0.F :: R0 (S0.eqt S0.pending S0.tag) S0.F :: R0 (S0.eqt S0.pending S0.true) S0.F :: R0 (S0.eqt S0.pending S0.undefined) S0.F :: R0 (S0.eqt S0.pending (S0.pid (V0 0))) S0.F :: R0 (S0.eqt S0.pending (S0.int (V0 0))) S0.F :: R0 (S0.eqt S0.pending (S0.cons (V0 0) (V0 1))) S0.F :: R0 (S0.eqt S0.pending (S0.tuple (V0 0) (V0 1))) S0.F :: R0 (S0.eqt S0.pending (S0.tuplenil (V0 0))) S0.F :: R0 (S0.eqt S0.release S0.nil) S0.F :: R0 (S0.eqt S0.release S0.a) S0.F :: R0 (S0.eqt S0.release S0.excl) S0.F :: R0 (S0.eqt S0.release S0.false) S0.F :: R0 (S0.eqt S0.release S0.lock) S0.F :: R0 (S0.eqt S0.release S0.locker) S0.F :: R0 (S0.eqt S0.release S0.mcrlrecord) S0.F :: R0 (S0.eqt S0.release S0.ok) S0.F :: R0 (S0.eqt S0.request S0.mcrlrecord) S0.F :: R0 (S0.eqt S0.request S0.ok) S0.F :: R0 (S0.eqt S0.request S0.pending) S0.F :: R0 (S0.eqt S0.request S0.release) S0.F :: R0 (S0.eqt S0.request S0.request) S0.T :: R0 (S0.eqt S0.request S0.resource) S0.F :: R0 (S0.eqt S0.request S0.tag) S0.F :: R0 (S0.eqt S0.request S0.true) S0.F :: R0 (S0.eqt S0.request S0.undefined) S0.F :: R0 (S0.eqt S0.request (S0.pid (V0 0))) S0.F :: R0 (S0.eqt S0.request (S0.int (V0 0))) S0.F :: R0 (S0.eqt S0.request (S0.cons (V0 0) (V0 1))) S0.F :: R0 (S0.eqt S0.request (S0.tuple (V0 0) (V0 1))) S0.F :: R0 (S0.eqt S0.request (S0.tuplenil (V0 0))) S0.F :: R0 (S0.eqt S0.resource S0.nil) S0.F :: R0 (S0.eqt S0.resource S0.a) S0.F :: R0 (S0.eqt S0.resource S0.excl) S0.F :: R0 (S0.eqt S0.resource S0.false) S0.F :: R0 (S0.eqt S0.resource S0.lock) S0.F :: R0 (S0.eqt S0.resource S0.locker) S0.F :: R0 (S0.eqt S0.resource S0.mcrlrecord) S0.F :: R0 (S0.eqt S0.resource S0.ok) S0.F :: R0 (S0.eqt S0.resource S0.pending) S0.F :: R0 (S0.eqt S0.resource S0.release) S0.F :: R0 (S0.eqt S0.resource S0.request) S0.F :: R0 (S0.eqt S0.resource S0.resource) S0.T :: R0 (S0.eqt S0.resource S0.tag) S0.F :: R0 (S0.eqt S0.resource S0.true) S0.F :: R0 (S0.eqt S0.resource S0.undefined) S0.F :: R0 (S0.eqt S0.resource (S0.pid (V0 0))) S0.F :: R0 (S0.eqt S0.resource (S0.int (V0 0))) S0.F :: R0 (S0.eqt S0.resource (S0.cons (V0 0) (V0 1))) S0.F :: R0 (S0.eqt S0.resource (S0.tuple (V0 0) (V0 1))) S0.F :: R0 (S0.eqt S0.resource (S0.tuplenil (V0 0))) S0.F :: R0 (S0.eqt S0.tag S0.nil) S0.F :: R0 (S0.eqt S0.tag S0.a) S0.F :: R0 (S0.eqt S0.tag S0.excl) S0.F :: R0 (S0.eqt S0.tag S0.false) S0.F :: R0 (S0.eqt S0.tag S0.lock) S0.F :: R0 (S0.eqt S0.tag S0.locker) S0.F :: R0 (S0.eqt S0.tag S0.mcrlrecord) S0.F :: R0 (S0.eqt S0.tag S0.ok) S0.F :: R0 (S0.eqt S0.tag S0.pending) S0.F :: R0 (S0.eqt S0.tag S0.release) S0.F :: R0 (S0.eqt S0.tag S0.request) S0.F :: R0 (S0.eqt S0.tag S0.resource) S0.F :: R0 (S0.eqt S0.tag S0.tag) S0.T :: R0 (S0.eqt S0.tag S0.true) S0.F :: R0 (S0.eqt S0.tag S0.undefined) S0.F :: R0 (S0.eqt S0.tag (S0.pid (V0 0))) S0.F :: R0 (S0.eqt S0.tag (S0.int (V0 0))) S0.F :: R0 (S0.eqt S0.tag (S0.cons (V0 0) (V0 1))) S0.F :: R0 (S0.eqt S0.tag (S0.tuple (V0 0) (V0 1))) S0.F :: R0 (S0.eqt S0.tag (S0.tuplenil (V0 0))) S0.F :: R0 (S0.eqt S0.true S0.nil) S0.F :: R0 (S0.eqt S0.true S0.a) S0.F :: R0 (S0.eqt S0.true S0.excl) S0.F :: R0 (S0.eqt S0.true S0.false) S0.F :: R0 (S0.eqt S0.true S0.lock) S0.F :: R0 (S0.eqt S0.true S0.locker) S0.F :: R0 (S0.eqt S0.true S0.mcrlrecord) S0.F :: R0 (S0.eqt S0.true S0.ok) S0.F :: R0 (S0.eqt S0.true S0.pending) S0.F :: R0 (S0.eqt S0.true S0.release) S0.F :: R0 (S0.eqt S0.true S0.request) S0.F :: R0 (S0.eqt S0.true S0.resource) S0.F :: R0 (S0.eqt S0.true S0.tag) S0.F :: R0 (S0.eqt S0.true S0.true) S0.T :: R0 (S0.eqt S0.true S0.undefined) S0.F :: R0 (S0.eqt S0.true (S0.pid (V0 0))) S0.F :: R0 (S0.eqt S0.true (S0.int (V0 0))) S0.F :: R0 (S0.eqt S0.true (S0.cons (V0 0) (V0 1))) S0.F :: R0 (S0.eqt S0.true (S0.tuple (V0 0) (V0 1))) S0.F :: R0 (S0.eqt S0.true (S0.tuplenil (V0 0))) S0.F :: R0 (S0.eqt S0.undefined S0.nil) S0.F :: R0 (S0.eqt S0.undefined S0.a) S0.F :: R0 (S0.eqt S0.undefined (S0.tuplenil (V0 0))) S0.F :: R0 (S0.eqt (S0.pid (V0 0)) S0.nil) S0.F :: R0 (S0.eqt (S0.pid (V0 0)) S0.a) S0.F :: R0 (S0.eqt (S0.pid (V0 0)) S0.excl) S0.F :: R0 (S0.eqt (S0.pid (V0 0)) S0.false) S0.F :: R0 (S0.eqt (S0.pid (V0 0)) S0.lock) S0.F :: R0 (S0.eqt (S0.pid (V0 0)) S0.locker) S0.F :: R0 (S0.eqt (S0.pid (V0 0)) S0.mcrlrecord) S0.F :: R0 (S0.eqt (S0.pid (V0 0)) S0.ok) S0.F :: R0 (S0.eqt (S0.pid (V0 0)) S0.pending) S0.F :: R0 (S0.eqt (S0.pid (V0 0)) S0.release) S0.F :: R0 (S0.eqt (S0.pid (V0 0)) S0.request) S0.F :: R0 (S0.eqt (S0.pid (V0 0)) S0.resource) S0.F :: R0 (S0.eqt (S0.pid (V0 0)) S0.tag) S0.F :: R0 (S0.eqt (S0.pid (V0 0)) S0.true) S0.F :: R0 (S0.eqt (S0.pid (V0 0)) S0.undefined) S0.F :: R0 (S0.eqt (S0.pid (V0 0)) (S0.pid (V0 1))) (S0.eqt (V0 0) (V0 1)) :: R0 (S0.eqt (S0.pid (V0 0)) (S0.int (V0 1))) S0.F :: R0 (S0.eqt (S0.pid (V0 0)) (S0.cons (V0 1) (V0 2))) S0.F :: R0 (S0.eqt (S0.pid (V0 0)) (S0.tuple (V0 1) (V0 2))) S0.F :: R0 (S0.eqt (S0.pid (V0 0)) (S0.tuplenil (V0 1))) S0.F :: R0 (S0.eqt (S0.int (V0 0)) S0.nil) S0.F :: R0 (S0.eqt (S0.int (V0 0)) S0.a) S0.F :: R0 (S0.eqt (S0.int (V0 0)) S0.excl) S0.F :: R0 (S0.eqt (S0.int (V0 0)) S0.false) S0.F :: R0 (S0.eqt (S0.int (V0 0)) S0.lock) S0.F :: R0 (S0.eqt (S0.int (V0 0)) S0.locker) S0.F :: R0 (S0.eqt (S0.int (V0 0)) S0.mcrlrecord) S0.F :: R0 (S0.eqt (S0.int (V0 0)) S0.ok) S0.F :: R0 (S0.eqt (S0.int (V0 0)) S0.pending) S0.F :: R0 (S0.eqt (S0.int (V0 0)) S0.release) S0.F :: R0 (S0.eqt (S0.int (V0 0)) S0.request) S0.F :: R0 (S0.eqt (S0.int (V0 0)) S0.resource) S0.F :: R0 (S0.eqt (S0.int (V0 0)) S0.tag) S0.F :: R0 (S0.eqt (S0.int (V0 0)) S0.true) S0.F :: R0 (S0.eqt (S0.int (V0 0)) S0.undefined) S0.F :: R0 (S0.eqt (S0.cons (V0 0) (V0 1)) S0.resource) S0.F :: R0 (S0.eqt (S0.cons (V0 0) (V0 1)) S0.tag) S0.F :: R0 (S0.eqt (S0.cons (V0 0) (V0 1)) S0.true) S0.F :: R0 (S0.eqt (S0.cons (V0 0) (V0 1)) S0.undefined) S0.F :: R0 (S0.eqt (S0.cons (V0 0) (V0 1)) (S0.pid (V0 2))) S0.F :: R0 (S0.eqt (S0.cons (V0 0) (V0 1)) (S0.int (V0 2))) S0.F :: R0 (S0.eqt (S0.cons (V0 0) (V0 1)) (S0.cons (V0 2) (V0 3))) (S0.and (S0.eqt (V0 0) (V0 2)) (S0.eqt (V0 1) (V0 3))) :: R0 (S0.eqt (S0.cons (V0 0) (V0 1)) (S0.tuple (V0 2) (V0 3))) S0.F :: R0 (S0.eqt (S0.cons (V0 0) (V0 1)) (S0.tuplenil (V0 2))) S0.F :: R0 (S0.eqt (S0.tuple (V0 0) (V0 1)) S0.nil) S0.F :: R0 (S0.eqt (S0.tuple (V0 0) (V0 1)) S0.a) S0.F :: R0 (S0.eqt (S0.tuple (V0 0) (V0 1)) S0.excl) S0.F :: R0 (S0.eqt (S0.tuple (V0 0) (V0 1)) S0.false) S0.F :: R0 (S0.eqt (S0.tuple (V0 0) (V0 1)) S0.lock) S0.F :: R0 (S0.eqt (S0.tuple (V0 0) (V0 1)) S0.locker) S0.F :: R0 (S0.eqt (S0.tuple (V0 0) (V0 1)) S0.mcrlrecord) S0.F :: R0 (S0.eqt (S0.tuple (V0 0) (V0 1)) S0.ok) S0.F :: R0 (S0.eqt (S0.tuple (V0 0) (V0 1)) S0.pending) S0.F :: R0 (S0.eqt (S0.tuple (V0 0) (V0 1)) S0.release) S0.F :: R0 (S0.eqt (S0.tuple (V0 0) (V0 1)) S0.request) S0.F :: R0 (S0.eqt (S0.tuple (V0 0) (V0 1)) S0.resource) S0.F :: R0 (S0.eqt (S0.tuple (V0 0) (V0 1)) S0.tag) S0.F :: R0 (S0.eqt (S0.tuple (V0 0) (V0 1)) S0.true) S0.F :: R0 (S0.eqt (S0.tuple (V0 0) (V0 1)) S0.undefined) S0.F :: R0 (S0.eqt (S0.tuple (V0 0) (V0 1)) (S0.pid (V0 2))) S0.F :: R0 (S0.eqt (S0.tuple (V0 0) (V0 1)) (S0.int (V0 2))) S0.F :: R0 (S0.eqt (S0.tuple (V0 0) (V0 1)) (S0.cons (V0 2) (V0 3))) S0.F :: R0 (S0.eqt (S0.tuple (V0 0) (V0 1)) (S0.tuple (V0 2) (V0 3))) (S0.and (S0.eqt (V0 0) (V0 2)) (S0.eqt (V0 1) (V0 3))) :: R0 (S0.eqt (S0.tuple (V0 0) (V0 1)) (S0.tuplenil (V0 2))) S0.F :: R0 (S0.eqt (S0.tuplenil (V0 0)) S0.nil) S0.F :: R0 (S0.eqt (S0.tuplenil (V0 0)) S0.a) S0.F :: R0 (S0.eqt (S0.tuplenil (V0 0)) S0.excl) S0.F :: R0 (S0.eqt (S0.tuplenil (V0 0)) S0.false) S0.F :: R0 (S0.eqt (S0.tuplenil (V0 0)) S0.lock) S0.F :: R0 (S0.eqt (S0.tuplenil (V0 0)) S0.locker) S0.F :: R0 (S0.eqt (S0.tuplenil (V0 0)) S0.mcrlrecord) S0.F :: R0 (S0.eqt (S0.tuplenil (V0 0)) S0.ok) S0.F :: R0 (S0.eqt (S0.tuplenil (V0 0)) S0.pending) S0.F :: R0 (S0.eqt (S0.tuplenil (V0 0)) S0.release) S0.F :: R0 (S0.eqt (S0.tuplenil (V0 0)) S0.request) S0.F :: R0 (S0.eqt (S0.tuplenil (V0 0)) S0.resource) S0.F :: R0 (S0.eqt (S0.tuplenil (V0 0)) S0.tag) S0.F :: R0 (S0.eqt (S0.tuplenil (V0 0)) S0.true) S0.F :: R0 (S0.eqt (S0.tuplenil (V0 0)) S0.undefined) S0.F :: R0 (S0.eqt (S0.tuplenil (V0 0)) (S0.pid (V0 1))) S0.F :: R0 (S0.eqt (S0.tuplenil (V0 0)) (S0.int (V0 1))) S0.F :: R0 (S0.eqt (S0.tuplenil (V0 0)) (S0.cons (V0 1) (V0 2))) S0.F :: R0 (S0.eqt (S0.tuplenil (V0 0)) (S0.tuple (V0 1) (V0 2))) S0.F :: R0 (S0.eqt (S0.tuplenil (V0 0)) (S0.tuplenil (V0 1))) (S0.eqt (V0 0) (V0 1)) :: R0 (S0.element (S0.int (S0.s S0._0_1)) (S0.tuplenil (V0 0))) (V0 0) :: R0 (S0.element (S0.int (S0.s S0._0_1)) (S0.tuple (V0 0) (V0 1))) (V0 0) :: R0 (S0.element (S0.int (S0.s (S0.s (V0 0)))) (S0.tuple (V0 1) (V0 2))) (S0.element (S0.int (S0.s (V0 0))) (V0 2)) :: R0 (S0.record_new S0.lock) (S0.tuple S0.mcrlrecord (S0.tuple S0.lock (S0.tuple S0.undefined (S0.tuple S0.nil (S0.tuplenil S0.nil))))) :: R0 (S0.record_extract (S0.tuple S0.mcrlrecord (S0.tuple S0.lock (S0.tuple (V0 0) (S0.tuple (V0 1) (S0.tuplenil (V0 2)))))) S0.lock S0.resource) (S0.tuple S0.mcrlrecord (S0.tuple S0.lock (S0.tuple (V0 0) (S0.tuple (V0 1) (S0.tuplenil (V0 2)))))) :: R0 (S0.record_update (S0.tuple S0.mcrlrecord (S0.tuple S0.lock (S0.tuple (V0 0) (S0.tuple (V0 1) (S0.tuplenil (V0 2)))))) S0.lock S0.pending (V0 3)) (S0.tuple S0.mcrlrecord (S0.tuple S0.lock (S0.tuple (V0 0) (S0.tuple (V0 1) (S0.tuplenil (V0 3)))))) :: R0 (S0.record_updates (V0 0) (V0 1) S0.nil) (V0 0) :: R0 (S0.record_updates (V0 0) (V0 1) (S0.cons (S0.tuple (V0 2) (S0.tuplenil (V0 3))) (V0 4))) (S0.record_updates (S0.record_update (V0 0) (V0 1) (V0 2) (V0 3)) (V0 1) (V0 4)) :: R0 (S0.locker2_map_promote_pending S0.nil (V0 0)) S0.nil :: R0 (S0.locker2_map_promote_pending (S0.cons (V0 0) (V0 1)) (V0 2)) (S0.cons (S0.locker2_promote_pending (V0 0) (V0 2)) (S0.locker2_map_promote_pending (V0 1) (V0 2))) :: R0 (S0.locker2_map_claim_lock S0.nil (V0 0) (V0 1)) S0.nil :: R0 (S0.locker2_map_claim_lock (S0.cons (V0 0) (V0 1)) (V0 2) (V0 3)) (S0.cons (S0.locker2_claim_lock (V0 0) (V0 2) (V0 3)) (S0.locker2_map_claim_lock (V0 1) (V0 2) (V0 3))) :: R0 (S0.locker2_map_add_pending S0.nil (V0 0) (V0 1)) S0.nil :: R0 (S0.locker2_promote_pending (V0 0) (V0 1)) (S0.case0 (V0 1) (V0 0) (S0.record_extract (V0 0) S0.lock S0.pending)) :: R0 (S0.case0 (V0 0) (V0 1) (S0.cons (V0 0) (V0 3))) (S0.record_updates (V0 1) S0.lock (S0.cons (S0.tuple S0.excl (S0.tuplenil (V0 0))) (S0.cons (S0.tuple S0.pending (S0.tuplenil (V0 3))) S0.nil))) :: R0 (S0.case0 (V0 0) (V0 1) (V0 2)) (V0 1) :: R0 (S0.locker2_remove_pending (V0 0) (V0 1)) (S0.record_updates (V0 0) S0.lock (S0.cons (S0.tuple S0.pending (S0.tuplenil (S0.subtract (S0.record_extract (V0 0) S0.lock S0.pending) (S0.cons (V0 1) S0.nil)))) S0.nil)) :: R0 (S0.locker2_add_pending (V0 0) (V0 1) (V0 2)) (S0.case1 (V0 2) (V0 1) (V0 0) (S0.member (S0.record_extract (V0 0) S0.lock S0.resource) (V0 1))) :: R0 (S0.case1 (V0 0) (V0 1) (V0 2) S0.true) (S0.record_updates (V0 2) S0.lock (S0.cons (S0.tuple S0.pending (S0.tuplenil (S0.append (S0.record_extract (V0 2) S0.lock S0.pending) (S0.cons (V0 0) S0.nil)))) S0.nil)) :: R0 (S0.case1 (V0 0) (V0 1) (V0 2) S0.false) (V0 2) :: R0 (S0.locker2_release_lock (V0 0) (V0 1)) (S0.case2 (V0 1) (V0 0) (S0.gen_modtageq (V0 1) (S0.record_extract (V0 0) S0.lock S0.excl))) :: R0 (S0.case2 (V0 0) (V0 1) S0.true) (S0.record_updates (V0 1) S0.lock (S0.cons (S0.tuple S0.excllock S0.excl) S0.nil)) :: R0 (S0.case4 (V0 0) (V0 1) (V0 2)) S0.false :: R0 (S0.locker2_obtainables S0.nil (V0 0)) S0.true :: R0 (S0.locker2_obtainables (S0.cons (V0 0) (V0 1)) (V0 2)) (S0.case5 (V0 2) (V0 1) (V0 0) (S0.member (V0 2) (S0.record_extract (V0 0) S0.lock S0.pending))) :: R0 (S0.case5 (V0 0) (V0 1) (V0 2) S0.true) (S0.andt (S0.locker2_obtainable (V0 2) (V0 0)) (S0.locker2_obtainables (V0 1) (V0 0))) :: R0 (S0.case5 (V0 0) (V0 1) (V0 2) S0.false) (S0.locker2_obtainables (V0 1) (V0 0)) :: R0 (S0.locker2_check_available (V0 0) S0.nil) S0.false :: R0 (S0.locker2_check_available (V0 0) (S0.cons (V0 1) (V0 2))) (S0.case6 (V0 2) (V0 1) (V0 0) (S0.equal (V0 0) (S0.record_extract (V0 1) S0.lock S0.resource))) :: R0 (S0.case6 (V0 0) (V0 1) (V0 2) S0.true) (S0.andt (S0.equal (S0.record_extract (V0 1) S0.lock S0.excl) S0.nil) (S0.equal (S0.record_extract (V0 1) S0.lock S0.pending) S0.nil)) :: R0 (S0.case6 (V0 0) (V0 1) (V0 2) S0.false) (S0.locker2_check_available (V0 2) (V0 0)) :: R0 (S0.locker2_check_availables S0.nil (V0 0)) S0.true :: R0 (S0.locker2_check_availables (S0.cons (V0 0) (V0 1)) (V0 2)) (S0.andt (S0.locker2_check_available (V0 0) (V0 2)) (S0.locker2_check_availables (V0 1) (V0 2))) :: R0 (S0.locker2_adduniq S0.nil (V0 0)) (V0 0) :: R0 (S0.append (S0.cons (V0 0) (V0 1)) (V0 2)) (S0.cons (V0 0) (S0.append (V0 1) (V0 2))) :: R0 (S0.subtract (V0 0) S0.nil) (V0 0) :: R0 (S0.subtract (V0 0) (S0.cons (V0 1) (V0 2))) (S0.subtract (S0.delete (V0 1) (V0 0)) (V0 2)) :: R0 (S0.delete (V0 0) S0.nil) S0.nil :: R0 (S0.delete (V0 0) (S0.cons (V0 1) (V0 2))) (S0.case8 (V0 2) (V0 1) (V0 0) (S0.equal (V0 0) (V0 1))) :: R0 (S0.case8 (V0 0) (V0 1) (V0 2) S0.true) (V0 0) :: R0 (S0.case8 (V0 0) (V0 1) (V0 2) S0.false) (S0.cons (V0 1) (S0.delete (V0 2) (V0 0))) :: R0 (S0.gen_tag (V0 0)) (S0.tuple (V0 0) (S0.tuplenil S0.tag)) :: R0 (S0.gen_modtageq (V0 0) (V0 1)) (S0.equal (V0 0) (V0 1)) :: R0 (S0.member (V0 0) S0.nil) S0.false :: R0 (S0.member (V0 0) (S0.cons (V0 1) (V0 2))) (S0.case9 (V0 2) (V0 1) (V0 0) (S0.equal (V0 0) (V0 1))) :: R0 (S0.case9 (V0 0) (V0 1) (V0 2) S0.true) S0.true :: R0 (S0.case9 (V0 0) (V0 1) (V0 2) S0.false) (S0.member (V0 2) (V0 0)) :: R0 (S0.eqs S0.empty S0.empty) S0.T :: R0 (S0.eqs S0.empty (S0.stack (V0 0) (V0 1))) S0.F :: R0 (S0.eqs (S0.stack (V0 0) (V0 1)) S0.empty) S0.F :: R0 (S0.eqs (S0.stack (V0 0) (V0 1)) (S0.stack (V0 2) (V0 3))) (S0.and (S0.eqt (V0 0) (V0 2)) (S0.eqs (V0 1) (V0 3))) :: R0 (S0.pushs (V0 0) (V0 1)) (S0.stack (V0 0) (V0 1)) :: R0 (S0.pops (S0.stack (V0 0) (V0 1))) (V0 1) :: R0 (S0.tops (S0.stack (V0 0) (V0 1))) (V0 0) :: R0 (S0.istops (V0 0) S0.empty) S0.F :: R0 (S0.istops (V0 0) (S0.stack (V0 1) (V0 2))) (S0.eqt (V0 0) (V0 1)) :: R0 (S0.eqc S0.nocalls S0.nocalls) S0.T :: R0 (S0.eqc S0.nocalls (S0.calls (V0 0) (V0 1) (V0 2))) S0.F :: R0 (S0.eqc (S0.calls (V0 0) (V0 1) (V0 2)) S0.nocalls) S0.F :: R0 (S0.eqc (S0.calls (V0 0) (V0 1) (V0 2)) (S0.calls (V0 3) (V0 4) (V0 5))) (S0.and (S0.eqt (V0 0) (V0 3)) (S0.and (S0.eqs (V0 1) (V0 4)) (S0.eqc (V0 2) (V0 5)))) :: R0 (S0.push (V0 0) (V0 1) S0.nocalls) (S0.calls (V0 0) (S0.stack (V0 1) S0.empty) S0.nocalls) :: R0 (S0.push (V0 0) (V0 1) (S0.calls (V0 2) (V0 3) (V0 4))) (S0.push1 (V0 0) (V0 1) (V0 2) (V0 3) (V0 4) (S0.eqt (V0 0) (V0 2))) :: R0 (S0.push1 (V0 0) (V0 1) (V0 2) (V0 3) (V0 4) S0.T) (S0.calls (V0 2) (S0.pushs (V0 1) (V0 3)) (V0 4)) :: @nil (@ATrs.rule s0). Definition rel := ATrs.red_mod E R. (* symbol marking *) Definition s1 := dup_sig s0. Definition s1_p := s0. Definition V1 := @ATerm.Var s1. Definition F1 := @ATerm.Fun s1. Definition R1 := @ATrs.mkRule s1. Module S1. Definition hF := F1 (hd_symb s1_p M.F) Vnil. Definition F := F1 (int_symb s1_p M.F) Vnil. Definition hT := F1 (hd_symb s1_p M.T) Vnil. Definition T := F1 (int_symb s1_p M.T) Vnil. Definition h_0_1 := F1 (hd_symb s1_p M._0_1) Vnil. Definition _0_1 := F1 (int_symb s1_p M._0_1) Vnil. Definition h_if_2 x3 x2 x1 := F1 (hd_symb s1_p M._if_2) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition _if_2 x3 x2 x1 := F1 (int_symb s1_p M._if_2) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition ha := F1 (hd_symb s1_p M.a) Vnil. Definition a := F1 (int_symb s1_p M.a) Vnil. Definition hand x2 x1 := F1 (hd_symb s1_p M.and) (Vcons x2 (Vcons x1 Vnil)). Definition and x2 x1 := F1 (int_symb s1_p M.and) (Vcons x2 (Vcons x1 Vnil)). Definition handt x2 x1 := F1 (hd_symb s1_p M.andt) (Vcons x2 (Vcons x1 Vnil)). Definition andt x2 x1 := F1 (int_symb s1_p M.andt) (Vcons x2 (Vcons x1 Vnil)). Definition happend x2 x1 := F1 (hd_symb s1_p M.append) (Vcons x2 (Vcons x1 Vnil)). Definition append x2 x1 := F1 (int_symb s1_p M.append) (Vcons x2 (Vcons x1 Vnil)). Definition hcalls x3 x2 x1 := F1 (hd_symb s1_p M.calls) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition calls x3 x2 x1 := F1 (int_symb s1_p M.calls) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition hcase0 x3 x2 x1 := F1 (hd_symb s1_p M.case0) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition case0 x3 x2 x1 := F1 (int_symb s1_p M.case0) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition hcase1 x4 x3 x2 x1 := F1 (hd_symb s1_p M.case1) (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil)))). Definition case1 x4 x3 x2 x1 := F1 (int_symb s1_p M.case1) (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil)))). Definition hcase2 x3 x2 x1 := F1 (hd_symb s1_p M.case2) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition case2 x3 x2 x1 := F1 (int_symb s1_p M.case2) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition hcase4 x3 x2 x1 := F1 (hd_symb s1_p M.case4) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition case4 x3 x2 x1 := F1 (int_symb s1_p M.case4) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition hcase5 x4 x3 x2 x1 := F1 (hd_symb s1_p M.case5) (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil)))). Definition case5 x4 x3 x2 x1 := F1 (int_symb s1_p M.case5) (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil)))). Definition hcase6 x4 x3 x2 x1 := F1 (hd_symb s1_p M.case6) (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil)))). Definition case6 x4 x3 x2 x1 := F1 (int_symb s1_p M.case6) (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil)))). Definition hcase8 x4 x3 x2 x1 := F1 (hd_symb s1_p M.case8) (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil)))). Definition case8 x4 x3 x2 x1 := F1 (int_symb s1_p M.case8) (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil)))). Definition hcase9 x4 x3 x2 x1 := F1 (hd_symb s1_p M.case9) (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil)))). Definition case9 x4 x3 x2 x1 := F1 (int_symb s1_p M.case9) (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil)))). Definition hcons x2 x1 := F1 (hd_symb s1_p M.cons) (Vcons x2 (Vcons x1 Vnil)). Definition cons x2 x1 := F1 (int_symb s1_p M.cons) (Vcons x2 (Vcons x1 Vnil)). Definition hdelete x2 x1 := F1 (hd_symb s1_p M.delete) (Vcons x2 (Vcons x1 Vnil)). Definition delete x2 x1 := F1 (int_symb s1_p M.delete) (Vcons x2 (Vcons x1 Vnil)). Definition helement x2 x1 := F1 (hd_symb s1_p M.element) (Vcons x2 (Vcons x1 Vnil)). Definition element x2 x1 := F1 (int_symb s1_p M.element) (Vcons x2 (Vcons x1 Vnil)). Definition hempty := F1 (hd_symb s1_p M.empty) Vnil. Definition empty := F1 (int_symb s1_p M.empty) Vnil. Definition heq x2 x1 := F1 (hd_symb s1_p M.eq) (Vcons x2 (Vcons x1 Vnil)). Definition eq x2 x1 := F1 (int_symb s1_p M.eq) (Vcons x2 (Vcons x1 Vnil)). Definition heqc x2 x1 := F1 (hd_symb s1_p M.eqc) (Vcons x2 (Vcons x1 Vnil)). Definition eqc x2 x1 := F1 (int_symb s1_p M.eqc) (Vcons x2 (Vcons x1 Vnil)). Definition heqs x2 x1 := F1 (hd_symb s1_p M.eqs) (Vcons x2 (Vcons x1 Vnil)). Definition eqs x2 x1 := F1 (int_symb s1_p M.eqs) (Vcons x2 (Vcons x1 Vnil)). Definition heqt x2 x1 := F1 (hd_symb s1_p M.eqt) (Vcons x2 (Vcons x1 Vnil)). Definition eqt x2 x1 := F1 (int_symb s1_p M.eqt) (Vcons x2 (Vcons x1 Vnil)). Definition hequal x2 x1 := F1 (hd_symb s1_p M.equal) (Vcons x2 (Vcons x1 Vnil)). Definition equal x2 x1 := F1 (int_symb s1_p M.equal) (Vcons x2 (Vcons x1 Vnil)). Definition hexcl := F1 (hd_symb s1_p M.excl) Vnil. Definition excl := F1 (int_symb s1_p M.excl) Vnil. Definition hexcllock := F1 (hd_symb s1_p M.excllock) Vnil. Definition excllock := F1 (int_symb s1_p M.excllock) Vnil. Definition hfalse := F1 (hd_symb s1_p M.false) Vnil. Definition false := F1 (int_symb s1_p M.false) Vnil. Definition hgen_modtageq x2 x1 := F1 (hd_symb s1_p M.gen_modtageq) (Vcons x2 (Vcons x1 Vnil)). Definition gen_modtageq x2 x1 := F1 (int_symb s1_p M.gen_modtageq) (Vcons x2 (Vcons x1 Vnil)). Definition hgen_tag x1 := F1 (hd_symb s1_p M.gen_tag) (Vcons x1 Vnil). Definition gen_tag x1 := F1 (int_symb s1_p M.gen_tag) (Vcons x1 Vnil). Definition himp x2 x1 := F1 (hd_symb s1_p M.imp) (Vcons x2 (Vcons x1 Vnil)). Definition imp x2 x1 := F1 (int_symb s1_p M.imp) (Vcons x2 (Vcons x1 Vnil)). Definition hint x1 := F1 (hd_symb s1_p M.int) (Vcons x1 Vnil). Definition int x1 := F1 (int_symb s1_p M.int) (Vcons x1 Vnil). Definition histops x2 x1 := F1 (hd_symb s1_p M.istops) (Vcons x2 (Vcons x1 Vnil)). Definition istops x2 x1 := F1 (int_symb s1_p M.istops) (Vcons x2 (Vcons x1 Vnil)). Definition hlock := F1 (hd_symb s1_p M.lock) Vnil. Definition lock := F1 (int_symb s1_p M.lock) Vnil. Definition hlocker := F1 (hd_symb s1_p M.locker) Vnil. Definition locker := F1 (int_symb s1_p M.locker) Vnil. Definition hlocker2_add_pending x3 x2 x1 := F1 (hd_symb s1_p M.locker2_add_pending) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition locker2_add_pending x3 x2 x1 := F1 (int_symb s1_p M.locker2_add_pending) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition hlocker2_adduniq x2 x1 := F1 (hd_symb s1_p M.locker2_adduniq) (Vcons x2 (Vcons x1 Vnil)). Definition locker2_adduniq x2 x1 := F1 (int_symb s1_p M.locker2_adduniq) (Vcons x2 (Vcons x1 Vnil)). Definition hlocker2_check_available x2 x1 := F1 (hd_symb s1_p M.locker2_check_available) (Vcons x2 (Vcons x1 Vnil)). Definition locker2_check_available x2 x1 := F1 (int_symb s1_p M.locker2_check_available) (Vcons x2 (Vcons x1 Vnil)). Definition hlocker2_check_availables x2 x1 := F1 (hd_symb s1_p M.locker2_check_availables) (Vcons x2 (Vcons x1 Vnil)). Definition locker2_check_availables x2 x1 := F1 (int_symb s1_p M.locker2_check_availables) (Vcons x2 (Vcons x1 Vnil)). Definition hlocker2_claim_lock x3 x2 x1 := F1 (hd_symb s1_p M.locker2_claim_lock) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition locker2_claim_lock x3 x2 x1 := F1 (int_symb s1_p M.locker2_claim_lock) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition hlocker2_map_add_pending x3 x2 x1 := F1 (hd_symb s1_p M.locker2_map_add_pending) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition locker2_map_add_pending x3 x2 x1 := F1 (int_symb s1_p M.locker2_map_add_pending) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition hlocker2_map_claim_lock x3 x2 x1 := F1 (hd_symb s1_p M.locker2_map_claim_lock) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition locker2_map_claim_lock x3 x2 x1 := F1 (int_symb s1_p M.locker2_map_claim_lock) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition hlocker2_map_promote_pending x2 x1 := F1 (hd_symb s1_p M.locker2_map_promote_pending) (Vcons x2 (Vcons x1 Vnil)). Definition locker2_map_promote_pending x2 x1 := F1 (int_symb s1_p M.locker2_map_promote_pending) (Vcons x2 (Vcons x1 Vnil)). Definition hlocker2_obtainable x2 x1 := F1 (hd_symb s1_p M.locker2_obtainable) (Vcons x2 (Vcons x1 Vnil)). Definition locker2_obtainable x2 x1 := F1 (int_symb s1_p M.locker2_obtainable) (Vcons x2 (Vcons x1 Vnil)). Definition hlocker2_obtainables x2 x1 := F1 (hd_symb s1_p M.locker2_obtainables) (Vcons x2 (Vcons x1 Vnil)). Definition locker2_obtainables x2 x1 := F1 (int_symb s1_p M.locker2_obtainables) (Vcons x2 (Vcons x1 Vnil)). Definition hlocker2_promote_pending x2 x1 := F1 (hd_symb s1_p M.locker2_promote_pending) (Vcons x2 (Vcons x1 Vnil)). Definition locker2_promote_pending x2 x1 := F1 (int_symb s1_p M.locker2_promote_pending) (Vcons x2 (Vcons x1 Vnil)). Definition hlocker2_release_lock x2 x1 := F1 (hd_symb s1_p M.locker2_release_lock) (Vcons x2 (Vcons x1 Vnil)). Definition locker2_release_lock x2 x1 := F1 (int_symb s1_p M.locker2_release_lock) (Vcons x2 (Vcons x1 Vnil)). Definition hlocker2_remove_pending x2 x1 := F1 (hd_symb s1_p M.locker2_remove_pending) (Vcons x2 (Vcons x1 Vnil)). Definition locker2_remove_pending x2 x1 := F1 (int_symb s1_p M.locker2_remove_pending) (Vcons x2 (Vcons x1 Vnil)). Definition hmcrlrecord := F1 (hd_symb s1_p M.mcrlrecord) Vnil. Definition mcrlrecord := F1 (int_symb s1_p M.mcrlrecord) Vnil. Definition hmember x2 x1 := F1 (hd_symb s1_p M.member) (Vcons x2 (Vcons x1 Vnil)). Definition member x2 x1 := F1 (int_symb s1_p M.member) (Vcons x2 (Vcons x1 Vnil)). Definition hnil := F1 (hd_symb s1_p M.nil) Vnil. Definition nil := F1 (int_symb s1_p M.nil) Vnil. Definition hnocalls := F1 (hd_symb s1_p M.nocalls) Vnil. Definition nocalls := F1 (int_symb s1_p M.nocalls) Vnil. Definition hnot x1 := F1 (hd_symb s1_p M.not) (Vcons x1 Vnil). Definition not x1 := F1 (int_symb s1_p M.not) (Vcons x1 Vnil). Definition hok := F1 (hd_symb s1_p M.ok) Vnil. Definition ok := F1 (int_symb s1_p M.ok) Vnil. Definition hor x2 x1 := F1 (hd_symb s1_p M.or) (Vcons x2 (Vcons x1 Vnil)). Definition or x2 x1 := F1 (int_symb s1_p M.or) (Vcons x2 (Vcons x1 Vnil)). Definition hpending := F1 (hd_symb s1_p M.pending) Vnil. Definition pending := F1 (int_symb s1_p M.pending) Vnil. Definition hpid x1 := F1 (hd_symb s1_p M.pid) (Vcons x1 Vnil). Definition pid x1 := F1 (int_symb s1_p M.pid) (Vcons x1 Vnil). Definition hpops x1 := F1 (hd_symb s1_p M.pops) (Vcons x1 Vnil). Definition pops x1 := F1 (int_symb s1_p M.pops) (Vcons x1 Vnil). Definition hpush x3 x2 x1 := F1 (hd_symb s1_p M.push) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition push x3 x2 x1 := F1 (int_symb s1_p M.push) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition hpush1 x6 x5 x4 x3 x2 x1 := F1 (hd_symb s1_p M.push1) (Vcons x6 (Vcons x5 (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil)))))). Definition push1 x6 x5 x4 x3 x2 x1 := F1 (int_symb s1_p M.push1) (Vcons x6 (Vcons x5 (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil)))))). Definition hpushs x2 x1 := F1 (hd_symb s1_p M.pushs) (Vcons x2 (Vcons x1 Vnil)). Definition pushs x2 x1 := F1 (int_symb s1_p M.pushs) (Vcons x2 (Vcons x1 Vnil)). Definition hrecord_extract x3 x2 x1 := F1 (hd_symb s1_p M.record_extract) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition record_extract x3 x2 x1 := F1 (int_symb s1_p M.record_extract) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition hrecord_new x1 := F1 (hd_symb s1_p M.record_new) (Vcons x1 Vnil). Definition record_new x1 := F1 (int_symb s1_p M.record_new) (Vcons x1 Vnil). Definition hrecord_update x4 x3 x2 x1 := F1 (hd_symb s1_p M.record_update) (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil)))). Definition record_update x4 x3 x2 x1 := F1 (int_symb s1_p M.record_update) (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil)))). Definition hrecord_updates x3 x2 x1 := F1 (hd_symb s1_p M.record_updates) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition record_updates x3 x2 x1 := F1 (int_symb s1_p M.record_updates) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition hrelease := F1 (hd_symb s1_p M.release) Vnil. Definition release := F1 (int_symb s1_p M.release) Vnil. Definition hrequest := F1 (hd_symb s1_p M.request) Vnil. Definition request := F1 (int_symb s1_p M.request) Vnil. Definition hresource := F1 (hd_symb s1_p M.resource) Vnil. Definition resource := F1 (int_symb s1_p M.resource) Vnil. Definition hs x1 := F1 (hd_symb s1_p M.s) (Vcons x1 Vnil). Definition s x1 := F1 (int_symb s1_p M.s) (Vcons x1 Vnil). Definition hstack x2 x1 := F1 (hd_symb s1_p M.stack) (Vcons x2 (Vcons x1 Vnil)). Definition stack x2 x1 := F1 (int_symb s1_p M.stack) (Vcons x2 (Vcons x1 Vnil)). Definition hsubtract x2 x1 := F1 (hd_symb s1_p M.subtract) (Vcons x2 (Vcons x1 Vnil)). Definition subtract x2 x1 := F1 (int_symb s1_p M.subtract) (Vcons x2 (Vcons x1 Vnil)). Definition htag := F1 (hd_symb s1_p M.tag) Vnil. Definition tag := F1 (int_symb s1_p M.tag) Vnil. Definition htops x1 := F1 (hd_symb s1_p M.tops) (Vcons x1 Vnil). Definition tops x1 := F1 (int_symb s1_p M.tops) (Vcons x1 Vnil). Definition htrue := F1 (hd_symb s1_p M.true) Vnil. Definition true := F1 (int_symb s1_p M.true) Vnil. Definition htuple x2 x1 := F1 (hd_symb s1_p M.tuple) (Vcons x2 (Vcons x1 Vnil)). Definition tuple x2 x1 := F1 (int_symb s1_p M.tuple) (Vcons x2 (Vcons x1 Vnil)). Definition htuplenil x1 := F1 (hd_symb s1_p M.tuplenil) (Vcons x1 Vnil). Definition tuplenil x1 := F1 (int_symb s1_p M.tuplenil) (Vcons x1 Vnil). Definition hundefined := F1 (hd_symb s1_p M.undefined) Vnil. Definition undefined := F1 (int_symb s1_p M.undefined) Vnil. End S1. (* graph decomposition 1 *) Definition cs1 : list (list (@ATrs.rule s1)) := ( R1 (S1.hpush1 (V1 0) (V1 1) (V1 2) (V1 3) (V1 4) (S1.T)) (S1.hpushs (V1 1) (V1 3)) :: nil) :: ( R1 (S1.hpush (V1 0) (V1 1) (S1.calls (V1 2) (V1 3) (V1 4))) (S1.hpush1 (V1 0) (V1 1) (V1 2) (V1 3) (V1 4) (S1.eqt (V1 0) (V1 2))) :: nil) :: ( R1 (S1.heqc (S1.calls (V1 0) (V1 1) (V1 2)) (S1.calls (V1 3) (V1 4) (V1 5))) (S1.hand (S1.eqs (V1 1) (V1 4)) (S1.eqc (V1 2) (V1 5))) :: nil) :: ( R1 (S1.heqc (S1.calls (V1 0) (V1 1) (V1 2)) (S1.calls (V1 3) (V1 4) (V1 5))) (S1.hand (S1.eqt (V1 0) (V1 3)) (S1.and (S1.eqs (V1 1) (V1 4)) (S1.eqc (V1 2) (V1 5)))) :: nil) :: ( R1 (S1.heqs (S1.stack (V1 0) (V1 1)) (S1.stack (V1 2) (V1 3))) (S1.hand (S1.eqt (V1 0) (V1 2)) (S1.eqs (V1 1) (V1 3))) :: nil) :: ( R1 (S1.hmember (V1 0) (S1.cons (V1 1) (V1 2))) (S1.hcase9 (V1 2) (V1 1) (V1 0) (S1.equal (V1 0) (V1 1))) :: nil) :: ( R1 (S1.hcase9 (V1 0) (V1 1) (V1 2) (S1.false)) (S1.hmember (V1 2) (V1 0)) :: nil) :: ( R1 (S1.hdelete (V1 0) (S1.cons (V1 1) (V1 2))) (S1.hcase8 (V1 2) (V1 1) (V1 0) (S1.equal (V1 0) (V1 1))) :: nil) :: ( R1 (S1.hcase8 (V1 0) (V1 1) (V1 2) (S1.false)) (S1.hdelete (V1 2) (V1 0)) :: nil) :: ( R1 (S1.hsubtract (V1 0) (S1.cons (V1 1) (V1 2))) (S1.hdelete (V1 1) (V1 0)) :: nil) :: ( R1 (S1.hsubtract (V1 0) (S1.cons (V1 1) (V1 2))) (S1.hsubtract (S1.delete (V1 1) (V1 0)) (V1 2)) :: nil) :: ( R1 (S1.happend (S1.cons (V1 0) (V1 1)) (V1 2)) (S1.happend (V1 1) (V1 2)) :: nil) :: ( R1 (S1.hcase6 (V1 0) (V1 1) (V1 2) (S1.true)) (S1.hrecord_extract (V1 1) (S1.lock) (S1.pending)) :: nil) :: ( R1 (S1.hcase6 (V1 0) (V1 1) (V1 2) (S1.true)) (S1.hrecord_extract (V1 1) (S1.lock) (S1.excl)) :: nil) :: ( R1 (S1.hlocker2_check_available (V1 0) (S1.cons (V1 1) (V1 2))) (S1.hrecord_extract (V1 1) (S1.lock) (S1.resource)) :: nil) :: ( R1 (S1.hlocker2_check_available (V1 0) (S1.cons (V1 1) (V1 2))) (S1.hcase6 (V1 2) (V1 1) (V1 0) (S1.equal (V1 0) (S1.record_extract (V1 1) (S1.lock) (S1.resource)))) :: nil) :: ( R1 (S1.hlocker2_check_availables (S1.cons (V1 0) (V1 1)) (V1 2)) (S1.hlocker2_check_available (V1 0) (V1 2)) :: nil) :: ( R1 (S1.hlocker2_check_availables (S1.cons (V1 0) (V1 1)) (V1 2)) (S1.hlocker2_check_availables (V1 1) (V1 2)) :: nil) :: ( R1 (S1.hcase6 (V1 0) (V1 1) (V1 2) (S1.false)) (S1.hlocker2_check_available (V1 2) (V1 0)) :: nil) :: ( R1 (S1.hlocker2_obtainables (S1.cons (V1 0) (V1 1)) (V1 2)) (S1.hrecord_extract (V1 0) (S1.lock) (S1.pending)) :: nil) :: ( R1 (S1.hlocker2_obtainables (S1.cons (V1 0) (V1 1)) (V1 2)) (S1.hmember (V1 2) (S1.record_extract (V1 0) (S1.lock) (S1.pending))) :: nil) :: ( R1 (S1.hcase5 (V1 0) (V1 1) (V1 2) (S1.true)) (S1.hlocker2_obtainables (V1 1) (V1 0)) :: R1 (S1.hlocker2_obtainables (S1.cons (V1 0) (V1 1)) (V1 2)) (S1.hcase5 (V1 2) (V1 1) (V1 0) (S1.member (V1 2) (S1.record_extract (V1 0) (S1.lock) (S1.pending)))) :: R1 (S1.hcase5 (V1 0) (V1 1) (V1 2) (S1.false)) (S1.hlocker2_obtainables (V1 1) (V1 0)) :: nil) :: ( R1 (S1.hlocker2_release_lock (V1 0) (V1 1)) (S1.hrecord_extract (V1 0) (S1.lock) (S1.excl)) :: nil) :: ( R1 (S1.hlocker2_release_lock (V1 0) (V1 1)) (S1.hgen_modtageq (V1 1) (S1.record_extract (V1 0) (S1.lock) (S1.excl))) :: nil) :: ( R1 (S1.hcase1 (V1 0) (V1 1) (V1 2) (S1.true)) (S1.hrecord_extract (V1 2) (S1.lock) (S1.pending)) :: nil) :: ( R1 (S1.hcase1 (V1 0) (V1 1) (V1 2) (S1.true)) (S1.happend (S1.record_extract (V1 2) (S1.lock) (S1.pending)) (S1.cons (V1 0) (S1.nil))) :: nil) :: ( R1 (S1.hlocker2_add_pending (V1 0) (V1 1) (V1 2)) (S1.hrecord_extract (V1 0) (S1.lock) (S1.resource)) :: nil) :: ( R1 (S1.hlocker2_add_pending (V1 0) (V1 1) (V1 2)) (S1.hmember (S1.record_extract (V1 0) (S1.lock) (S1.resource)) (V1 1)) :: nil) :: ( R1 (S1.hlocker2_remove_pending (V1 0) (V1 1)) (S1.hrecord_extract (V1 0) (S1.lock) (S1.pending)) :: nil) :: ( R1 (S1.hlocker2_remove_pending (V1 0) (V1 1)) (S1.hsubtract (S1.record_extract (V1 0) (S1.lock) (S1.pending)) (S1.cons (V1 1) (S1.nil))) :: nil) :: ( R1 (S1.hlocker2_promote_pending (V1 0) (V1 1)) (S1.hrecord_extract (V1 0) (S1.lock) (S1.pending)) :: nil) :: ( R1 (S1.hlocker2_map_claim_lock (S1.cons (V1 0) (V1 1)) (V1 2) (V1 3)) (S1.hlocker2_map_claim_lock (V1 1) (V1 2) (V1 3)) :: nil) :: ( R1 (S1.hrecord_updates (V1 0) (V1 1) (S1.cons (S1.tuple (V1 2) (S1.tuplenil (V1 3))) (V1 4))) (S1.hrecord_update (V1 0) (V1 1) (V1 2) (V1 3)) :: nil) :: ( R1 (S1.hrecord_updates (V1 0) (V1 1) (S1.cons (S1.tuple (V1 2) (S1.tuplenil (V1 3))) (V1 4))) (S1.hrecord_updates (S1.record_update (V1 0) (V1 1) (V1 2) (V1 3)) (V1 1) (V1 4)) :: nil) :: ( R1 (S1.hcase2 (V1 0) (V1 1) (S1.true)) (S1.hrecord_updates (V1 1) (S1.lock) (S1.cons (S1.tuple (S1.excllock) (S1.excl)) (S1.nil))) :: nil) :: ( R1 (S1.hlocker2_release_lock (V1 0) (V1 1)) (S1.hcase2 (V1 1) (V1 0) (S1.gen_modtageq (V1 1) (S1.record_extract (V1 0) (S1.lock) (S1.excl)))) :: nil) :: ( R1 (S1.hcase1 (V1 0) (V1 1) (V1 2) (S1.true)) (S1.hrecord_updates (V1 2) (S1.lock) (S1.cons (S1.tuple (S1.pending) (S1.tuplenil (S1.append (S1.record_extract (V1 2) (S1.lock) (S1.pending)) (S1.cons (V1 0) (S1.nil))))) (S1.nil))) :: nil) :: ( R1 (S1.hlocker2_add_pending (V1 0) (V1 1) (V1 2)) (S1.hcase1 (V1 2) (V1 1) (V1 0) (S1.member (S1.record_extract (V1 0) (S1.lock) (S1.resource)) (V1 1))) :: nil) :: ( R1 (S1.hlocker2_remove_pending (V1 0) (V1 1)) (S1.hrecord_updates (V1 0) (S1.lock) (S1.cons (S1.tuple (S1.pending) (S1.tuplenil (S1.subtract (S1.record_extract (V1 0) (S1.lock) (S1.pending)) (S1.cons (V1 1) (S1.nil))))) (S1.nil))) :: nil) :: ( R1 (S1.hcase0 (V1 0) (V1 1) (S1.cons (V1 0) (V1 3))) (S1.hrecord_updates (V1 1) (S1.lock) (S1.cons (S1.tuple (S1.excl) (S1.tuplenil (V1 0))) (S1.cons (S1.tuple (S1.pending) (S1.tuplenil (V1 3))) (S1.nil)))) :: nil) :: ( R1 (S1.hlocker2_promote_pending (V1 0) (V1 1)) (S1.hcase0 (V1 1) (V1 0) (S1.record_extract (V1 0) (S1.lock) (S1.pending))) :: nil) :: ( R1 (S1.hlocker2_map_promote_pending (S1.cons (V1 0) (V1 1)) (V1 2)) (S1.hlocker2_promote_pending (V1 0) (V1 2)) :: nil) :: ( R1 (S1.hlocker2_map_promote_pending (S1.cons (V1 0) (V1 1)) (V1 2)) (S1.hlocker2_map_promote_pending (V1 1) (V1 2)) :: nil) :: ( R1 (S1.helement (S1.int (S1.s (S1.s (V1 0)))) (S1.tuple (V1 1) (V1 2))) (S1.helement (S1.int (S1.s (V1 0))) (V1 2)) :: nil) :: ( R1 (S1.heqt (S1.tuple (V1 0) (V1 1)) (S1.tuple (V1 2) (V1 3))) (S1.hand (S1.eqt (V1 0) (V1 2)) (S1.eqt (V1 1) (V1 3))) :: nil) :: ( R1 (S1.heqt (S1.cons (V1 0) (V1 1)) (S1.cons (V1 2) (V1 3))) (S1.hand (S1.eqt (V1 0) (V1 2)) (S1.eqt (V1 1) (V1 3))) :: nil) :: ( R1 (S1.heqt (S1.cons (V1 0) (V1 1)) (S1.cons (V1 2) (V1 3))) (S1.heqt (V1 0) (V1 2)) :: R1 (S1.heqt (S1.pid (V1 0)) (S1.pid (V1 1))) (S1.heqt (V1 0) (V1 1)) :: R1 (S1.heqt (S1.cons (V1 0) (V1 1)) (S1.cons (V1 2) (V1 3))) (S1.heqt (V1 1) (V1 3)) :: R1 (S1.heqt (S1.tuple (V1 0) (V1 1)) (S1.tuple (V1 2) (V1 3))) (S1.heqt (V1 0) (V1 2)) :: R1 (S1.heqt (S1.tuple (V1 0) (V1 1)) (S1.tuple (V1 2) (V1 3))) (S1.heqt (V1 1) (V1 3)) :: R1 (S1.heqt (S1.tuplenil (V1 0)) (S1.tuplenil (V1 1))) (S1.heqt (V1 0) (V1 1)) :: nil) :: ( R1 (S1.hpush (V1 0) (V1 1) (S1.calls (V1 2) (V1 3) (V1 4))) (S1.heqt (V1 0) (V1 2)) :: nil) :: ( R1 (S1.heqc (S1.calls (V1 0) (V1 1) (V1 2)) (S1.calls (V1 3) (V1 4) (V1 5))) (S1.heqt (V1 0) (V1 3)) :: nil) :: ( R1 (S1.histops (V1 0) (S1.stack (V1 1) (V1 2))) (S1.heqt (V1 0) (V1 1)) :: nil) :: ( R1 (S1.heqs (S1.stack (V1 0) (V1 1)) (S1.stack (V1 2) (V1 3))) (S1.heqt (V1 0) (V1 2)) :: nil) :: ( R1 (S1.heqs (S1.stack (V1 0) (V1 1)) (S1.stack (V1 2) (V1 3))) (S1.heqs (V1 1) (V1 3)) :: nil) :: ( R1 (S1.heqc (S1.calls (V1 0) (V1 1) (V1 2)) (S1.calls (V1 3) (V1 4) (V1 5))) (S1.heqs (V1 1) (V1 4)) :: nil) :: ( R1 (S1.heqc (S1.calls (V1 0) (V1 1) (V1 2)) (S1.calls (V1 3) (V1 4) (V1 5))) (S1.heqc (V1 2) (V1 5)) :: nil) :: nil. (* polynomial interpretation 1 *) Module PIS1 (*<: TPolyInt*). Definition sig := s1. Definition trsInt f := match f as f return poly (@ASignature.arity s1 f) with | (hd_symb M.or) => nil | (int_symb M.or) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (hd_symb M.T) => nil | (int_symb M.T) => nil | (hd_symb M.F) => nil | (int_symb M.F) => nil | (hd_symb M.and) => nil | (int_symb M.and) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.imp) => nil | (int_symb M.imp) => (3%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.not) => nil | (int_symb M.not) => (1%Z, (Vcons 0 Vnil)) :: nil | (hd_symb M._if_2) => nil | (int_symb M._if_2) => (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.eq) => nil | (int_symb M.eq) => nil | (hd_symb M.eqt) => nil | (int_symb M.eqt) => nil | (hd_symb M.nil) => nil | (int_symb M.nil) => nil | (hd_symb M.undefined) => nil | (int_symb M.undefined) => nil | (hd_symb M.pid) => nil | (int_symb M.pid) => nil | (hd_symb M.int) => nil | (int_symb M.int) => nil | (hd_symb M.cons) => nil | (int_symb M.cons) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.tuple) => nil | (int_symb M.tuple) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.tuplenil) => nil | (int_symb M.tuplenil) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a) => nil | (int_symb M.a) => nil | (hd_symb M.excl) => nil | (int_symb M.excl) => nil | (hd_symb M.false) => nil | (int_symb M.false) => nil | (hd_symb M.lock) => nil | (int_symb M.lock) => nil | (hd_symb M.locker) => nil | (int_symb M.locker) => nil | (hd_symb M.mcrlrecord) => nil | (int_symb M.mcrlrecord) => nil | (hd_symb M.ok) => nil | (int_symb M.ok) => nil | (hd_symb M.pending) => nil | (int_symb M.pending) => nil | (hd_symb M.release) => nil | (int_symb M.release) => nil | (hd_symb M.request) => nil | (int_symb M.request) => nil | (hd_symb M.resource) => nil | (int_symb M.resource) => nil | (hd_symb M.tag) => nil | (int_symb M.tag) => nil | (hd_symb M.true) => nil | (int_symb M.true) => nil | (hd_symb M.element) => nil | (int_symb M.element) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.s) => nil | (int_symb M.s) => nil | (hd_symb M._0_1) => nil | (int_symb M._0_1) => nil | (hd_symb M.record_new) => nil | (int_symb M.record_new) => nil | (hd_symb M.record_extract) => nil | (int_symb M.record_extract) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.record_update) => nil | (int_symb M.record_update) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))) :: nil | (hd_symb M.record_updates) => nil | (int_symb M.record_updates) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.locker2_map_promote_pending) => nil | (int_symb M.locker2_map_promote_pending) => (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_promote_pending) => nil | (int_symb M.locker2_promote_pending) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_map_claim_lock) => nil | (int_symb M.locker2_map_claim_lock) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_claim_lock) => nil | (int_symb M.locker2_claim_lock) => nil | (hd_symb M.locker2_map_add_pending) => nil | (int_symb M.locker2_map_add_pending) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.case0) => nil | (int_symb M.case0) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.locker2_remove_pending) => nil | (int_symb M.locker2_remove_pending) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.subtract) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (int_symb M.subtract) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_add_pending) => nil | (int_symb M.locker2_add_pending) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (3%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.case1) => nil | (int_symb M.case1) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: (3%Z, (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))) :: nil | (hd_symb M.member) => nil | (int_symb M.member) => nil | (hd_symb M.append) => nil | (int_symb M.append) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_release_lock) => nil | (int_symb M.locker2_release_lock) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.case2) => nil | (int_symb M.case2) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: nil | (hd_symb M.gen_modtageq) => nil | (int_symb M.gen_modtageq) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.excllock) => nil | (int_symb M.excllock) => nil | (hd_symb M.case4) => nil | (int_symb M.case4) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_obtainables) => nil | (int_symb M.locker2_obtainables) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.case5) => nil | (int_symb M.case5) => (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))) :: nil | (hd_symb M.andt) => nil | (int_symb M.andt) => nil | (hd_symb M.locker2_obtainable) => nil | (int_symb M.locker2_obtainable) => nil | (hd_symb M.locker2_check_available) => nil | (int_symb M.locker2_check_available) => (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.case6) => nil | (int_symb M.case6) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: nil | (hd_symb M.equal) => nil | (int_symb M.equal) => nil | (hd_symb M.locker2_check_availables) => nil | (int_symb M.locker2_check_availables) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_adduniq) => nil | (int_symb M.locker2_adduniq) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.delete) => nil | (int_symb M.delete) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.case8) => nil | (int_symb M.case8) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: nil | (hd_symb M.gen_tag) => nil | (int_symb M.gen_tag) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.case9) => nil | (int_symb M.case9) => nil | (hd_symb M.eqs) => nil | (int_symb M.eqs) => nil | (hd_symb M.empty) => nil | (int_symb M.empty) => nil | (hd_symb M.stack) => nil | (int_symb M.stack) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.pushs) => nil | (int_symb M.pushs) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.pops) => nil | (int_symb M.pops) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.tops) => nil | (int_symb M.tops) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.istops) => nil | (int_symb M.istops) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.eqc) => nil | (int_symb M.eqc) => nil | (hd_symb M.nocalls) => nil | (int_symb M.nocalls) => nil | (hd_symb M.calls) => nil | (int_symb M.calls) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.push) => nil | (int_symb M.push) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (3%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.push1) => nil | (int_symb M.push1) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))))) :: nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS1. Module PI1 := PolyInt PIS1. (* polynomial interpretation 2 *) Module PIS2 (*<: TPolyInt*). Definition sig := s1. Definition trsInt f := match f as f return poly (@ASignature.arity s1 f) with | (hd_symb M.or) => nil | (int_symb M.or) => nil | (hd_symb M.T) => nil | (int_symb M.T) => nil | (hd_symb M.F) => nil | (int_symb M.F) => nil | (hd_symb M.and) => nil | (int_symb M.and) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.imp) => nil | (int_symb M.imp) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.not) => nil | (int_symb M.not) => (1%Z, (Vcons 0 Vnil)) :: nil | (hd_symb M._if_2) => nil | (int_symb M._if_2) => (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.eq) => nil | (int_symb M.eq) => nil | (hd_symb M.eqt) => nil | (int_symb M.eqt) => nil | (hd_symb M.nil) => nil | (int_symb M.nil) => nil | (hd_symb M.undefined) => nil | (int_symb M.undefined) => nil | (hd_symb M.pid) => nil | (int_symb M.pid) => nil | (hd_symb M.int) => nil | (int_symb M.int) => nil | (hd_symb M.cons) => nil | (int_symb M.cons) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.tuple) => nil | (int_symb M.tuple) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.tuplenil) => nil | (int_symb M.tuplenil) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a) => nil | (int_symb M.a) => nil | (hd_symb M.excl) => nil | (int_symb M.excl) => nil | (hd_symb M.false) => nil | (int_symb M.false) => nil | (hd_symb M.lock) => nil | (int_symb M.lock) => (1%Z, Vnil) :: nil | (hd_symb M.locker) => nil | (int_symb M.locker) => nil | (hd_symb M.mcrlrecord) => nil | (int_symb M.mcrlrecord) => nil | (hd_symb M.ok) => nil | (int_symb M.ok) => nil | (hd_symb M.pending) => nil | (int_symb M.pending) => nil | (hd_symb M.release) => nil | (int_symb M.release) => nil | (hd_symb M.request) => nil | (int_symb M.request) => nil | (hd_symb M.resource) => nil | (int_symb M.resource) => (1%Z, Vnil) :: nil | (hd_symb M.tag) => nil | (int_symb M.tag) => nil | (hd_symb M.true) => nil | (int_symb M.true) => nil | (hd_symb M.element) => nil | (int_symb M.element) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.s) => nil | (int_symb M.s) => nil | (hd_symb M._0_1) => nil | (int_symb M._0_1) => nil | (hd_symb M.record_new) => nil | (int_symb M.record_new) => (3%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.record_extract) => nil | (int_symb M.record_extract) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.record_update) => nil | (int_symb M.record_update) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))) :: nil | (hd_symb M.record_updates) => nil | (int_symb M.record_updates) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.locker2_map_promote_pending) => nil | (int_symb M.locker2_map_promote_pending) => (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_promote_pending) => nil | (int_symb M.locker2_promote_pending) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_map_claim_lock) => nil | (int_symb M.locker2_map_claim_lock) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_claim_lock) => nil | (int_symb M.locker2_claim_lock) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_map_add_pending) => nil | (int_symb M.locker2_map_add_pending) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.case0) => nil | (int_symb M.case0) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.locker2_remove_pending) => nil | (int_symb M.locker2_remove_pending) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.subtract) => nil | (int_symb M.subtract) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_add_pending) => nil | (int_symb M.locker2_add_pending) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (3%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.case1) => nil | (int_symb M.case1) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))) :: nil | (hd_symb M.member) => nil | (int_symb M.member) => (3%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.append) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (int_symb M.append) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_release_lock) => nil | (int_symb M.locker2_release_lock) => (3%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (3%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.case2) => nil | (int_symb M.case2) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: nil | (hd_symb M.gen_modtageq) => nil | (int_symb M.gen_modtageq) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.excllock) => nil | (int_symb M.excllock) => nil | (hd_symb M.case4) => nil | (int_symb M.case4) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_obtainables) => nil | (int_symb M.locker2_obtainables) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.case5) => nil | (int_symb M.case5) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: nil | (hd_symb M.andt) => nil | (int_symb M.andt) => nil | (hd_symb M.locker2_obtainable) => nil | (int_symb M.locker2_obtainable) => nil | (hd_symb M.locker2_check_available) => nil | (int_symb M.locker2_check_available) => nil | (hd_symb M.case6) => nil | (int_symb M.case6) => nil | (hd_symb M.equal) => nil | (int_symb M.equal) => nil | (hd_symb M.locker2_check_availables) => nil | (int_symb M.locker2_check_availables) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_adduniq) => nil | (int_symb M.locker2_adduniq) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.delete) => nil | (int_symb M.delete) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.case8) => nil | (int_symb M.case8) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: nil | (hd_symb M.gen_tag) => nil | (int_symb M.gen_tag) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.case9) => nil | (int_symb M.case9) => (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (3%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: nil | (hd_symb M.eqs) => nil | (int_symb M.eqs) => nil | (hd_symb M.empty) => nil | (int_symb M.empty) => nil | (hd_symb M.stack) => nil | (int_symb M.stack) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.pushs) => nil | (int_symb M.pushs) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.pops) => nil | (int_symb M.pops) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.tops) => nil | (int_symb M.tops) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.istops) => nil | (int_symb M.istops) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.eqc) => nil | (int_symb M.eqc) => nil | (hd_symb M.nocalls) => nil | (int_symb M.nocalls) => nil | (hd_symb M.calls) => nil | (int_symb M.calls) => nil | (hd_symb M.push) => nil | (int_symb M.push) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: nil | (hd_symb M.push1) => nil | (int_symb M.push1) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))))) :: nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS2. Module PI2 := PolyInt PIS2. (* polynomial interpretation 3 *) Module PIS3 (*<: TPolyInt*). Definition sig := s1. Definition trsInt f := match f as f return poly (@ASignature.arity s1 f) with | (hd_symb M.or) => nil | (int_symb M.or) => nil | (hd_symb M.T) => nil | (int_symb M.T) => nil | (hd_symb M.F) => nil | (int_symb M.F) => nil | (hd_symb M.and) => nil | (int_symb M.and) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.imp) => nil | (int_symb M.imp) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.not) => nil | (int_symb M.not) => (1%Z, (Vcons 0 Vnil)) :: nil | (hd_symb M._if_2) => nil | (int_symb M._if_2) => (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.eq) => nil | (int_symb M.eq) => nil | (hd_symb M.eqt) => nil | (int_symb M.eqt) => nil | (hd_symb M.nil) => nil | (int_symb M.nil) => nil | (hd_symb M.undefined) => nil | (int_symb M.undefined) => nil | (hd_symb M.pid) => nil | (int_symb M.pid) => nil | (hd_symb M.int) => nil | (int_symb M.int) => nil | (hd_symb M.cons) => nil | (int_symb M.cons) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.tuple) => nil | (int_symb M.tuple) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.tuplenil) => nil | (int_symb M.tuplenil) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a) => nil | (int_symb M.a) => nil | (hd_symb M.excl) => nil | (int_symb M.excl) => nil | (hd_symb M.false) => nil | (int_symb M.false) => nil | (hd_symb M.lock) => nil | (int_symb M.lock) => (1%Z, Vnil) :: nil | (hd_symb M.locker) => nil | (int_symb M.locker) => nil | (hd_symb M.mcrlrecord) => nil | (int_symb M.mcrlrecord) => nil | (hd_symb M.ok) => nil | (int_symb M.ok) => nil | (hd_symb M.pending) => nil | (int_symb M.pending) => nil | (hd_symb M.release) => nil | (int_symb M.release) => nil | (hd_symb M.request) => nil | (int_symb M.request) => nil | (hd_symb M.resource) => nil | (int_symb M.resource) => (1%Z, Vnil) :: nil | (hd_symb M.tag) => nil | (int_symb M.tag) => nil | (hd_symb M.true) => nil | (int_symb M.true) => nil | (hd_symb M.element) => nil | (int_symb M.element) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.s) => nil | (int_symb M.s) => nil | (hd_symb M._0_1) => nil | (int_symb M._0_1) => nil | (hd_symb M.record_new) => nil | (int_symb M.record_new) => (3%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.record_extract) => nil | (int_symb M.record_extract) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.record_update) => nil | (int_symb M.record_update) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))) :: nil | (hd_symb M.record_updates) => nil | (int_symb M.record_updates) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.locker2_map_promote_pending) => nil | (int_symb M.locker2_map_promote_pending) => (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_promote_pending) => nil | (int_symb M.locker2_promote_pending) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_map_claim_lock) => nil | (int_symb M.locker2_map_claim_lock) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_claim_lock) => nil | (int_symb M.locker2_claim_lock) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_map_add_pending) => nil | (int_symb M.locker2_map_add_pending) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.case0) => nil | (int_symb M.case0) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.locker2_remove_pending) => nil | (int_symb M.locker2_remove_pending) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.subtract) => nil | (int_symb M.subtract) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_add_pending) => nil | (int_symb M.locker2_add_pending) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (3%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.case1) => nil | (int_symb M.case1) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))) :: nil | (hd_symb M.member) => nil | (int_symb M.member) => (3%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.append) => nil | (int_symb M.append) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_release_lock) => nil | (int_symb M.locker2_release_lock) => (3%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (3%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.case2) => nil | (int_symb M.case2) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: nil | (hd_symb M.gen_modtageq) => nil | (int_symb M.gen_modtageq) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.excllock) => nil | (int_symb M.excllock) => nil | (hd_symb M.case4) => nil | (int_symb M.case4) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_obtainables) => nil | (int_symb M.locker2_obtainables) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.case5) => nil | (int_symb M.case5) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: nil | (hd_symb M.andt) => nil | (int_symb M.andt) => nil | (hd_symb M.locker2_obtainable) => nil | (int_symb M.locker2_obtainable) => nil | (hd_symb M.locker2_check_available) => nil | (int_symb M.locker2_check_available) => nil | (hd_symb M.case6) => nil | (int_symb M.case6) => nil | (hd_symb M.equal) => nil | (int_symb M.equal) => nil | (hd_symb M.locker2_check_availables) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (int_symb M.locker2_check_availables) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_adduniq) => nil | (int_symb M.locker2_adduniq) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.delete) => nil | (int_symb M.delete) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.case8) => nil | (int_symb M.case8) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: nil | (hd_symb M.gen_tag) => nil | (int_symb M.gen_tag) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.case9) => nil | (int_symb M.case9) => (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (3%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: nil | (hd_symb M.eqs) => nil | (int_symb M.eqs) => nil | (hd_symb M.empty) => nil | (int_symb M.empty) => nil | (hd_symb M.stack) => nil | (int_symb M.stack) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.pushs) => nil | (int_symb M.pushs) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.pops) => nil | (int_symb M.pops) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.tops) => nil | (int_symb M.tops) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.istops) => nil | (int_symb M.istops) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.eqc) => nil | (int_symb M.eqc) => nil | (hd_symb M.nocalls) => nil | (int_symb M.nocalls) => nil | (hd_symb M.calls) => nil | (int_symb M.calls) => nil | (hd_symb M.push) => nil | (int_symb M.push) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: nil | (hd_symb M.push1) => nil | (int_symb M.push1) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))))) :: nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS3. Module PI3 := PolyInt PIS3. (* polynomial interpretation 4 *) Module PIS4 (*<: TPolyInt*). Definition sig := s1. Definition trsInt f := match f as f return poly (@ASignature.arity s1 f) with | (hd_symb M.or) => nil | (int_symb M.or) => nil | (hd_symb M.T) => nil | (int_symb M.T) => nil | (hd_symb M.F) => nil | (int_symb M.F) => nil | (hd_symb M.and) => nil | (int_symb M.and) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.imp) => nil | (int_symb M.imp) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.not) => nil | (int_symb M.not) => (3%Z, (Vcons 0 Vnil)) :: nil | (hd_symb M._if_2) => nil | (int_symb M._if_2) => (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.eq) => nil | (int_symb M.eq) => nil | (hd_symb M.eqt) => nil | (int_symb M.eqt) => nil | (hd_symb M.nil) => nil | (int_symb M.nil) => nil | (hd_symb M.undefined) => nil | (int_symb M.undefined) => nil | (hd_symb M.pid) => nil | (int_symb M.pid) => nil | (hd_symb M.int) => nil | (int_symb M.int) => nil | (hd_symb M.cons) => nil | (int_symb M.cons) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.tuple) => nil | (int_symb M.tuple) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.tuplenil) => nil | (int_symb M.tuplenil) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a) => nil | (int_symb M.a) => nil | (hd_symb M.excl) => nil | (int_symb M.excl) => nil | (hd_symb M.false) => nil | (int_symb M.false) => nil | (hd_symb M.lock) => nil | (int_symb M.lock) => nil | (hd_symb M.locker) => nil | (int_symb M.locker) => nil | (hd_symb M.mcrlrecord) => nil | (int_symb M.mcrlrecord) => nil | (hd_symb M.ok) => nil | (int_symb M.ok) => nil | (hd_symb M.pending) => nil | (int_symb M.pending) => nil | (hd_symb M.release) => nil | (int_symb M.release) => nil | (hd_symb M.request) => nil | (int_symb M.request) => nil | (hd_symb M.resource) => nil | (int_symb M.resource) => nil | (hd_symb M.tag) => nil | (int_symb M.tag) => nil | (hd_symb M.true) => nil | (int_symb M.true) => (1%Z, Vnil) :: nil | (hd_symb M.element) => nil | (int_symb M.element) => (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.s) => nil | (int_symb M.s) => nil | (hd_symb M._0_1) => nil | (int_symb M._0_1) => nil | (hd_symb M.record_new) => nil | (int_symb M.record_new) => (1%Z, (Vcons 0 Vnil)) :: nil | (hd_symb M.record_extract) => nil | (int_symb M.record_extract) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.record_update) => nil | (int_symb M.record_update) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))) :: nil | (hd_symb M.record_updates) => nil | (int_symb M.record_updates) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.locker2_map_promote_pending) => nil | (int_symb M.locker2_map_promote_pending) => (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_promote_pending) => nil | (int_symb M.locker2_promote_pending) => (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_map_claim_lock) => nil | (int_symb M.locker2_map_claim_lock) => (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_claim_lock) => nil | (int_symb M.locker2_claim_lock) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_map_add_pending) => nil | (int_symb M.locker2_map_add_pending) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.case0) => nil | (int_symb M.case0) => (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.locker2_remove_pending) => nil | (int_symb M.locker2_remove_pending) => (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.subtract) => nil | (int_symb M.subtract) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_add_pending) => nil | (int_symb M.locker2_add_pending) => (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (3%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.case1) => nil | (int_symb M.case1) => (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: (3%Z, (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))) :: nil | (hd_symb M.member) => nil | (int_symb M.member) => nil | (hd_symb M.append) => nil | (int_symb M.append) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_release_lock) => nil | (int_symb M.locker2_release_lock) => (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.case2) => nil | (int_symb M.case2) => (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: nil | (hd_symb M.gen_modtageq) => nil | (int_symb M.gen_modtageq) => nil | (hd_symb M.excllock) => nil | (int_symb M.excllock) => nil | (hd_symb M.case4) => nil | (int_symb M.case4) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_obtainables) => nil | (int_symb M.locker2_obtainables) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (hd_symb M.case5) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))) :: nil | (int_symb M.case5) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: nil | (hd_symb M.andt) => nil | (int_symb M.andt) => nil | (hd_symb M.locker2_obtainable) => nil | (int_symb M.locker2_obtainable) => nil | (hd_symb M.locker2_check_available) => nil | (int_symb M.locker2_check_available) => nil | (hd_symb M.case6) => nil | (int_symb M.case6) => nil | (hd_symb M.equal) => nil | (int_symb M.equal) => nil | (hd_symb M.locker2_check_availables) => nil | (int_symb M.locker2_check_availables) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: (3%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.locker2_adduniq) => nil | (int_symb M.locker2_adduniq) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.delete) => nil | (int_symb M.delete) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.case8) => nil | (int_symb M.case8) => (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: nil | (hd_symb M.gen_tag) => nil | (int_symb M.gen_tag) => (3%Z, (Vcons 0 Vnil)) :: (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.case9) => nil | (int_symb M.case9) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))) :: nil | (hd_symb M.eqs) => nil | (int_symb M.eqs) => nil | (hd_symb M.empty) => nil | (int_symb M.empty) => nil | (hd_symb M.stack) => nil | (int_symb M.stack) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.pushs) => nil | (int_symb M.pushs) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.pops) => nil | (int_symb M.pops) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.tops) => nil | (int_symb M.tops) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.istops) => nil | (int_symb M.istops) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.eqc) => nil | (int_symb M.eqc) => nil | (hd_symb M.nocalls) => nil | (int_symb M.nocalls) => (1%Z, Vnil) :: nil | (hd_symb M.calls) => nil | (int_symb M.calls) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.push) => nil | (int_symb M.push) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.push1) => nil | (int_symb M.push1) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))))) :: (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))))) :: nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS4. Module PI4 := PolyInt PIS4. (* polynomial interpretation 5 *) Module PIS5 (*<: TPolyInt*). Definition sig := s1. Definition trsInt f := match f as f return poly (@ASignature.arity s1 f) with | (hd_symb M.or) => nil | (int_symb M.or) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (hd_symb M.T) => nil | (int_symb M.T) => nil | (hd_symb M.F) => nil | (int_symb M.F) => nil | (hd_symb M.and) => nil | (int_symb M.and) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.imp) => nil | (int_symb M.imp) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.not) => nil | (int_symb M.not) => nil | (hd_symb M._if_2) => nil | (int_symb M._if_2) => (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.eq) => nil | (int_symb M.eq) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (hd_symb M.eqt) => nil | (int_symb M.eqt) => nil | (hd_symb M.nil) => nil | (int_symb M.nil) => nil | (hd_symb M.undefined) => nil | (int_symb M.undefined) => nil | (hd_symb M.pid) => nil | (int_symb M.pid) => nil | (hd_symb M.int) => nil | (int_symb M.int) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.cons) => nil | (int_symb M.cons) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.tuple) => nil | (int_symb M.tuple) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.tuplenil) => nil | (int_symb M.tuplenil) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a) => nil | (int_symb M.a) => nil | (hd_symb M.excl) => nil | (int_symb M.excl) => nil | (hd_symb M.false) => nil | (int_symb M.false) => nil | (hd_symb M.lock) => nil | (int_symb M.lock) => nil | (hd_symb M.locker) => nil | (int_symb M.locker) => nil | (hd_symb M.mcrlrecord) => nil | (int_symb M.mcrlrecord) => nil | (hd_symb M.ok) => nil | (int_symb M.ok) => nil | (hd_symb M.pending) => nil | (int_symb M.pending) => nil | (hd_symb M.release) => nil | (int_symb M.release) => nil | (hd_symb M.request) => nil | (int_symb M.request) => nil | (hd_symb M.resource) => nil | (int_symb M.resource) => nil | (hd_symb M.tag) => nil | (int_symb M.tag) => (1%Z, Vnil) :: nil | (hd_symb M.true) => nil | (int_symb M.true) => nil | (hd_symb M.element) => nil | (int_symb M.element) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.s) => nil | (int_symb M.s) => (3%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M._0_1) => nil | (int_symb M._0_1) => nil | (hd_symb M.record_new) => nil | (int_symb M.record_new) => (1%Z, (Vcons 0 Vnil)) :: nil | (hd_symb M.record_extract) => nil | (int_symb M.record_extract) => (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.record_update) => nil | (int_symb M.record_update) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))) :: nil | (hd_symb M.record_updates) => nil | (int_symb M.record_updates) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.locker2_map_promote_pending) => nil | (int_symb M.locker2_map_promote_pending) => (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_promote_pending) => nil | (int_symb M.locker2_promote_pending) => (3%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_map_claim_lock) => nil | (int_symb M.locker2_map_claim_lock) => (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_claim_lock) => nil | (int_symb M.locker2_claim_lock) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_map_add_pending) => nil | (int_symb M.locker2_map_add_pending) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.case0) => nil | (int_symb M.case0) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.locker2_remove_pending) => nil | (int_symb M.locker2_remove_pending) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.subtract) => nil | (int_symb M.subtract) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_add_pending) => nil | (int_symb M.locker2_add_pending) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (3%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.case1) => nil | (int_symb M.case1) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: (3%Z, (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))) :: nil | (hd_symb M.member) => nil | (int_symb M.member) => nil | (hd_symb M.append) => nil | (int_symb M.append) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_release_lock) => nil | (int_symb M.locker2_release_lock) => (3%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.case2) => nil | (int_symb M.case2) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: nil | (hd_symb M.gen_modtageq) => nil | (int_symb M.gen_modtageq) => (3%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: (3%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.excllock) => nil | (int_symb M.excllock) => nil | (hd_symb M.case4) => nil | (int_symb M.case4) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_obtainables) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (int_symb M.locker2_obtainables) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.case5) => (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: nil | (int_symb M.case5) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))) :: nil | (hd_symb M.andt) => nil | (int_symb M.andt) => nil | (hd_symb M.locker2_obtainable) => nil | (int_symb M.locker2_obtainable) => nil | (hd_symb M.locker2_check_available) => nil | (int_symb M.locker2_check_available) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (hd_symb M.case6) => nil | (int_symb M.case6) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: nil | (hd_symb M.equal) => nil | (int_symb M.equal) => nil | (hd_symb M.locker2_check_availables) => nil | (int_symb M.locker2_check_availables) => (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.locker2_adduniq) => nil | (int_symb M.locker2_adduniq) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.delete) => nil | (int_symb M.delete) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.case8) => nil | (int_symb M.case8) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: nil | (hd_symb M.gen_tag) => nil | (int_symb M.gen_tag) => (1%Z, (Vcons 0 Vnil)) :: (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.case9) => nil | (int_symb M.case9) => nil | (hd_symb M.eqs) => nil | (int_symb M.eqs) => nil | (hd_symb M.empty) => nil | (int_symb M.empty) => nil | (hd_symb M.stack) => nil | (int_symb M.stack) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.pushs) => nil | (int_symb M.pushs) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.pops) => nil | (int_symb M.pops) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.tops) => nil | (int_symb M.tops) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.istops) => nil | (int_symb M.istops) => (3%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (hd_symb M.eqc) => nil | (int_symb M.eqc) => nil | (hd_symb M.nocalls) => nil | (int_symb M.nocalls) => nil | (hd_symb M.calls) => nil | (int_symb M.calls) => nil | (hd_symb M.push) => nil | (int_symb M.push) => nil | (hd_symb M.push1) => nil | (int_symb M.push1) => nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS5. Module PI5 := PolyInt PIS5. (* graph decomposition 2 *) Definition cs2 : list (list (@ATrs.rule s1)) := ( R1 (S1.hcase5 (V1 0) (V1 1) (V1 2) (S1.false)) (S1.hlocker2_obtainables (V1 1) (V1 0)) :: nil) :: nil. (* polynomial interpretation 6 *) Module PIS6 (*<: TPolyInt*). Definition sig := s1. Definition trsInt f := match f as f return poly (@ASignature.arity s1 f) with | (hd_symb M.or) => nil | (int_symb M.or) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (hd_symb M.T) => nil | (int_symb M.T) => nil | (hd_symb M.F) => nil | (int_symb M.F) => nil | (hd_symb M.and) => nil | (int_symb M.and) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.imp) => nil | (int_symb M.imp) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.not) => nil | (int_symb M.not) => (1%Z, (Vcons 0 Vnil)) :: nil | (hd_symb M._if_2) => nil | (int_symb M._if_2) => (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.eq) => nil | (int_symb M.eq) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (hd_symb M.eqt) => nil | (int_symb M.eqt) => nil | (hd_symb M.nil) => nil | (int_symb M.nil) => nil | (hd_symb M.undefined) => nil | (int_symb M.undefined) => nil | (hd_symb M.pid) => nil | (int_symb M.pid) => nil | (hd_symb M.int) => nil | (int_symb M.int) => nil | (hd_symb M.cons) => nil | (int_symb M.cons) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.tuple) => nil | (int_symb M.tuple) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.tuplenil) => nil | (int_symb M.tuplenil) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a) => nil | (int_symb M.a) => nil | (hd_symb M.excl) => nil | (int_symb M.excl) => nil | (hd_symb M.false) => nil | (int_symb M.false) => nil | (hd_symb M.lock) => nil | (int_symb M.lock) => nil | (hd_symb M.locker) => nil | (int_symb M.locker) => nil | (hd_symb M.mcrlrecord) => nil | (int_symb M.mcrlrecord) => nil | (hd_symb M.ok) => nil | (int_symb M.ok) => nil | (hd_symb M.pending) => nil | (int_symb M.pending) => nil | (hd_symb M.release) => nil | (int_symb M.release) => nil | (hd_symb M.request) => nil | (int_symb M.request) => nil | (hd_symb M.resource) => nil | (int_symb M.resource) => (2%Z, Vnil) :: nil | (hd_symb M.tag) => nil | (int_symb M.tag) => nil | (hd_symb M.true) => nil | (int_symb M.true) => (2%Z, Vnil) :: nil | (hd_symb M.element) => nil | (int_symb M.element) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.s) => nil | (int_symb M.s) => nil | (hd_symb M._0_1) => nil | (int_symb M._0_1) => nil | (hd_symb M.record_new) => nil | (int_symb M.record_new) => nil | (hd_symb M.record_extract) => nil | (int_symb M.record_extract) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.record_update) => nil | (int_symb M.record_update) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))) :: nil | (hd_symb M.record_updates) => nil | (int_symb M.record_updates) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.locker2_map_promote_pending) => nil | (int_symb M.locker2_map_promote_pending) => (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_promote_pending) => nil | (int_symb M.locker2_promote_pending) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_map_claim_lock) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (int_symb M.locker2_map_claim_lock) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_claim_lock) => nil | (int_symb M.locker2_claim_lock) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_map_add_pending) => nil | (int_symb M.locker2_map_add_pending) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.case0) => nil | (int_symb M.case0) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.locker2_remove_pending) => nil | (int_symb M.locker2_remove_pending) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: (3%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.subtract) => nil | (int_symb M.subtract) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_add_pending) => nil | (int_symb M.locker2_add_pending) => (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.case1) => nil | (int_symb M.case1) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))) :: nil | (hd_symb M.member) => nil | (int_symb M.member) => nil | (hd_symb M.append) => nil | (int_symb M.append) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_release_lock) => nil | (int_symb M.locker2_release_lock) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (3%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.case2) => nil | (int_symb M.case2) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: nil | (hd_symb M.gen_modtageq) => nil | (int_symb M.gen_modtageq) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.excllock) => nil | (int_symb M.excllock) => nil | (hd_symb M.case4) => nil | (int_symb M.case4) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_obtainables) => nil | (int_symb M.locker2_obtainables) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.case5) => nil | (int_symb M.case5) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: (3%Z, (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))) :: nil | (hd_symb M.andt) => nil | (int_symb M.andt) => nil | (hd_symb M.locker2_obtainable) => nil | (int_symb M.locker2_obtainable) => nil | (hd_symb M.locker2_check_available) => nil | (int_symb M.locker2_check_available) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.case6) => nil | (int_symb M.case6) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))) :: nil | (hd_symb M.equal) => nil | (int_symb M.equal) => nil | (hd_symb M.locker2_check_availables) => nil | (int_symb M.locker2_check_availables) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.locker2_adduniq) => nil | (int_symb M.locker2_adduniq) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.delete) => nil | (int_symb M.delete) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.case8) => nil | (int_symb M.case8) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: nil | (hd_symb M.gen_tag) => nil | (int_symb M.gen_tag) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.case9) => nil | (int_symb M.case9) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))) :: nil | (hd_symb M.eqs) => nil | (int_symb M.eqs) => nil | (hd_symb M.empty) => nil | (int_symb M.empty) => nil | (hd_symb M.stack) => nil | (int_symb M.stack) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.pushs) => nil | (int_symb M.pushs) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.pops) => nil | (int_symb M.pops) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.tops) => nil | (int_symb M.tops) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.istops) => nil | (int_symb M.istops) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.eqc) => nil | (int_symb M.eqc) => nil | (hd_symb M.nocalls) => nil | (int_symb M.nocalls) => nil | (hd_symb M.calls) => nil | (int_symb M.calls) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.push) => nil | (int_symb M.push) => (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.push1) => nil | (int_symb M.push1) => (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))))) :: nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS6. Module PI6 := PolyInt PIS6. (* polynomial interpretation 7 *) Module PIS7 (*<: TPolyInt*). Definition sig := s1. Definition trsInt f := match f as f return poly (@ASignature.arity s1 f) with | (hd_symb M.or) => nil | (int_symb M.or) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (hd_symb M.T) => nil | (int_symb M.T) => nil | (hd_symb M.F) => nil | (int_symb M.F) => nil | (hd_symb M.and) => nil | (int_symb M.and) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.imp) => nil | (int_symb M.imp) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.not) => nil | (int_symb M.not) => (3%Z, (Vcons 0 Vnil)) :: nil | (hd_symb M._if_2) => nil | (int_symb M._if_2) => (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.eq) => nil | (int_symb M.eq) => nil | (hd_symb M.eqt) => nil | (int_symb M.eqt) => nil | (hd_symb M.nil) => nil | (int_symb M.nil) => nil | (hd_symb M.undefined) => nil | (int_symb M.undefined) => nil | (hd_symb M.pid) => nil | (int_symb M.pid) => nil | (hd_symb M.int) => nil | (int_symb M.int) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.cons) => nil | (int_symb M.cons) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.tuple) => nil | (int_symb M.tuple) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.tuplenil) => nil | (int_symb M.tuplenil) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a) => nil | (int_symb M.a) => nil | (hd_symb M.excl) => nil | (int_symb M.excl) => nil | (hd_symb M.false) => nil | (int_symb M.false) => (1%Z, Vnil) :: nil | (hd_symb M.lock) => nil | (int_symb M.lock) => nil | (hd_symb M.locker) => nil | (int_symb M.locker) => nil | (hd_symb M.mcrlrecord) => nil | (int_symb M.mcrlrecord) => nil | (hd_symb M.ok) => nil | (int_symb M.ok) => nil | (hd_symb M.pending) => nil | (int_symb M.pending) => nil | (hd_symb M.release) => nil | (int_symb M.release) => nil | (hd_symb M.request) => nil | (int_symb M.request) => nil | (hd_symb M.resource) => nil | (int_symb M.resource) => nil | (hd_symb M.tag) => nil | (int_symb M.tag) => nil | (hd_symb M.true) => nil | (int_symb M.true) => nil | (hd_symb M.element) => nil | (int_symb M.element) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.s) => nil | (int_symb M.s) => (3%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M._0_1) => nil | (int_symb M._0_1) => nil | (hd_symb M.record_new) => nil | (int_symb M.record_new) => nil | (hd_symb M.record_extract) => nil | (int_symb M.record_extract) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.record_update) => nil | (int_symb M.record_update) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))) :: nil | (hd_symb M.record_updates) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (int_symb M.record_updates) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.locker2_map_promote_pending) => nil | (int_symb M.locker2_map_promote_pending) => (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_promote_pending) => nil | (int_symb M.locker2_promote_pending) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_map_claim_lock) => nil | (int_symb M.locker2_map_claim_lock) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_claim_lock) => nil | (int_symb M.locker2_claim_lock) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_map_add_pending) => nil | (int_symb M.locker2_map_add_pending) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.case0) => nil | (int_symb M.case0) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.locker2_remove_pending) => nil | (int_symb M.locker2_remove_pending) => (3%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: (3%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.subtract) => nil | (int_symb M.subtract) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_add_pending) => nil | (int_symb M.locker2_add_pending) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (3%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.case1) => nil | (int_symb M.case1) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: (3%Z, (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))) :: nil | (hd_symb M.member) => nil | (int_symb M.member) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.append) => nil | (int_symb M.append) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_release_lock) => nil | (int_symb M.locker2_release_lock) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.case2) => nil | (int_symb M.case2) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: nil | (hd_symb M.gen_modtageq) => nil | (int_symb M.gen_modtageq) => (3%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.excllock) => nil | (int_symb M.excllock) => nil | (hd_symb M.case4) => nil | (int_symb M.case4) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_obtainables) => nil | (int_symb M.locker2_obtainables) => nil | (hd_symb M.case5) => nil | (int_symb M.case5) => nil | (hd_symb M.andt) => nil | (int_symb M.andt) => nil | (hd_symb M.locker2_obtainable) => nil | (int_symb M.locker2_obtainable) => nil | (hd_symb M.locker2_check_available) => nil | (int_symb M.locker2_check_available) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.case6) => nil | (int_symb M.case6) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))) :: nil | (hd_symb M.equal) => nil | (int_symb M.equal) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_check_availables) => nil | (int_symb M.locker2_check_availables) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.locker2_adduniq) => nil | (int_symb M.locker2_adduniq) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.delete) => nil | (int_symb M.delete) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.case8) => nil | (int_symb M.case8) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: nil | (hd_symb M.gen_tag) => nil | (int_symb M.gen_tag) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.case9) => nil | (int_symb M.case9) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))) :: nil | (hd_symb M.eqs) => nil | (int_symb M.eqs) => nil | (hd_symb M.empty) => nil | (int_symb M.empty) => nil | (hd_symb M.stack) => nil | (int_symb M.stack) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.pushs) => nil | (int_symb M.pushs) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (3%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.pops) => nil | (int_symb M.pops) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.tops) => nil | (int_symb M.tops) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.istops) => nil | (int_symb M.istops) => (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.eqc) => nil | (int_symb M.eqc) => nil | (hd_symb M.nocalls) => nil | (int_symb M.nocalls) => nil | (hd_symb M.calls) => nil | (int_symb M.calls) => nil | (hd_symb M.push) => nil | (int_symb M.push) => nil | (hd_symb M.push1) => nil | (int_symb M.push1) => nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS7. Module PI7 := PolyInt PIS7. (* polynomial interpretation 8 *) Module PIS8 (*<: TPolyInt*). Definition sig := s1. Definition trsInt f := match f as f return poly (@ASignature.arity s1 f) with | (hd_symb M.or) => nil | (int_symb M.or) => nil | (hd_symb M.T) => nil | (int_symb M.T) => nil | (hd_symb M.F) => nil | (int_symb M.F) => nil | (hd_symb M.and) => nil | (int_symb M.and) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.imp) => nil | (int_symb M.imp) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.not) => nil | (int_symb M.not) => (1%Z, (Vcons 0 Vnil)) :: nil | (hd_symb M._if_2) => nil | (int_symb M._if_2) => (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.eq) => nil | (int_symb M.eq) => nil | (hd_symb M.eqt) => nil | (int_symb M.eqt) => nil | (hd_symb M.nil) => nil | (int_symb M.nil) => nil | (hd_symb M.undefined) => nil | (int_symb M.undefined) => nil | (hd_symb M.pid) => nil | (int_symb M.pid) => nil | (hd_symb M.int) => nil | (int_symb M.int) => nil | (hd_symb M.cons) => nil | (int_symb M.cons) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.tuple) => nil | (int_symb M.tuple) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.tuplenil) => nil | (int_symb M.tuplenil) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a) => nil | (int_symb M.a) => nil | (hd_symb M.excl) => nil | (int_symb M.excl) => nil | (hd_symb M.false) => nil | (int_symb M.false) => nil | (hd_symb M.lock) => nil | (int_symb M.lock) => (1%Z, Vnil) :: nil | (hd_symb M.locker) => nil | (int_symb M.locker) => nil | (hd_symb M.mcrlrecord) => nil | (int_symb M.mcrlrecord) => nil | (hd_symb M.ok) => nil | (int_symb M.ok) => nil | (hd_symb M.pending) => nil | (int_symb M.pending) => nil | (hd_symb M.release) => nil | (int_symb M.release) => nil | (hd_symb M.request) => nil | (int_symb M.request) => nil | (hd_symb M.resource) => nil | (int_symb M.resource) => (1%Z, Vnil) :: nil | (hd_symb M.tag) => nil | (int_symb M.tag) => nil | (hd_symb M.true) => nil | (int_symb M.true) => nil | (hd_symb M.element) => nil | (int_symb M.element) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.s) => nil | (int_symb M.s) => nil | (hd_symb M._0_1) => nil | (int_symb M._0_1) => nil | (hd_symb M.record_new) => nil | (int_symb M.record_new) => (3%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.record_extract) => nil | (int_symb M.record_extract) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.record_update) => nil | (int_symb M.record_update) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))) :: nil | (hd_symb M.record_updates) => nil | (int_symb M.record_updates) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.locker2_map_promote_pending) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (int_symb M.locker2_map_promote_pending) => (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_promote_pending) => nil | (int_symb M.locker2_promote_pending) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_map_claim_lock) => nil | (int_symb M.locker2_map_claim_lock) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_claim_lock) => nil | (int_symb M.locker2_claim_lock) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_map_add_pending) => nil | (int_symb M.locker2_map_add_pending) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.case0) => nil | (int_symb M.case0) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.locker2_remove_pending) => nil | (int_symb M.locker2_remove_pending) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.subtract) => nil | (int_symb M.subtract) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_add_pending) => nil | (int_symb M.locker2_add_pending) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (3%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.case1) => nil | (int_symb M.case1) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))) :: nil | (hd_symb M.member) => nil | (int_symb M.member) => (3%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.append) => nil | (int_symb M.append) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_release_lock) => nil | (int_symb M.locker2_release_lock) => (3%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (3%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.case2) => nil | (int_symb M.case2) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: nil | (hd_symb M.gen_modtageq) => nil | (int_symb M.gen_modtageq) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.excllock) => nil | (int_symb M.excllock) => nil | (hd_symb M.case4) => nil | (int_symb M.case4) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_obtainables) => nil | (int_symb M.locker2_obtainables) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.case5) => nil | (int_symb M.case5) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: nil | (hd_symb M.andt) => nil | (int_symb M.andt) => nil | (hd_symb M.locker2_obtainable) => nil | (int_symb M.locker2_obtainable) => nil | (hd_symb M.locker2_check_available) => nil | (int_symb M.locker2_check_available) => nil | (hd_symb M.case6) => nil | (int_symb M.case6) => nil | (hd_symb M.equal) => nil | (int_symb M.equal) => nil | (hd_symb M.locker2_check_availables) => nil | (int_symb M.locker2_check_availables) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_adduniq) => nil | (int_symb M.locker2_adduniq) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.delete) => nil | (int_symb M.delete) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.case8) => nil | (int_symb M.case8) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: nil | (hd_symb M.gen_tag) => nil | (int_symb M.gen_tag) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.case9) => nil | (int_symb M.case9) => (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (3%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: nil | (hd_symb M.eqs) => nil | (int_symb M.eqs) => nil | (hd_symb M.empty) => nil | (int_symb M.empty) => nil | (hd_symb M.stack) => nil | (int_symb M.stack) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.pushs) => nil | (int_symb M.pushs) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.pops) => nil | (int_symb M.pops) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.tops) => nil | (int_symb M.tops) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.istops) => nil | (int_symb M.istops) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.eqc) => nil | (int_symb M.eqc) => nil | (hd_symb M.nocalls) => nil | (int_symb M.nocalls) => nil | (hd_symb M.calls) => nil | (int_symb M.calls) => nil | (hd_symb M.push) => nil | (int_symb M.push) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: nil | (hd_symb M.push1) => nil | (int_symb M.push1) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))))) :: nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS8. Module PI8 := PolyInt PIS8. (* polynomial interpretation 9 *) Module PIS9 (*<: TPolyInt*). Definition sig := s1. Definition trsInt f := match f as f return poly (@ASignature.arity s1 f) with | (hd_symb M.or) => nil | (int_symb M.or) => nil | (hd_symb M.T) => nil | (int_symb M.T) => nil | (hd_symb M.F) => nil | (int_symb M.F) => nil | (hd_symb M.and) => nil | (int_symb M.and) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.imp) => nil | (int_symb M.imp) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.not) => nil | (int_symb M.not) => (1%Z, (Vcons 0 Vnil)) :: nil | (hd_symb M._if_2) => nil | (int_symb M._if_2) => (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.eq) => nil | (int_symb M.eq) => nil | (hd_symb M.eqt) => nil | (int_symb M.eqt) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.nil) => nil | (int_symb M.nil) => nil | (hd_symb M.undefined) => nil | (int_symb M.undefined) => nil | (hd_symb M.pid) => nil | (int_symb M.pid) => (1%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.int) => nil | (int_symb M.int) => (1%Z, (Vcons 0 Vnil)) :: (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.cons) => nil | (int_symb M.cons) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.tuple) => nil | (int_symb M.tuple) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.tuplenil) => nil | (int_symb M.tuplenil) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a) => nil | (int_symb M.a) => (2%Z, Vnil) :: nil | (hd_symb M.excl) => nil | (int_symb M.excl) => nil | (hd_symb M.false) => nil | (int_symb M.false) => nil | (hd_symb M.lock) => nil | (int_symb M.lock) => nil | (hd_symb M.locker) => nil | (int_symb M.locker) => (2%Z, Vnil) :: nil | (hd_symb M.mcrlrecord) => nil | (int_symb M.mcrlrecord) => nil | (hd_symb M.ok) => nil | (int_symb M.ok) => nil | (hd_symb M.pending) => nil | (int_symb M.pending) => nil | (hd_symb M.release) => nil | (int_symb M.release) => nil | (hd_symb M.request) => nil | (int_symb M.request) => nil | (hd_symb M.resource) => nil | (int_symb M.resource) => (1%Z, Vnil) :: nil | (hd_symb M.tag) => nil | (int_symb M.tag) => (2%Z, Vnil) :: nil | (hd_symb M.true) => nil | (int_symb M.true) => nil | (hd_symb M.element) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (int_symb M.element) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.s) => nil | (int_symb M.s) => (1%Z, (Vcons 0 Vnil)) :: (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M._0_1) => nil | (int_symb M._0_1) => nil | (hd_symb M.record_new) => nil | (int_symb M.record_new) => nil | (hd_symb M.record_extract) => nil | (int_symb M.record_extract) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.record_update) => nil | (int_symb M.record_update) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (3%Z, (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))) :: nil | (hd_symb M.record_updates) => nil | (int_symb M.record_updates) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.locker2_map_promote_pending) => nil | (int_symb M.locker2_map_promote_pending) => (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_promote_pending) => nil | (int_symb M.locker2_promote_pending) => (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_map_claim_lock) => nil | (int_symb M.locker2_map_claim_lock) => nil | (hd_symb M.locker2_claim_lock) => nil | (int_symb M.locker2_claim_lock) => nil | (hd_symb M.locker2_map_add_pending) => nil | (int_symb M.locker2_map_add_pending) => nil | (hd_symb M.case0) => nil | (int_symb M.case0) => (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.locker2_remove_pending) => nil | (int_symb M.locker2_remove_pending) => (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.subtract) => nil | (int_symb M.subtract) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_add_pending) => nil | (int_symb M.locker2_add_pending) => (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.case1) => nil | (int_symb M.case1) => (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: (3%Z, (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))) :: nil | (hd_symb M.member) => nil | (int_symb M.member) => nil | (hd_symb M.append) => nil | (int_symb M.append) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_release_lock) => nil | (int_symb M.locker2_release_lock) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.case2) => nil | (int_symb M.case2) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: nil | (hd_symb M.gen_modtageq) => nil | (int_symb M.gen_modtageq) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (hd_symb M.excllock) => nil | (int_symb M.excllock) => nil | (hd_symb M.case4) => nil | (int_symb M.case4) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_obtainables) => nil | (int_symb M.locker2_obtainables) => nil | (hd_symb M.case5) => nil | (int_symb M.case5) => nil | (hd_symb M.andt) => nil | (int_symb M.andt) => nil | (hd_symb M.locker2_obtainable) => nil | (int_symb M.locker2_obtainable) => nil | (hd_symb M.locker2_check_available) => nil | (int_symb M.locker2_check_available) => nil | (hd_symb M.case6) => nil | (int_symb M.case6) => nil | (hd_symb M.equal) => nil | (int_symb M.equal) => nil | (hd_symb M.locker2_check_availables) => nil | (int_symb M.locker2_check_availables) => (3%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.locker2_adduniq) => nil | (int_symb M.locker2_adduniq) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.delete) => nil | (int_symb M.delete) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.case8) => nil | (int_symb M.case8) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: nil | (hd_symb M.gen_tag) => nil | (int_symb M.gen_tag) => (3%Z, (Vcons 0 Vnil)) :: (3%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.case9) => nil | (int_symb M.case9) => nil | (hd_symb M.eqs) => nil | (int_symb M.eqs) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.empty) => nil | (int_symb M.empty) => nil | (hd_symb M.stack) => nil | (int_symb M.stack) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.pushs) => nil | (int_symb M.pushs) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.pops) => nil | (int_symb M.pops) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.tops) => nil | (int_symb M.tops) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.istops) => nil | (int_symb M.istops) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.eqc) => nil | (int_symb M.eqc) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.nocalls) => nil | (int_symb M.nocalls) => nil | (hd_symb M.calls) => nil | (int_symb M.calls) => (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.push) => nil | (int_symb M.push) => (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (3%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.push1) => nil | (int_symb M.push1) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))))) :: (3%Z, (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))))) :: nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS9. Module PI9 := PolyInt PIS9. (* polynomial interpretation 10 *) Module PIS10 (*<: TPolyInt*). Definition sig := s1. Definition trsInt f := match f as f return poly (@ASignature.arity s1 f) with | (hd_symb M.or) => nil | (int_symb M.or) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (hd_symb M.T) => nil | (int_symb M.T) => nil | (hd_symb M.F) => nil | (int_symb M.F) => nil | (hd_symb M.and) => nil | (int_symb M.and) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.imp) => nil | (int_symb M.imp) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.not) => nil | (int_symb M.not) => (1%Z, (Vcons 0 Vnil)) :: nil | (hd_symb M._if_2) => nil | (int_symb M._if_2) => (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.eq) => nil | (int_symb M.eq) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (hd_symb M.eqt) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (int_symb M.eqt) => nil | (hd_symb M.nil) => nil | (int_symb M.nil) => nil | (hd_symb M.undefined) => nil | (int_symb M.undefined) => nil | (hd_symb M.pid) => nil | (int_symb M.pid) => (3%Z, (Vcons 0 Vnil)) :: (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.int) => nil | (int_symb M.int) => nil | (hd_symb M.cons) => nil | (int_symb M.cons) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.tuple) => nil | (int_symb M.tuple) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.tuplenil) => nil | (int_symb M.tuplenil) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a) => nil | (int_symb M.a) => nil | (hd_symb M.excl) => nil | (int_symb M.excl) => nil | (hd_symb M.false) => nil | (int_symb M.false) => nil | (hd_symb M.lock) => nil | (int_symb M.lock) => nil | (hd_symb M.locker) => nil | (int_symb M.locker) => nil | (hd_symb M.mcrlrecord) => nil | (int_symb M.mcrlrecord) => nil | (hd_symb M.ok) => nil | (int_symb M.ok) => nil | (hd_symb M.pending) => nil | (int_symb M.pending) => nil | (hd_symb M.release) => nil | (int_symb M.release) => nil | (hd_symb M.request) => nil | (int_symb M.request) => nil | (hd_symb M.resource) => nil | (int_symb M.resource) => nil | (hd_symb M.tag) => nil | (int_symb M.tag) => nil | (hd_symb M.true) => nil | (int_symb M.true) => nil | (hd_symb M.element) => nil | (int_symb M.element) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.s) => nil | (int_symb M.s) => nil | (hd_symb M._0_1) => nil | (int_symb M._0_1) => nil | (hd_symb M.record_new) => nil | (int_symb M.record_new) => (1%Z, (Vcons 0 Vnil)) :: nil | (hd_symb M.record_extract) => nil | (int_symb M.record_extract) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.record_update) => nil | (int_symb M.record_update) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))) :: nil | (hd_symb M.record_updates) => nil | (int_symb M.record_updates) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.locker2_map_promote_pending) => nil | (int_symb M.locker2_map_promote_pending) => (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_promote_pending) => nil | (int_symb M.locker2_promote_pending) => (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_map_claim_lock) => nil | (int_symb M.locker2_map_claim_lock) => (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_claim_lock) => nil | (int_symb M.locker2_claim_lock) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_map_add_pending) => nil | (int_symb M.locker2_map_add_pending) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.case0) => nil | (int_symb M.case0) => (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.locker2_remove_pending) => nil | (int_symb M.locker2_remove_pending) => (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.subtract) => nil | (int_symb M.subtract) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_add_pending) => nil | (int_symb M.locker2_add_pending) => (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (3%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.case1) => nil | (int_symb M.case1) => (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: (3%Z, (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))) :: nil | (hd_symb M.member) => nil | (int_symb M.member) => nil | (hd_symb M.append) => nil | (int_symb M.append) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_release_lock) => nil | (int_symb M.locker2_release_lock) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.case2) => nil | (int_symb M.case2) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: nil | (hd_symb M.gen_modtageq) => nil | (int_symb M.gen_modtageq) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.excllock) => nil | (int_symb M.excllock) => nil | (hd_symb M.case4) => nil | (int_symb M.case4) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_obtainables) => nil | (int_symb M.locker2_obtainables) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.case5) => nil | (int_symb M.case5) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: nil | (hd_symb M.andt) => nil | (int_symb M.andt) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_obtainable) => nil | (int_symb M.locker2_obtainable) => nil | (hd_symb M.locker2_check_available) => nil | (int_symb M.locker2_check_available) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.case6) => nil | (int_symb M.case6) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: nil | (hd_symb M.equal) => nil | (int_symb M.equal) => nil | (hd_symb M.locker2_check_availables) => nil | (int_symb M.locker2_check_availables) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.locker2_adduniq) => nil | (int_symb M.locker2_adduniq) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.delete) => nil | (int_symb M.delete) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.case8) => nil | (int_symb M.case8) => (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: nil | (hd_symb M.gen_tag) => nil | (int_symb M.gen_tag) => (3%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.case9) => nil | (int_symb M.case9) => nil | (hd_symb M.eqs) => nil | (int_symb M.eqs) => nil | (hd_symb M.empty) => nil | (int_symb M.empty) => nil | (hd_symb M.stack) => nil | (int_symb M.stack) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.pushs) => nil | (int_symb M.pushs) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.pops) => nil | (int_symb M.pops) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.tops) => nil | (int_symb M.tops) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.istops) => nil | (int_symb M.istops) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.eqc) => nil | (int_symb M.eqc) => nil | (hd_symb M.nocalls) => nil | (int_symb M.nocalls) => (2%Z, Vnil) :: nil | (hd_symb M.calls) => nil | (int_symb M.calls) => nil | (hd_symb M.push) => nil | (int_symb M.push) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (3%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.push1) => nil | (int_symb M.push1) => nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS10. Module PI10 := PolyInt PIS10. (* polynomial interpretation 11 *) Module PIS11 (*<: TPolyInt*). Definition sig := s1. Definition trsInt f := match f as f return poly (@ASignature.arity s1 f) with | (hd_symb M.or) => nil | (int_symb M.or) => nil | (hd_symb M.T) => nil | (int_symb M.T) => nil | (hd_symb M.F) => nil | (int_symb M.F) => nil | (hd_symb M.and) => nil | (int_symb M.and) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.imp) => nil | (int_symb M.imp) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.not) => nil | (int_symb M.not) => nil | (hd_symb M._if_2) => nil | (int_symb M._if_2) => (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.eq) => nil | (int_symb M.eq) => nil | (hd_symb M.eqt) => (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: (3%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (int_symb M.eqt) => nil | (hd_symb M.nil) => nil | (int_symb M.nil) => nil | (hd_symb M.undefined) => nil | (int_symb M.undefined) => nil | (hd_symb M.pid) => nil | (int_symb M.pid) => nil | (hd_symb M.int) => nil | (int_symb M.int) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.cons) => nil | (int_symb M.cons) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.tuple) => nil | (int_symb M.tuple) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.tuplenil) => nil | (int_symb M.tuplenil) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a) => nil | (int_symb M.a) => nil | (hd_symb M.excl) => nil | (int_symb M.excl) => nil | (hd_symb M.false) => nil | (int_symb M.false) => (2%Z, Vnil) :: nil | (hd_symb M.lock) => nil | (int_symb M.lock) => nil | (hd_symb M.locker) => nil | (int_symb M.locker) => nil | (hd_symb M.mcrlrecord) => nil | (int_symb M.mcrlrecord) => nil | (hd_symb M.ok) => nil | (int_symb M.ok) => nil | (hd_symb M.pending) => nil | (int_symb M.pending) => nil | (hd_symb M.release) => nil | (int_symb M.release) => nil | (hd_symb M.request) => nil | (int_symb M.request) => nil | (hd_symb M.resource) => nil | (int_symb M.resource) => nil | (hd_symb M.tag) => nil | (int_symb M.tag) => nil | (hd_symb M.true) => nil | (int_symb M.true) => nil | (hd_symb M.element) => nil | (int_symb M.element) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.s) => nil | (int_symb M.s) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M._0_1) => nil | (int_symb M._0_1) => nil | (hd_symb M.record_new) => nil | (int_symb M.record_new) => (1%Z, (Vcons 0 Vnil)) :: nil | (hd_symb M.record_extract) => nil | (int_symb M.record_extract) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.record_update) => nil | (int_symb M.record_update) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))) :: nil | (hd_symb M.record_updates) => nil | (int_symb M.record_updates) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.locker2_map_promote_pending) => nil | (int_symb M.locker2_map_promote_pending) => (3%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_promote_pending) => nil | (int_symb M.locker2_promote_pending) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_map_claim_lock) => nil | (int_symb M.locker2_map_claim_lock) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_claim_lock) => nil | (int_symb M.locker2_claim_lock) => nil | (hd_symb M.locker2_map_add_pending) => nil | (int_symb M.locker2_map_add_pending) => nil | (hd_symb M.case0) => nil | (int_symb M.case0) => (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.locker2_remove_pending) => nil | (int_symb M.locker2_remove_pending) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: (3%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.subtract) => nil | (int_symb M.subtract) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_add_pending) => nil | (int_symb M.locker2_add_pending) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (3%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.case1) => nil | (int_symb M.case1) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: (3%Z, (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))) :: nil | (hd_symb M.member) => nil | (int_symb M.member) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (hd_symb M.append) => nil | (int_symb M.append) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_release_lock) => nil | (int_symb M.locker2_release_lock) => (3%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.case2) => nil | (int_symb M.case2) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: nil | (hd_symb M.gen_modtageq) => nil | (int_symb M.gen_modtageq) => (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.excllock) => nil | (int_symb M.excllock) => nil | (hd_symb M.case4) => nil | (int_symb M.case4) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_obtainables) => nil | (int_symb M.locker2_obtainables) => nil | (hd_symb M.case5) => nil | (int_symb M.case5) => nil | (hd_symb M.andt) => nil | (int_symb M.andt) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_obtainable) => nil | (int_symb M.locker2_obtainable) => nil | (hd_symb M.locker2_check_available) => nil | (int_symb M.locker2_check_available) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (hd_symb M.case6) => nil | (int_symb M.case6) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))) :: nil | (hd_symb M.equal) => nil | (int_symb M.equal) => nil | (hd_symb M.locker2_check_availables) => nil | (int_symb M.locker2_check_availables) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.locker2_adduniq) => nil | (int_symb M.locker2_adduniq) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.delete) => nil | (int_symb M.delete) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.case8) => nil | (int_symb M.case8) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: nil | (hd_symb M.gen_tag) => nil | (int_symb M.gen_tag) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.case9) => nil | (int_symb M.case9) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))) :: nil | (hd_symb M.eqs) => nil | (int_symb M.eqs) => nil | (hd_symb M.empty) => nil | (int_symb M.empty) => nil | (hd_symb M.stack) => nil | (int_symb M.stack) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.pushs) => nil | (int_symb M.pushs) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.pops) => nil | (int_symb M.pops) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.tops) => nil | (int_symb M.tops) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.istops) => nil | (int_symb M.istops) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.eqc) => nil | (int_symb M.eqc) => nil | (hd_symb M.nocalls) => nil | (int_symb M.nocalls) => nil | (hd_symb M.calls) => nil | (int_symb M.calls) => nil | (hd_symb M.push) => nil | (int_symb M.push) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (3%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: nil | (hd_symb M.push1) => nil | (int_symb M.push1) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))))) :: (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))))) :: nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS11. Module PI11 := PolyInt PIS11. (* polynomial interpretation 12 *) Module PIS12 (*<: TPolyInt*). Definition sig := s1. Definition trsInt f := match f as f return poly (@ASignature.arity s1 f) with | (hd_symb M.or) => nil | (int_symb M.or) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (hd_symb M.T) => nil | (int_symb M.T) => nil | (hd_symb M.F) => nil | (int_symb M.F) => nil | (hd_symb M.and) => nil | (int_symb M.and) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.imp) => nil | (int_symb M.imp) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.not) => nil | (int_symb M.not) => (2%Z, (Vcons 0 Vnil)) :: nil | (hd_symb M._if_2) => nil | (int_symb M._if_2) => (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.eq) => nil | (int_symb M.eq) => nil | (hd_symb M.eqt) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (int_symb M.eqt) => nil | (hd_symb M.nil) => nil | (int_symb M.nil) => nil | (hd_symb M.undefined) => nil | (int_symb M.undefined) => nil | (hd_symb M.pid) => nil | (int_symb M.pid) => nil | (hd_symb M.int) => nil | (int_symb M.int) => nil | (hd_symb M.cons) => nil | (int_symb M.cons) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.tuple) => nil | (int_symb M.tuple) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.tuplenil) => nil | (int_symb M.tuplenil) => (1%Z, (Vcons 0 Vnil)) :: (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a) => nil | (int_symb M.a) => nil | (hd_symb M.excl) => nil | (int_symb M.excl) => nil | (hd_symb M.false) => nil | (int_symb M.false) => (2%Z, Vnil) :: nil | (hd_symb M.lock) => nil | (int_symb M.lock) => nil | (hd_symb M.locker) => nil | (int_symb M.locker) => nil | (hd_symb M.mcrlrecord) => nil | (int_symb M.mcrlrecord) => nil | (hd_symb M.ok) => nil | (int_symb M.ok) => nil | (hd_symb M.pending) => nil | (int_symb M.pending) => nil | (hd_symb M.release) => nil | (int_symb M.release) => nil | (hd_symb M.request) => nil | (int_symb M.request) => nil | (hd_symb M.resource) => nil | (int_symb M.resource) => nil | (hd_symb M.tag) => nil | (int_symb M.tag) => nil | (hd_symb M.true) => nil | (int_symb M.true) => nil | (hd_symb M.element) => nil | (int_symb M.element) => (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.s) => nil | (int_symb M.s) => nil | (hd_symb M._0_1) => nil | (int_symb M._0_1) => nil | (hd_symb M.record_new) => nil | (int_symb M.record_new) => (1%Z, (Vcons 0 Vnil)) :: nil | (hd_symb M.record_extract) => nil | (int_symb M.record_extract) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.record_update) => nil | (int_symb M.record_update) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))) :: nil | (hd_symb M.record_updates) => nil | (int_symb M.record_updates) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.locker2_map_promote_pending) => nil | (int_symb M.locker2_map_promote_pending) => (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_promote_pending) => nil | (int_symb M.locker2_promote_pending) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_map_claim_lock) => nil | (int_symb M.locker2_map_claim_lock) => (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_claim_lock) => nil | (int_symb M.locker2_claim_lock) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_map_add_pending) => nil | (int_symb M.locker2_map_add_pending) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.case0) => nil | (int_symb M.case0) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.locker2_remove_pending) => nil | (int_symb M.locker2_remove_pending) => (3%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.subtract) => nil | (int_symb M.subtract) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_add_pending) => nil | (int_symb M.locker2_add_pending) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.case1) => nil | (int_symb M.case1) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: (3%Z, (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))) :: nil | (hd_symb M.member) => nil | (int_symb M.member) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (hd_symb M.append) => nil | (int_symb M.append) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_release_lock) => nil | (int_symb M.locker2_release_lock) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.case2) => nil | (int_symb M.case2) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: nil | (hd_symb M.gen_modtageq) => nil | (int_symb M.gen_modtageq) => (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: (3%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.excllock) => nil | (int_symb M.excllock) => nil | (hd_symb M.case4) => nil | (int_symb M.case4) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_obtainables) => nil | (int_symb M.locker2_obtainables) => (3%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.case5) => nil | (int_symb M.case5) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: nil | (hd_symb M.andt) => nil | (int_symb M.andt) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_obtainable) => nil | (int_symb M.locker2_obtainable) => nil | (hd_symb M.locker2_check_available) => nil | (int_symb M.locker2_check_available) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (hd_symb M.case6) => nil | (int_symb M.case6) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))) :: nil | (hd_symb M.equal) => nil | (int_symb M.equal) => nil | (hd_symb M.locker2_check_availables) => nil | (int_symb M.locker2_check_availables) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_adduniq) => nil | (int_symb M.locker2_adduniq) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.delete) => nil | (int_symb M.delete) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.case8) => nil | (int_symb M.case8) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))) :: nil | (hd_symb M.gen_tag) => nil | (int_symb M.gen_tag) => (2%Z, (Vcons 0 Vnil)) :: (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.case9) => nil | (int_symb M.case9) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))) :: nil | (hd_symb M.eqs) => nil | (int_symb M.eqs) => nil | (hd_symb M.empty) => nil | (int_symb M.empty) => nil | (hd_symb M.stack) => nil | (int_symb M.stack) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.pushs) => nil | (int_symb M.pushs) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.pops) => nil | (int_symb M.pops) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.tops) => nil | (int_symb M.tops) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.istops) => nil | (int_symb M.istops) => nil | (hd_symb M.eqc) => nil | (int_symb M.eqc) => nil | (hd_symb M.nocalls) => nil | (int_symb M.nocalls) => nil | (hd_symb M.calls) => nil | (int_symb M.calls) => nil | (hd_symb M.push) => nil | (int_symb M.push) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: nil | (hd_symb M.push1) => nil | (int_symb M.push1) => nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS12. Module PI12 := PolyInt PIS12. (* polynomial interpretation 13 *) Module PIS13 (*<: TPolyInt*). Definition sig := s1. Definition trsInt f := match f as f return poly (@ASignature.arity s1 f) with | (hd_symb M.or) => nil | (int_symb M.or) => nil | (hd_symb M.T) => nil | (int_symb M.T) => nil | (hd_symb M.F) => nil | (int_symb M.F) => nil | (hd_symb M.and) => nil | (int_symb M.and) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.imp) => nil | (int_symb M.imp) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.not) => nil | (int_symb M.not) => (3%Z, (Vcons 0 Vnil)) :: nil | (hd_symb M._if_2) => nil | (int_symb M._if_2) => (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.eq) => nil | (int_symb M.eq) => nil | (hd_symb M.eqt) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (int_symb M.eqt) => nil | (hd_symb M.nil) => nil | (int_symb M.nil) => nil | (hd_symb M.undefined) => nil | (int_symb M.undefined) => nil | (hd_symb M.pid) => nil | (int_symb M.pid) => nil | (hd_symb M.int) => nil | (int_symb M.int) => nil | (hd_symb M.cons) => nil | (int_symb M.cons) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.tuple) => nil | (int_symb M.tuple) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.tuplenil) => nil | (int_symb M.tuplenil) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a) => nil | (int_symb M.a) => nil | (hd_symb M.excl) => nil | (int_symb M.excl) => nil | (hd_symb M.false) => nil | (int_symb M.false) => nil | (hd_symb M.lock) => nil | (int_symb M.lock) => (2%Z, Vnil) :: nil | (hd_symb M.locker) => nil | (int_symb M.locker) => nil | (hd_symb M.mcrlrecord) => nil | (int_symb M.mcrlrecord) => nil | (hd_symb M.ok) => nil | (int_symb M.ok) => nil | (hd_symb M.pending) => nil | (int_symb M.pending) => nil | (hd_symb M.release) => nil | (int_symb M.release) => nil | (hd_symb M.request) => nil | (int_symb M.request) => nil | (hd_symb M.resource) => nil | (int_symb M.resource) => nil | (hd_symb M.tag) => nil | (int_symb M.tag) => nil | (hd_symb M.true) => nil | (int_symb M.true) => nil | (hd_symb M.element) => nil | (int_symb M.element) => (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.s) => nil | (int_symb M.s) => nil | (hd_symb M._0_1) => nil | (int_symb M._0_1) => nil | (hd_symb M.record_new) => nil | (int_symb M.record_new) => (3%Z, (Vcons 0 Vnil)) :: (3%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.record_extract) => nil | (int_symb M.record_extract) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.record_update) => nil | (int_symb M.record_update) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))) :: nil | (hd_symb M.record_updates) => nil | (int_symb M.record_updates) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.locker2_map_promote_pending) => nil | (int_symb M.locker2_map_promote_pending) => (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_promote_pending) => nil | (int_symb M.locker2_promote_pending) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_map_claim_lock) => nil | (int_symb M.locker2_map_claim_lock) => (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_claim_lock) => nil | (int_symb M.locker2_claim_lock) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_map_add_pending) => nil | (int_symb M.locker2_map_add_pending) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.case0) => nil | (int_symb M.case0) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.locker2_remove_pending) => nil | (int_symb M.locker2_remove_pending) => (3%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.subtract) => nil | (int_symb M.subtract) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_add_pending) => nil | (int_symb M.locker2_add_pending) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (3%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.case1) => nil | (int_symb M.case1) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: (3%Z, (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))) :: nil | (hd_symb M.member) => nil | (int_symb M.member) => (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.append) => nil | (int_symb M.append) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_release_lock) => nil | (int_symb M.locker2_release_lock) => (3%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.case2) => nil | (int_symb M.case2) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: nil | (hd_symb M.gen_modtageq) => nil | (int_symb M.gen_modtageq) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.excllock) => nil | (int_symb M.excllock) => nil | (hd_symb M.case4) => nil | (int_symb M.case4) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_obtainables) => nil | (int_symb M.locker2_obtainables) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (hd_symb M.case5) => nil | (int_symb M.case5) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: nil | (hd_symb M.andt) => nil | (int_symb M.andt) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_obtainable) => nil | (int_symb M.locker2_obtainable) => nil | (hd_symb M.locker2_check_available) => nil | (int_symb M.locker2_check_available) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (hd_symb M.case6) => nil | (int_symb M.case6) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: nil | (hd_symb M.equal) => nil | (int_symb M.equal) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_check_availables) => nil | (int_symb M.locker2_check_availables) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_adduniq) => nil | (int_symb M.locker2_adduniq) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.delete) => nil | (int_symb M.delete) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.case8) => nil | (int_symb M.case8) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: nil | (hd_symb M.gen_tag) => nil | (int_symb M.gen_tag) => (1%Z, (Vcons 0 Vnil)) :: (3%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.case9) => nil | (int_symb M.case9) => (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))) :: nil | (hd_symb M.eqs) => nil | (int_symb M.eqs) => nil | (hd_symb M.empty) => nil | (int_symb M.empty) => nil | (hd_symb M.stack) => nil | (int_symb M.stack) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.pushs) => nil | (int_symb M.pushs) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.pops) => nil | (int_symb M.pops) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.tops) => nil | (int_symb M.tops) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.istops) => nil | (int_symb M.istops) => nil | (hd_symb M.eqc) => nil | (int_symb M.eqc) => nil | (hd_symb M.nocalls) => nil | (int_symb M.nocalls) => nil | (hd_symb M.calls) => nil | (int_symb M.calls) => (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.push) => nil | (int_symb M.push) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.push1) => nil | (int_symb M.push1) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))))) :: nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS13. Module PI13 := PolyInt PIS13. (* polynomial interpretation 14 *) Module PIS14 (*<: TPolyInt*). Definition sig := s1. Definition trsInt f := match f as f return poly (@ASignature.arity s1 f) with | (hd_symb M.or) => nil | (int_symb M.or) => nil | (hd_symb M.T) => nil | (int_symb M.T) => nil | (hd_symb M.F) => nil | (int_symb M.F) => nil | (hd_symb M.and) => nil | (int_symb M.and) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.imp) => nil | (int_symb M.imp) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.not) => nil | (int_symb M.not) => nil | (hd_symb M._if_2) => nil | (int_symb M._if_2) => (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.eq) => nil | (int_symb M.eq) => nil | (hd_symb M.eqt) => nil | (int_symb M.eqt) => nil | (hd_symb M.nil) => nil | (int_symb M.nil) => nil | (hd_symb M.undefined) => nil | (int_symb M.undefined) => nil | (hd_symb M.pid) => nil | (int_symb M.pid) => nil | (hd_symb M.int) => nil | (int_symb M.int) => nil | (hd_symb M.cons) => nil | (int_symb M.cons) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.tuple) => nil | (int_symb M.tuple) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.tuplenil) => nil | (int_symb M.tuplenil) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a) => nil | (int_symb M.a) => nil | (hd_symb M.excl) => nil | (int_symb M.excl) => nil | (hd_symb M.false) => nil | (int_symb M.false) => nil | (hd_symb M.lock) => nil | (int_symb M.lock) => nil | (hd_symb M.locker) => nil | (int_symb M.locker) => nil | (hd_symb M.mcrlrecord) => nil | (int_symb M.mcrlrecord) => nil | (hd_symb M.ok) => nil | (int_symb M.ok) => nil | (hd_symb M.pending) => nil | (int_symb M.pending) => nil | (hd_symb M.release) => nil | (int_symb M.release) => nil | (hd_symb M.request) => nil | (int_symb M.request) => nil | (hd_symb M.resource) => nil | (int_symb M.resource) => nil | (hd_symb M.tag) => nil | (int_symb M.tag) => nil | (hd_symb M.true) => nil | (int_symb M.true) => nil | (hd_symb M.element) => nil | (int_symb M.element) => (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.s) => nil | (int_symb M.s) => nil | (hd_symb M._0_1) => nil | (int_symb M._0_1) => nil | (hd_symb M.record_new) => nil | (int_symb M.record_new) => nil | (hd_symb M.record_extract) => nil | (int_symb M.record_extract) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.record_update) => nil | (int_symb M.record_update) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (3%Z, (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))) :: nil | (hd_symb M.record_updates) => nil | (int_symb M.record_updates) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.locker2_map_promote_pending) => nil | (int_symb M.locker2_map_promote_pending) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_promote_pending) => nil | (int_symb M.locker2_promote_pending) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_map_claim_lock) => nil | (int_symb M.locker2_map_claim_lock) => (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_claim_lock) => nil | (int_symb M.locker2_claim_lock) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_map_add_pending) => nil | (int_symb M.locker2_map_add_pending) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.case0) => nil | (int_symb M.case0) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.locker2_remove_pending) => nil | (int_symb M.locker2_remove_pending) => (3%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.subtract) => nil | (int_symb M.subtract) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_add_pending) => nil | (int_symb M.locker2_add_pending) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (3%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.case1) => nil | (int_symb M.case1) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: (3%Z, (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))) :: nil | (hd_symb M.member) => nil | (int_symb M.member) => nil | (hd_symb M.append) => nil | (int_symb M.append) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_release_lock) => nil | (int_symb M.locker2_release_lock) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.case2) => nil | (int_symb M.case2) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: nil | (hd_symb M.gen_modtageq) => nil | (int_symb M.gen_modtageq) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (3%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.excllock) => nil | (int_symb M.excllock) => nil | (hd_symb M.case4) => nil | (int_symb M.case4) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_obtainables) => nil | (int_symb M.locker2_obtainables) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.case5) => nil | (int_symb M.case5) => (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: nil | (hd_symb M.andt) => nil | (int_symb M.andt) => nil | (hd_symb M.locker2_obtainable) => nil | (int_symb M.locker2_obtainable) => nil | (hd_symb M.locker2_check_available) => nil | (int_symb M.locker2_check_available) => (3%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.case6) => nil | (int_symb M.case6) => (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: nil | (hd_symb M.equal) => nil | (int_symb M.equal) => (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.locker2_check_availables) => nil | (int_symb M.locker2_check_availables) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.locker2_adduniq) => nil | (int_symb M.locker2_adduniq) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.delete) => nil | (int_symb M.delete) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.case8) => nil | (int_symb M.case8) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: nil | (hd_symb M.gen_tag) => nil | (int_symb M.gen_tag) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.case9) => nil | (int_symb M.case9) => nil | (hd_symb M.eqs) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (int_symb M.eqs) => nil | (hd_symb M.empty) => nil | (int_symb M.empty) => nil | (hd_symb M.stack) => nil | (int_symb M.stack) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.pushs) => nil | (int_symb M.pushs) => (3%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.pops) => nil | (int_symb M.pops) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.tops) => nil | (int_symb M.tops) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.istops) => nil | (int_symb M.istops) => (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.eqc) => nil | (int_symb M.eqc) => nil | (hd_symb M.nocalls) => nil | (int_symb M.nocalls) => nil | (hd_symb M.calls) => nil | (int_symb M.calls) => nil | (hd_symb M.push) => nil | (int_symb M.push) => (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: nil | (hd_symb M.push1) => nil | (int_symb M.push1) => (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))))) :: nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS14. Module PI14 := PolyInt PIS14. (* polynomial interpretation 15 *) Module PIS15 (*<: TPolyInt*). Definition sig := s1. Definition trsInt f := match f as f return poly (@ASignature.arity s1 f) with | (hd_symb M.or) => nil | (int_symb M.or) => nil | (hd_symb M.T) => nil | (int_symb M.T) => nil | (hd_symb M.F) => nil | (int_symb M.F) => nil | (hd_symb M.and) => nil | (int_symb M.and) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.imp) => nil | (int_symb M.imp) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.not) => nil | (int_symb M.not) => (2%Z, (Vcons 0 Vnil)) :: nil | (hd_symb M._if_2) => nil | (int_symb M._if_2) => (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.eq) => nil | (int_symb M.eq) => nil | (hd_symb M.eqt) => nil | (int_symb M.eqt) => nil | (hd_symb M.nil) => nil | (int_symb M.nil) => nil | (hd_symb M.undefined) => nil | (int_symb M.undefined) => nil | (hd_symb M.pid) => nil | (int_symb M.pid) => nil | (hd_symb M.int) => nil | (int_symb M.int) => nil | (hd_symb M.cons) => nil | (int_symb M.cons) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.tuple) => nil | (int_symb M.tuple) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.tuplenil) => nil | (int_symb M.tuplenil) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a) => nil | (int_symb M.a) => nil | (hd_symb M.excl) => nil | (int_symb M.excl) => nil | (hd_symb M.false) => nil | (int_symb M.false) => nil | (hd_symb M.lock) => nil | (int_symb M.lock) => nil | (hd_symb M.locker) => nil | (int_symb M.locker) => nil | (hd_symb M.mcrlrecord) => nil | (int_symb M.mcrlrecord) => nil | (hd_symb M.ok) => nil | (int_symb M.ok) => nil | (hd_symb M.pending) => nil | (int_symb M.pending) => nil | (hd_symb M.release) => nil | (int_symb M.release) => nil | (hd_symb M.request) => nil | (int_symb M.request) => nil | (hd_symb M.resource) => nil | (int_symb M.resource) => nil | (hd_symb M.tag) => nil | (int_symb M.tag) => nil | (hd_symb M.true) => nil | (int_symb M.true) => nil | (hd_symb M.element) => nil | (int_symb M.element) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.s) => nil | (int_symb M.s) => nil | (hd_symb M._0_1) => nil | (int_symb M._0_1) => nil | (hd_symb M.record_new) => nil | (int_symb M.record_new) => (1%Z, (Vcons 0 Vnil)) :: nil | (hd_symb M.record_extract) => nil | (int_symb M.record_extract) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.record_update) => nil | (int_symb M.record_update) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (3%Z, (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))) :: nil | (hd_symb M.record_updates) => nil | (int_symb M.record_updates) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.locker2_map_promote_pending) => nil | (int_symb M.locker2_map_promote_pending) => (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_promote_pending) => nil | (int_symb M.locker2_promote_pending) => (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_map_claim_lock) => nil | (int_symb M.locker2_map_claim_lock) => nil | (hd_symb M.locker2_claim_lock) => nil | (int_symb M.locker2_claim_lock) => nil | (hd_symb M.locker2_map_add_pending) => nil | (int_symb M.locker2_map_add_pending) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.case0) => nil | (int_symb M.case0) => (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.locker2_remove_pending) => nil | (int_symb M.locker2_remove_pending) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.subtract) => nil | (int_symb M.subtract) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_add_pending) => nil | (int_symb M.locker2_add_pending) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (3%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.case1) => nil | (int_symb M.case1) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: (3%Z, (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))) :: nil | (hd_symb M.member) => nil | (int_symb M.member) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.append) => nil | (int_symb M.append) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_release_lock) => nil | (int_symb M.locker2_release_lock) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.case2) => nil | (int_symb M.case2) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: nil | (hd_symb M.gen_modtageq) => nil | (int_symb M.gen_modtageq) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.excllock) => nil | (int_symb M.excllock) => nil | (hd_symb M.case4) => nil | (int_symb M.case4) => (3%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.locker2_obtainables) => nil | (int_symb M.locker2_obtainables) => nil | (hd_symb M.case5) => nil | (int_symb M.case5) => nil | (hd_symb M.andt) => nil | (int_symb M.andt) => nil | (hd_symb M.locker2_obtainable) => nil | (int_symb M.locker2_obtainable) => nil | (hd_symb M.locker2_check_available) => nil | (int_symb M.locker2_check_available) => (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.case6) => nil | (int_symb M.case6) => (3%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (3%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: nil | (hd_symb M.equal) => nil | (int_symb M.equal) => nil | (hd_symb M.locker2_check_availables) => nil | (int_symb M.locker2_check_availables) => (3%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (hd_symb M.locker2_adduniq) => nil | (int_symb M.locker2_adduniq) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.delete) => nil | (int_symb M.delete) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.case8) => nil | (int_symb M.case8) => (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: nil | (hd_symb M.gen_tag) => nil | (int_symb M.gen_tag) => (2%Z, (Vcons 0 Vnil)) :: (3%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.case9) => nil | (int_symb M.case9) => (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))) :: nil | (hd_symb M.eqs) => nil | (int_symb M.eqs) => nil | (hd_symb M.empty) => nil | (int_symb M.empty) => nil | (hd_symb M.stack) => nil | (int_symb M.stack) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.pushs) => nil | (int_symb M.pushs) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.pops) => nil | (int_symb M.pops) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.tops) => nil | (int_symb M.tops) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.istops) => nil | (int_symb M.istops) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.eqc) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (int_symb M.eqc) => nil | (hd_symb M.nocalls) => nil | (int_symb M.nocalls) => nil | (hd_symb M.calls) => nil | (int_symb M.calls) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.push) => nil | (int_symb M.push) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.push1) => nil | (int_symb M.push1) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))))) :: (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))))) :: nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS15. Module PI15 := PolyInt PIS15. (* termination proof *) Lemma termination : WF rel. Proof. unfold rel. dp_trans. mark. let D := fresh "D" in let R := fresh "R" in set_rules_to D; set_mod_rules_to R; graph_decomp (dpg_unif_N 100 R D) cs1; subst D; subst R. dpg_unif_N_correct. left. co_scc. left. co_scc. left. co_scc. left. co_scc. left. co_scc. left. co_scc. left. co_scc. left. co_scc. left. co_scc. left. co_scc. right. PI1.prove_termination. termination_trivial. right. PI2.prove_termination. termination_trivial. left. co_scc. left. co_scc. left. co_scc. left. co_scc. left. co_scc. right. PI3.prove_termination. termination_trivial. left. co_scc. left. co_scc. left. co_scc. right. PI4.prove_termination. PI5.prove_termination. let D := fresh "D" in let R := fresh "R" in set_rules_to D; set_mod_rules_to R; graph_decomp (dpg_unif_N 100 R D) cs2; subst D; subst R. dpg_unif_N_correct. left. co_scc. left. co_scc. left. co_scc. left. co_scc. left. co_scc. left. co_scc. left. co_scc. left. co_scc. left. co_scc. left. co_scc. right. PI6.prove_termination. termination_trivial. left. co_scc. right. PI7.prove_termination. termination_trivial. left. co_scc. left. co_scc. left. co_scc. left. co_scc. left. co_scc. left. co_scc. left. co_scc. left. co_scc. right. PI8.prove_termination. termination_trivial. right. PI9.prove_termination. termination_trivial. left. co_scc. left. co_scc. right. PI10.prove_termination. PI11.prove_termination. PI12.prove_termination. PI13.prove_termination. termination_trivial. left. co_scc. left. co_scc. left. co_scc. left. co_scc. right. PI14.prove_termination. termination_trivial. left. co_scc. right. PI15.prove_termination. termination_trivial. Qed.