menu

Return to entry

Context_Notation
Typing
Term_Typing
Generic_Context
Parallel_Induct
IsaFoR_Ground_Term
IsaFoR_Ground_Context
Ground_Term_Typing
Nonground_Term
Multiset_Extra
Multiset_Grounding_Lifting
Nonground_Clause_Generic
Selection_Function
Nonground_Selection_Function
HOL_Extra
Grounded_Selection_Function
IsaFoR_Nonground_Term
Literal_Functor
Uprod_Extra
Uprod_Literal_Functor
Nonground_Clause_With_Equality
IsaFoR_Nonground_Clause_With_Equality
Nonground_Context
Context_Functor
IsaFoR_Nonground_Context
Restricted_Order
Context_Compatible_Order
Term_Order_Notation
Transitive_Closure_Extra
Ground_Term_Order
Grounded_Order
Nonground_Term_Order
Multiset_Extension
Natural_Functor_To_Multiset
Grounded_Multiset_Extension
Maximal_Literal
Term_Order_Lifting
Ground_Order_Generic
Nonground_Order_Generic
Ground_Order_With_Equality
Nonground_Order_With_Equality
Selection_Function_Select_Max
IsaFoR_KBO
Nonground_Clause
IsaFoR_Nonground_Clause
Ground_Term_Rewrite_System
Ground_Critical_Pairs
Ground_Critical_Peaks
IsaFoR_Ground_Critical_Pairs
Collect_Extra
Infinite_Variables_Per_Type
Typed_Substitution
Nonground_Term_Typing
Typed_IMGU
Monomorphic_Typing
Entailment_Lifting
Fold_Extra
Nonground_Entailment
Inference_Functor
Nonground_Inference
Ground_Order
Nonground_Order
Natural_Magma_Typing_Lifting
Multiset_Typing_Lifting
Clause_Typing_Generic
Typed_Substitution_Lifting
Nonground_Typing_Generic
Clause_Typing
Nonground_Typing
Clause_Typing_With_Equality
Nonground_Typing_With_Equality
Typed_Substitution_Example
Typed_Substitution_Lifting_Example
Tiebreakers
Typed_Tiebreakers
Untyped_Calculus

First_Order_Clause.Typed_Substitution_Lifting_Example

HTML Presentation