今回は項書換え的な書き方にしてみた。まずKコンビネータから。 open util/ordering[Term] some abstract sig Term {} one sig K extends Term {} sig Apply extends Term { f, g: Term } fact { all x, y: Term | (x -> y) in (f + g) => y not in (x.prevs…