src/HOL/Tools/atp-inputs/const_combS_e.tptp
author huffman
Sun, 24 Sep 2006 07:14:02 +0200
changeset 20694 76c49548d14c
parent 20660 8606ddd42554
permissions -rw-r--r--
real_norm_def [simp]

%ID: $Id$
%Author: Jia Meng, NICTA
%const-typed combinator reduction for S'

%S' c f g x --> c (f x) (g x)
input_clause(a8,axiom,
[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBS__e(A,B,U,V),C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),hAPP(G,X)))]).