From b5256ce20e1af905903f0029ae1fdb049260c279 Mon Sep 17 00:00:00 2001 From: hkalbasi Date: Fri, 2 Feb 2024 13:43:20 +0330 Subject: [PATCH] Add some theorems --- library/Automata.v | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/library/Automata.v b/library/Automata.v index fe5d650..f180185 100644 --- a/library/Automata.v +++ b/library/Automata.v @@ -189,6 +189,11 @@ Axiom conditional_tm_reject_unfold: ∀ cond then else: TM, ∀ s, turing_reject Axiom conditional_tm_reject_fold: ∀ cond then else: TM, ∀ s, turing_accept cond s ∧ turing_reject then s ∨ turing_reject cond s ∧ turing_reject else s -> turing_reject (conditional_tm cond then else) s; +Todo conditional_tm_halt_unfold: ∀ cond then else: TM, ∀ s, turing_halt (conditional_tm cond then else) s + -> turing_halt cond s ∧ (turing_accept cond s -> turing_halt then s) ∧ (turing_reject cond s -> turing_halt else s); +Todo conditional_tm_halt_fold: ∀ cond then else: TM, ∀ s, + turing_halt cond s ∧ (turing_accept cond s -> turing_halt then s) ∧ (turing_reject cond s -> turing_halt else s) + -> turing_halt (conditional_tm cond then else) s; Axiom is_decidable: set (list char) -> U; Axiom is_decidable_fold: ∀ lang, (∃ t, decider t ∧ ∀ s, s ∈ lang ↔ turing_accept t s) -> is_decidable lang; @@ -199,6 +204,8 @@ Suggest hyp default apply is_decidable_unfold in $n with label Destruct; Axiom #2 computable: ∀ X Y: U, (X → Y) → U; Axiom computable_concat: computable (plus (list char)); +Axiom computable_plus: computable (plus ℤ); +Axiom computable_minus: computable (λ x: ℤ, - x); Axiom computable_const: ∀ X Y: U, ∀ a: Y, computable (λ x: X, a); Suggest goal default apply computable_const with label Trivial;