Analogies between Proofs : A Case Study
Erica Melis⋆ · 1993
ion of both problems (i.e., theorem and assumptions) 7.5.7.2.c and 5.7.2.c based on the meaning of the two respective definitions of homomorphism. The key is a reformulation of terms of the form f \\Delta term(x) to terms Op(term(x)) for 7.5.7.2c and term1\\Deltaterm2 to Op(term1,term2) with a function variable Op. This reformulation affects the definitions of homomorphism within the relevant assumptions: 8f8x(f 2 F x 2 S ! OE(f \\Delta x) = f \\Delta OE(x)) becomes 8x(x 2 S ! OE(Op(x)) = Op(OE(x))) by the mapping f \\Delta term )Op(term) 8x; y(x 2 S 0 y 2 S 0 ! OE(x \\Delta y) = OE(x) \\Delta OE(y)) becomes 8x; y(x 2 S 0 y 2 S 0 ! OE(Op 0 (x; y)) = Op 0 (OE(x); OE(y))) by the mapping term1\\Deltaterm2 )Op(term1,term2). The reformulation affects also the corresponding terms within the whole proof. Certain subformulae and quantifiers become superfluous and, hence, can be omitted. As a result we obtain the theorems and reformulated proofs 7.5.7.2c 0 and 5.7.2.c 0 . 2. T...