SSLC : Simplified Symbolic Lambda Calculus

MAIN IDEAS

SSLC is a formal system for proving equality of terms called symbolic lambda-terms derived from SLC. The following simplifications are introduced :
- instead of a potential infinity of symbols, there is only one symbol (SMB)
- like in SLC, De Bruijn index notation is used, but the variable (DBV n) is replaced by (DBS (DBS ... (DBS DB0) ... )) with DBS repeated n times
- there is only one axiom
These simplifications does not introduce restrictions : several symbols may be represented by different terms applied to the unique symbol, and several axioms a1 = b1, a2 = b2, ... , an = bn may be represented by a unique axiom, for example  <a1, a2, ..., an> = <b1, b2, ... , bn>

A SSLC term may be 
 - (SMB) the unique symbol
 - (DB0) the initial variable 
 - (DBS x) the variable following x
 - (DBL x) abstraction, where x is a SSLC term
 - (APL x y) application of SSLC term x to SSLC term y
 - (LTR x y) left transitivity - symmetry with reduction applied to SSLC terms x and y
             representing the rule a = b, c = d, a -> e, c -> e, b -> f, d -> g => f = g
 - (AXM) the unique axiom

Reduction of a term is defined by iterating a reduction step which consists of substituting (AP (DBL x) y) by the result of the substitution in x of variables whose index equals to the nesting level in DBL terms by y, according to De Bruijn index notation.

Like in SLC, SSLC terms represent both extended (with (SMB)) lambda-terms and proofs in theories. A theory t is represented by a unique axiom u = v.
To any SSLC term and any theory are associated two SSLC terms called left and right. A SSLC term is associated to a proof in theory t of the equality of its left and its right : x proves left(t,x) = right(t,x). Symbolic lambda-terms are particular SSLC terms which represent both a symbolic lambda-term and the proof that this symbolic lambda-term equals itself. Left and right of a lambda-term is itself.

Any SSLC term proves that its left equals its right. In a theory t with axiom u = v : 

 - (SMB) proves (SMB) = (SMB)
 - (DB0) proves (DB0) = (DB0)
 - (DBS x) proves (DBS a) = (DBS b) if x proves a = b
 - (DBL x) proves (DBL a) = (DBL b) if x proves a = b
 - (APL x y) proves (APL a c) = (APL b d) if x proves a = b and y proves c = d
   in other terms, if a = b and c = d then (APL a c) = (APL b d)
 - (LTR x y) proves f = g if x proves a = b, y proves c = d, a reduces to e, c reduces to e, b reduces to f and d reduces to g, otherwise it proves (LTR x y) = (LTR x y)
 - (AXM) proves u = v.