ClassicalProp__ __ jlc | Jim Caldwell's development of Classical Propositional Logic. |

decidability | |

normalization | The normalization lemma. |

elimination | |

sequent__ __ valid | |

full__ __ sequent__ __ assignment | |

sequent__ __ sat__ __ lemmas | |

sequent__ __ falsification | |

sequent__ __ satisfaction | |

sequent__ __ rank | |

formula__ __ list | |

sequent__ __ equality | |

sequent | |

formula__ __ validity | |

full__ __ assignment | |

sat__ __ lemmas | |

formula__ __ equality | |

formula__ __ falsification | |

formula__ __ satisfaction | |

formula__ __ rank | |

valuation | |

Kleene | Kleene 3-valued truth connectives. |

assignment | |

Three | Type of 3-truth-values |

formula | Propositional formula structure. |

var__ __ jlc | |

list__ __ 3__ __ jlc | More on Lists |

core__ __ 3__ __ jlc | Various facts about Propositional Operators |

discrete__ __ jlc | Basics of Discrete Types |

bool__ __ 2__ __ jlc | A few basic facts about asserting Bools and Bool Equalities |

lambda__ __ jlc | Currying functions and Explicitly expressing recursion. |

list__ __ 1 | |

int__ __ 2 | Defines mod, floor, max and min functions over the integers. Lemmas concern basic properties of arithmetic functions over integers, and induction principles. |

rfunction__ __ 1 | |

prog__ __ 1 | |

sqequal__ __ 1 | |

quot__ __ 1 | Support lemmas for quotient type. |

rel__ __ 1 | Common properties of binary relations. |

union | Non canonical functions (isl, outl, outr) for union type. |

bool__ __ 1 | Definitions, theorems and tactics for the boolean type and boolean-related expressions. |

int__ __ 1 | Integer inequalities, subtypes, and induction lemmas for subtypes. |

well__ __ fnd | Well-founded predicate. Rank induction lemmas and tactics. |

fun__ __ 1 | Polymorphic identity and composition functions. Lemmas covering properties such as injectivity and surjectivity. |

core | Some basic concepts defined type-theoretically. |