insert std/K.mli theory TK1. -- Test K (predicate theory). include theory K. [* trace_result -- trace_proof trace_variable_type trace_bind trace_substitute trace_unify *] [* -- Mendelson, p. 60. lemma X2. formula A, C. A, ∀x A ⇒ C ⊢ ∀x C. proof. -- conclusion by Gen, premiss, MP. 1. A by premiss. 2. ∀x A by 1, Gen. 3. ∀x A ⇒ C by premiss. 4. C by 2, 3, MP. conclusion by 4, Gen. ∎ *] trace_result -- trace_proof trace_variable_type trace_bind [*trace_unify trace_substitute *] -- Mendelson, p. 62. lemma X3. formula A. -- metaobject x, y. ∀x, y A ⊢ ∀y, x A. proof. conclusion by Gen, premiss, K1a. [* 1. ∀x, y A by premiss. 2. ∀x, y A ⊢ ∀y A by K1a. -- K1a. ∀x A ⊢ A[x.t] 3. ∀y A by 2, 1. 4. ∀y A ⊢ A by K1a. conclusion by 3, 4, Gen. *] [* 1. ∀x, y A by premiss. 2. ∀x, y A ⊢ (∀y A) by K1a. -- 2. ∀x, y A ⊢ (∀y A)[x.x] by K1a. 3. ∀y A by 2, 1. 4. ∀y A ⊢ A by K1a. -- 4. ∀y A ⊢ A[y.y] by K1a. 5. A by 3, 4. 6. ∀x A by 5, Gen. 7. ∀y, x A by 6, Gen. conclusion by 7. *] ∎ --untrace_all [* lemma X3a. formula A. -- metaobject x, y. ∀x, y A ⇒ ∀y, x A. proof. conclusion by DT; Gen; Gen; K1a. -- conclusion by Gen, K1a, DT. ∎ *] trace_result trace_proof trace_variable_type trace_bind trace_unify trace_substitute [**] lemma X3b. formula A. -- metaobject x, y. ∀x, y A ⇒ ∀y, x A. proof. conclusion by DT; X3. -- conclusion by Gen, K1a, DT. ∎ -- rule K1a. ∀x A ⊢ A[x.t]. untrace_all [* trace_result trace_proof trace_variable_type trace_bind trace_unify trace_substitute *] [* lemma X4. formula A object x. ∀x A ⊢ ∀y: A[x.y]. proof. conclusion by premiss. ∎ *] untrace_all end theory TK1.