rewriting in a uniform way. We define the relation 1=, a notion of infinitary equational reasoning, and !1, the standard notion of infinitary rewriting as follows: 1= := R. (=R [ R) !1 := μR. S. (!R [ R)  S where μ and  are the least and greatest fixed-point operators, respectively, and where R := { hf(s1, . . . , sn), f(t1, . . . , tn)i | f 2 , s1 R t1, . . . , sn R tn } [ Id . The setup captures rewrite sequences of arbitrary ordinal length, but it has neither the need for ordinals nor for metric convergence. This makes the framework especially suitable for formalizations in theorem provers.
Cornell University Library e-Print archive
Computer Security

Endrullis, J., Hansen, H., Hendriks, D., Polonsky, A., & Silva, A. (2015). A Coinductive Treatment of Infinitary Term Rewriting and Equational Reasoning (Extended Version).. e-Print archive. Cornell University Library .