OAI/Analysis/MatrixSigning/Arithmetic/RationalExpressionHeight.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W17.RationalExpr.leaves line 9
2. def OAI.KS.W17.RationalExpr.inputsBounded line 14
3. theorem OAI.KS.W17.RationalExpr.leaves_le_operations_add_one line 19
4. theorem OAI.KS.W17.RationalExpr.eval_parts_le line 23
5. theorem OAI.KS.W17.RationalExpr.eval_parts_le_of_operations line 94
6. inductive OAI.KS.W17.RationalExpr.IsSubexpression line 105
7. theorem OAI.KS.W17.RationalExpr.IsSubexpression.inputsBounded line 117
8. theorem OAI.KS.W17.RationalExpr.IsSubexpression.operations_le line 125
9. theorem OAI.KS.W17.RationalExpr.IsSubexpression.eval_parts_le line 129