From 8564c7f51e34897656ef1adbc19f5f939533307c Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 20 Apr 2025 11:55:31 -0700 Subject: [PATCH 1/4] cp coq_benchmark.py lean_benchmark.py --- .../rewrite_with_eq_f_a/lean_benchmark.py | 108 ++++++++++++++++++ .../rewrite_with_eq_haa_a/lean_benchmark.py | 106 +++++++++++++++++ 2 files changed, 214 insertions(+) create mode 100644 benchmark/rewrite_with_eq_f_a/lean_benchmark.py create mode 100644 benchmark/rewrite_with_eq_haa_a/lean_benchmark.py diff --git a/benchmark/rewrite_with_eq_f_a/lean_benchmark.py b/benchmark/rewrite_with_eq_f_a/lean_benchmark.py new file mode 100644 index 0000000..5d9b4ae --- /dev/null +++ b/benchmark/rewrite_with_eq_f_a/lean_benchmark.py @@ -0,0 +1,108 @@ +import json +import subprocess +import time +import os +import glob + +benchmark_results_fn = "mengine_benchmark_results.json" +context_fn = "base.v" +program = "coqc" + +rewrite_strategies = [ + "repeat rewrite eq_fa_a.", + "rewrite! eq_fa_a.", + "rewrite_strat topdown eq_fa_a.", + "rewrite_strat bottomup eq_fa_a." +] + +SKIP_STRATEGIES = { + "repeat rewrite eq_fa_a.", + "rewrite! eq_fa_a." +} + +def get_theorem_with_file_content(filename, input_expr, expected_equality, index, rewrite_strat_str): + with open(filename, 'r') as file: + content = file.readlines() + + theorem_str = f"\nTheorem test_{index} : eq nat ({input_expr}) ({expected_equality}). Proof. {rewrite_strat_str} reflexivity. Qed. End Test." + combined_content = ''.join(content) + theorem_str + '\n' + + return combined_content + + +def read_benchmark_results(filename): + with open(filename, 'r') as file: + benchmark_data = json.load(file) + + return benchmark_data + + +def calculate_equality(test_case): + if test_case['G'] != 0: + return '(g a)' + else: + return 'a' + + +def run_tests(): + input_values = read_benchmark_results(benchmark_results_fn) + results = {} + + if os.path.exists('coq_benchmark_results.json'): + with open('coq_benchmark_results.json', 'r') as f: + results = json.load(f) + + for key, test_case in input_values.items(): + test_input = test_case['input'] + test_output = calculate_equality(test_case) + + if key not in results: + results[key] = {} + + for rewrite_strat in rewrite_strategies: + rewrite_command = rewrite_strat.strip() + + if rewrite_command in results[key]: + print(f"Test {key} with '{rewrite_command}': EXISTS") + continue + + if rewrite_command in SKIP_STRATEGIES: + print(f"Test {key} with '{rewrite_command}': SKIPPED") + continue + + + coq_benchmark_content = get_theorem_with_file_content( + context_fn, test_input, test_output, key, rewrite_strat + ) + + test_filename = f"test_{key}.v" + with open(test_filename, 'w') as f: + f.write(coq_benchmark_content) + + # Time how long it takes to run "coqc test_{key}.v" + start_time = time.time() + result = subprocess.run([program, test_filename], + stdout=subprocess.PIPE, stderr=subprocess.PIPE) + elapsed_time = time.time() - start_time + + vo_filename = f"test_{key}.vo" + rewrite_result = { + "rewrite_command": rewrite_strat.strip(), + "status": "PASSED" if os.path.exists(vo_filename) else "FAILED", + "time": elapsed_time if os.path.exists(vo_filename) else None + } + + results[key][rewrite_strat.strip()] = rewrite_result + print(f"Test {key} with '{rewrite_strat.strip()}': {rewrite_result['status']}") + + for file in glob.glob(f"test_{key}.*") + glob.glob(f".test_{key}.*"): + os.remove(file) + + with open('coq_benchmark_results.json', 'w') as f: + json.dump(results, f, indent=4) + + return results + + +if __name__ == "__main__": + run_tests() diff --git a/benchmark/rewrite_with_eq_haa_a/lean_benchmark.py b/benchmark/rewrite_with_eq_haa_a/lean_benchmark.py new file mode 100644 index 0000000..3e7d9af --- /dev/null +++ b/benchmark/rewrite_with_eq_haa_a/lean_benchmark.py @@ -0,0 +1,106 @@ +import json +import subprocess +import time +import os +import glob + +benchmark_results_fn = "mengine_benchmark_results.json" +context_fn = "base.v" +program = "coqc" + +rewrite_strategies = [ + "repeat rewrite eq_haa_a.", + "rewrite! eq_haa_a.", + "rewrite_strat topdown eq_haa_a.", + "rewrite_strat bottomup eq_haa_a." +] + +SKIP_STRATEGIES = { + "repeat rewrite eq_haa_a.", + "rewrite! eq_haa_a.", + "rewrite_strat bottomup eq_haa_a." +} + +def get_theorem_with_file_content(filename, input_expr, expected_equality, index, rewrite_strat_str): + with open(filename, 'r') as file: + content = file.readlines() + + theorem_str = f"\nTheorem test_{index} : eq nat ({input_expr}) ({expected_equality}). Proof. {rewrite_strat_str} reflexivity. Qed. End Test." + combined_content = ''.join(content) + theorem_str + '\n' + + return combined_content + + +def read_benchmark_results(filename): + with open(filename, 'r') as file: + benchmark_data = json.load(file) + + return benchmark_data + + +def calculate_equality(test_case): + return 'c' + + +def run_tests(): + input_values = read_benchmark_results(benchmark_results_fn) + results = {} + + if os.path.exists('coq_benchmark_results.json'): + with open('coq_benchmark_results.json', 'r') as f: + results = json.load(f) + + for key, test_case in input_values.items(): + test_input = test_case['input'] + test_output = calculate_equality(test_case) + + if key not in results: + results[key] = {} + + for rewrite_strat in rewrite_strategies: + rewrite_command = rewrite_strat.strip() + + if rewrite_command in results[key]: + print(f"Test {key} with '{rewrite_command}': EXISTS") + continue + + if rewrite_command in SKIP_STRATEGIES: + print(f"Test {key} with '{rewrite_command}': SKIPPED") + continue + + + coq_benchmark_content = get_theorem_with_file_content( + context_fn, test_input, test_output, key, rewrite_strat + ) + + test_filename = f"test_{key}.v" + with open(test_filename, 'w') as f: + f.write(coq_benchmark_content) + + # Time how long it takes to run "coqc test_{key}.v" + start_time = time.time() + result = subprocess.run([program, test_filename], + stdout=subprocess.PIPE, stderr=subprocess.PIPE) + elapsed_time = time.time() - start_time + + vo_filename = f"test_{key}.vo" + rewrite_result = { + "rewrite_command": rewrite_strat.strip(), + "status": "PASSED" if os.path.exists(vo_filename) else "FAILED", + "time": elapsed_time if os.path.exists(vo_filename) else None + } + + results[key][rewrite_strat.strip()] = rewrite_result + print(f"Test {key} with '{rewrite_strat.strip()}': {rewrite_result['status']}") + + for file in glob.glob(f"test_{key}.*") + glob.glob(f".test_{key}.*"): + os.remove(file) + + with open('coq_benchmark_results.json', 'w') as f: + json.dump(results, f, indent=4) + + return results + + +if __name__ == "__main__": + run_tests() From 3b75d879ad5105c37153bf0a003e1db0ad8444d2 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 20 Apr 2025 11:56:15 -0700 Subject: [PATCH 2/4] Autoformat .py file --- .../rewrite_with_eq_f_a/lean_benchmark.py | 50 ++++++++++--------- .../rewrite_with_eq_haa_a/lean_benchmark.py | 43 +++++++++------- 2 files changed, 50 insertions(+), 43 deletions(-) diff --git a/benchmark/rewrite_with_eq_f_a/lean_benchmark.py b/benchmark/rewrite_with_eq_f_a/lean_benchmark.py index 5d9b4ae..ae2b5d4 100644 --- a/benchmark/rewrite_with_eq_f_a/lean_benchmark.py +++ b/benchmark/rewrite_with_eq_f_a/lean_benchmark.py @@ -12,56 +12,56 @@ "repeat rewrite eq_fa_a.", "rewrite! eq_fa_a.", "rewrite_strat topdown eq_fa_a.", - "rewrite_strat bottomup eq_fa_a." + "rewrite_strat bottomup eq_fa_a.", ] -SKIP_STRATEGIES = { - "repeat rewrite eq_fa_a.", - "rewrite! eq_fa_a." -} +SKIP_STRATEGIES = {"repeat rewrite eq_fa_a.", "rewrite! eq_fa_a."} + -def get_theorem_with_file_content(filename, input_expr, expected_equality, index, rewrite_strat_str): - with open(filename, 'r') as file: +def get_theorem_with_file_content( + filename, input_expr, expected_equality, index, rewrite_strat_str +): + with open(filename, "r") as file: content = file.readlines() theorem_str = f"\nTheorem test_{index} : eq nat ({input_expr}) ({expected_equality}). Proof. {rewrite_strat_str} reflexivity. Qed. End Test." - combined_content = ''.join(content) + theorem_str + '\n' + combined_content = "".join(content) + theorem_str + "\n" return combined_content def read_benchmark_results(filename): - with open(filename, 'r') as file: + with open(filename, "r") as file: benchmark_data = json.load(file) return benchmark_data def calculate_equality(test_case): - if test_case['G'] != 0: - return '(g a)' + if test_case["G"] != 0: + return "(g a)" else: - return 'a' + return "a" def run_tests(): input_values = read_benchmark_results(benchmark_results_fn) results = {} - if os.path.exists('coq_benchmark_results.json'): - with open('coq_benchmark_results.json', 'r') as f: + if os.path.exists("coq_benchmark_results.json"): + with open("coq_benchmark_results.json", "r") as f: results = json.load(f) for key, test_case in input_values.items(): - test_input = test_case['input'] + test_input = test_case["input"] test_output = calculate_equality(test_case) - + if key not in results: results[key] = {} for rewrite_strat in rewrite_strategies: rewrite_command = rewrite_strat.strip() - + if rewrite_command in results[key]: print(f"Test {key} with '{rewrite_command}': EXISTS") continue @@ -70,35 +70,37 @@ def run_tests(): print(f"Test {key} with '{rewrite_command}': SKIPPED") continue - coq_benchmark_content = get_theorem_with_file_content( context_fn, test_input, test_output, key, rewrite_strat ) test_filename = f"test_{key}.v" - with open(test_filename, 'w') as f: + with open(test_filename, "w") as f: f.write(coq_benchmark_content) # Time how long it takes to run "coqc test_{key}.v" start_time = time.time() - result = subprocess.run([program, test_filename], - stdout=subprocess.PIPE, stderr=subprocess.PIPE) + result = subprocess.run( + [program, test_filename], stdout=subprocess.PIPE, stderr=subprocess.PIPE + ) elapsed_time = time.time() - start_time vo_filename = f"test_{key}.vo" rewrite_result = { "rewrite_command": rewrite_strat.strip(), "status": "PASSED" if os.path.exists(vo_filename) else "FAILED", - "time": elapsed_time if os.path.exists(vo_filename) else None + "time": elapsed_time if os.path.exists(vo_filename) else None, } results[key][rewrite_strat.strip()] = rewrite_result - print(f"Test {key} with '{rewrite_strat.strip()}': {rewrite_result['status']}") + print( + f"Test {key} with '{rewrite_strat.strip()}': {rewrite_result['status']}" + ) for file in glob.glob(f"test_{key}.*") + glob.glob(f".test_{key}.*"): os.remove(file) - with open('coq_benchmark_results.json', 'w') as f: + with open("coq_benchmark_results.json", "w") as f: json.dump(results, f, indent=4) return results diff --git a/benchmark/rewrite_with_eq_haa_a/lean_benchmark.py b/benchmark/rewrite_with_eq_haa_a/lean_benchmark.py index 3e7d9af..71c424c 100644 --- a/benchmark/rewrite_with_eq_haa_a/lean_benchmark.py +++ b/benchmark/rewrite_with_eq_haa_a/lean_benchmark.py @@ -12,54 +12,57 @@ "repeat rewrite eq_haa_a.", "rewrite! eq_haa_a.", "rewrite_strat topdown eq_haa_a.", - "rewrite_strat bottomup eq_haa_a." + "rewrite_strat bottomup eq_haa_a.", ] SKIP_STRATEGIES = { "repeat rewrite eq_haa_a.", "rewrite! eq_haa_a.", - "rewrite_strat bottomup eq_haa_a." + "rewrite_strat bottomup eq_haa_a.", } -def get_theorem_with_file_content(filename, input_expr, expected_equality, index, rewrite_strat_str): - with open(filename, 'r') as file: + +def get_theorem_with_file_content( + filename, input_expr, expected_equality, index, rewrite_strat_str +): + with open(filename, "r") as file: content = file.readlines() theorem_str = f"\nTheorem test_{index} : eq nat ({input_expr}) ({expected_equality}). Proof. {rewrite_strat_str} reflexivity. Qed. End Test." - combined_content = ''.join(content) + theorem_str + '\n' + combined_content = "".join(content) + theorem_str + "\n" return combined_content def read_benchmark_results(filename): - with open(filename, 'r') as file: + with open(filename, "r") as file: benchmark_data = json.load(file) return benchmark_data def calculate_equality(test_case): - return 'c' + return "c" def run_tests(): input_values = read_benchmark_results(benchmark_results_fn) results = {} - if os.path.exists('coq_benchmark_results.json'): - with open('coq_benchmark_results.json', 'r') as f: + if os.path.exists("coq_benchmark_results.json"): + with open("coq_benchmark_results.json", "r") as f: results = json.load(f) for key, test_case in input_values.items(): - test_input = test_case['input'] + test_input = test_case["input"] test_output = calculate_equality(test_case) - + if key not in results: results[key] = {} for rewrite_strat in rewrite_strategies: rewrite_command = rewrite_strat.strip() - + if rewrite_command in results[key]: print(f"Test {key} with '{rewrite_command}': EXISTS") continue @@ -68,35 +71,37 @@ def run_tests(): print(f"Test {key} with '{rewrite_command}': SKIPPED") continue - coq_benchmark_content = get_theorem_with_file_content( context_fn, test_input, test_output, key, rewrite_strat ) test_filename = f"test_{key}.v" - with open(test_filename, 'w') as f: + with open(test_filename, "w") as f: f.write(coq_benchmark_content) # Time how long it takes to run "coqc test_{key}.v" start_time = time.time() - result = subprocess.run([program, test_filename], - stdout=subprocess.PIPE, stderr=subprocess.PIPE) + result = subprocess.run( + [program, test_filename], stdout=subprocess.PIPE, stderr=subprocess.PIPE + ) elapsed_time = time.time() - start_time vo_filename = f"test_{key}.vo" rewrite_result = { "rewrite_command": rewrite_strat.strip(), "status": "PASSED" if os.path.exists(vo_filename) else "FAILED", - "time": elapsed_time if os.path.exists(vo_filename) else None + "time": elapsed_time if os.path.exists(vo_filename) else None, } results[key][rewrite_strat.strip()] = rewrite_result - print(f"Test {key} with '{rewrite_strat.strip()}': {rewrite_result['status']}") + print( + f"Test {key} with '{rewrite_strat.strip()}': {rewrite_result['status']}" + ) for file in glob.glob(f"test_{key}.*") + glob.glob(f".test_{key}.*"): os.remove(file) - with open('coq_benchmark_results.json', 'w') as f: + with open("coq_benchmark_results.json", "w") as f: json.dump(results, f, indent=4) return results From 684e64103e314fc55c70d76176261526d2003fdb Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 20 Apr 2025 11:54:50 -0700 Subject: [PATCH 3/4] Add Lean benchmark --- .gitignore | 5 +- benchmark/rewrite_with_eq_f_a/base.lean | 7 ++ .../rewrite_with_eq_f_a/lean_benchmark.py | 57 ++++++++++------- benchmark/rewrite_with_eq_haa_a/base.lean | 8 +++ .../rewrite_with_eq_haa_a/lean_benchmark.py | 64 +++++++++++-------- 5 files changed, 90 insertions(+), 51 deletions(-) create mode 100644 benchmark/rewrite_with_eq_f_a/base.lean create mode 100644 benchmark/rewrite_with_eq_haa_a/base.lean diff --git a/.gitignore b/.gitignore index fb1347d..3fe44be 100644 --- a/.gitignore +++ b/.gitignore @@ -25,4 +25,7 @@ tests/__pycache__/ .git/* -.vscode/* \ No newline at end of file +.vscode/* + +.venv/ + diff --git a/benchmark/rewrite_with_eq_f_a/base.lean b/benchmark/rewrite_with_eq_f_a/base.lean new file mode 100644 index 0000000..89965f5 --- /dev/null +++ b/benchmark/rewrite_with_eq_f_a/base.lean @@ -0,0 +1,7 @@ +import Std.Tactic +section Test + +variable {α : Type} + +variable (f : α → α) (g : α → α) (eq_fa_a : ∀ x : α, f x = x) +variable (a b : α) diff --git a/benchmark/rewrite_with_eq_f_a/lean_benchmark.py b/benchmark/rewrite_with_eq_f_a/lean_benchmark.py index ae2b5d4..84c033f 100644 --- a/benchmark/rewrite_with_eq_f_a/lean_benchmark.py +++ b/benchmark/rewrite_with_eq_f_a/lean_benchmark.py @@ -3,19 +3,15 @@ import time import os import glob +import re -benchmark_results_fn = "mengine_benchmark_results.json" -context_fn = "base.v" -program = "coqc" +benchmark_results_fn = "mengine_benchmark_2_results.json" +context_fn = "base.lean" +program = "lean" -rewrite_strategies = [ - "repeat rewrite eq_fa_a.", - "rewrite! eq_fa_a.", - "rewrite_strat topdown eq_fa_a.", - "rewrite_strat bottomup eq_fa_a.", -] +rewrite_strategies = ["sorry", "repeat' rw [eq_fa_a]", "simp only [eq_fa_a]"] -SKIP_STRATEGIES = {"repeat rewrite eq_fa_a.", "rewrite! eq_fa_a."} +SKIP_STRATEGIES = {} def get_theorem_with_file_content( @@ -24,7 +20,8 @@ def get_theorem_with_file_content( with open(filename, "r") as file: content = file.readlines() - theorem_str = f"\nTheorem test_{index} : eq nat ({input_expr}) ({expected_equality}). Proof. {rewrite_strat_str} reflexivity. Qed. End Test." + indented_rewrite_strat_str = rewrite_strat_str.replace("\n", "\n ") + theorem_str = f"\nset_option trace.profiler true in\nset_option trace.profiler.threshold 0 in\nexample : ({input_expr}) = ({expected_equality}) := by\n {indented_rewrite_strat_str}\nend Test" combined_content = "".join(content) + theorem_str + "\n" return combined_content @@ -48,8 +45,8 @@ def run_tests(): input_values = read_benchmark_results(benchmark_results_fn) results = {} - if os.path.exists("coq_benchmark_results.json"): - with open("coq_benchmark_results.json", "r") as f: + if os.path.exists("lean_benchmark_results.json"): + with open("lean_benchmark_results.json", "r") as f: results = json.load(f) for key, test_case in input_values.items(): @@ -70,27 +67,41 @@ def run_tests(): print(f"Test {key} with '{rewrite_command}': SKIPPED") continue - coq_benchmark_content = get_theorem_with_file_content( + lean_benchmark_content = get_theorem_with_file_content( context_fn, test_input, test_output, key, rewrite_strat ) - test_filename = f"test_{key}.v" + test_filename = f"test_{key}.lean" with open(test_filename, "w") as f: - f.write(coq_benchmark_content) + f.write(lean_benchmark_content) - # Time how long it takes to run "coqc test_{key}.v" + # Time how long it takes to run "lean test_{key}.lean" start_time = time.time() result = subprocess.run( - [program, test_filename], stdout=subprocess.PIPE, stderr=subprocess.PIPE + [program, test_filename], + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + check=False, ) elapsed_time = time.time() - start_time - vo_filename = f"test_{key}.vo" + times = re.findall(r"\[Elab.command\] \[(\d+\.\d+)\] example", result.stdout.decode("utf-8")) + rewrite_result = { "rewrite_command": rewrite_strat.strip(), - "status": "PASSED" if os.path.exists(vo_filename) else "FAILED", - "time": elapsed_time if os.path.exists(vo_filename) else None, - } + "status": "PASSED" if result.returncode == 0 else "FAILED", + "file_time": elapsed_time if result.returncode == 0 else None, + "time": max(map(float, times)) if len(times) != 0 else None, + } | ( + {} + if result.returncode == 0 or len(times) != 1 + else { + "stdout": result.stdout.decode("utf-8"), + "stderr": result.stderr.decode("utf-8"), + "returncode": result.returncode, + "times": times, + } + ) results[key][rewrite_strat.strip()] = rewrite_result print( @@ -100,7 +111,7 @@ def run_tests(): for file in glob.glob(f"test_{key}.*") + glob.glob(f".test_{key}.*"): os.remove(file) - with open("coq_benchmark_results.json", "w") as f: + with open("lean_benchmark_results.json", "w") as f: json.dump(results, f, indent=4) return results diff --git a/benchmark/rewrite_with_eq_haa_a/base.lean b/benchmark/rewrite_with_eq_haa_a/base.lean new file mode 100644 index 0000000..b63e786 --- /dev/null +++ b/benchmark/rewrite_with_eq_haa_a/base.lean @@ -0,0 +1,8 @@ +import Std.Tactic +section Test + +variable {α : Type} + +variable (f : α → α) (g : α → α) (h : α → α → α) +variable (a b c : α) +variable (eq_haa_a : ∀ x y : α, (h x y) = c) diff --git a/benchmark/rewrite_with_eq_haa_a/lean_benchmark.py b/benchmark/rewrite_with_eq_haa_a/lean_benchmark.py index 71c424c..e527883 100644 --- a/benchmark/rewrite_with_eq_haa_a/lean_benchmark.py +++ b/benchmark/rewrite_with_eq_haa_a/lean_benchmark.py @@ -3,23 +3,15 @@ import time import os import glob +import re -benchmark_results_fn = "mengine_benchmark_results.json" -context_fn = "base.v" -program = "coqc" +benchmark_results_fn = "mengine_benchmark_2_results.json" +context_fn = "base.lean" +program = "lean" -rewrite_strategies = [ - "repeat rewrite eq_haa_a.", - "rewrite! eq_haa_a.", - "rewrite_strat topdown eq_haa_a.", - "rewrite_strat bottomup eq_haa_a.", -] +rewrite_strategies = ["sorry", "repeat' rw [eq_haa_a]", "simp only [eq_haa_a]"] -SKIP_STRATEGIES = { - "repeat rewrite eq_haa_a.", - "rewrite! eq_haa_a.", - "rewrite_strat bottomup eq_haa_a.", -} +SKIP_STRATEGIES = {} def get_theorem_with_file_content( @@ -28,7 +20,8 @@ def get_theorem_with_file_content( with open(filename, "r") as file: content = file.readlines() - theorem_str = f"\nTheorem test_{index} : eq nat ({input_expr}) ({expected_equality}). Proof. {rewrite_strat_str} reflexivity. Qed. End Test." + indented_rewrite_strat_str = rewrite_strat_str.replace("\n", "\n ") + theorem_str = f"\nset_option trace.profiler true in\nset_option trace.profiler.threshold 0 in\nexample : ({input_expr}) = ({expected_equality}) := by\n {indented_rewrite_strat_str}\nend Test" combined_content = "".join(content) + theorem_str + "\n" return combined_content @@ -49,8 +42,8 @@ def run_tests(): input_values = read_benchmark_results(benchmark_results_fn) results = {} - if os.path.exists("coq_benchmark_results.json"): - with open("coq_benchmark_results.json", "r") as f: + if os.path.exists("lean_benchmark_results.json"): + with open("lean_benchmark_results.json", "r") as f: results = json.load(f) for key, test_case in input_values.items(): @@ -71,27 +64,44 @@ def run_tests(): print(f"Test {key} with '{rewrite_command}': SKIPPED") continue - coq_benchmark_content = get_theorem_with_file_content( + lean_benchmark_content = get_theorem_with_file_content( context_fn, test_input, test_output, key, rewrite_strat ) - test_filename = f"test_{key}.v" + test_filename = f"test_{key}.lean" with open(test_filename, "w") as f: - f.write(coq_benchmark_content) + f.write(lean_benchmark_content) - # Time how long it takes to run "coqc test_{key}.v" + # Time how long it takes to run "lean test_{key}.lean" start_time = time.time() result = subprocess.run( - [program, test_filename], stdout=subprocess.PIPE, stderr=subprocess.PIPE + [program, test_filename], + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + check=False, ) elapsed_time = time.time() - start_time - vo_filename = f"test_{key}.vo" + times = re.findall( + r"\[Elab.command\] \[(\d+\.\d+)\] example", + result.stdout.decode("utf-8"), + ) + rewrite_result = { "rewrite_command": rewrite_strat.strip(), - "status": "PASSED" if os.path.exists(vo_filename) else "FAILED", - "time": elapsed_time if os.path.exists(vo_filename) else None, - } + "status": "PASSED" if result.returncode == 0 else "FAILED", + "file_time": elapsed_time if result.returncode == 0 else None, + "time": max(map(float, times)) if len(times) != 0 else None, + } | ( + {} + if result.returncode == 0 or len(times) != 1 + else { + "stdout": result.stdout.decode("utf-8"), + "stderr": result.stderr.decode("utf-8"), + "returncode": result.returncode, + "times": times, + } + ) results[key][rewrite_strat.strip()] = rewrite_result print( @@ -101,7 +111,7 @@ def run_tests(): for file in glob.glob(f"test_{key}.*") + glob.glob(f".test_{key}.*"): os.remove(file) - with open("coq_benchmark_results.json", "w") as f: + with open("lean_benchmark_results.json", "w") as f: json.dump(results, f, indent=4) return results From c3e624beba5dec42c92976f6dce7ba552d4c7ecc Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 21 Apr 2025 08:59:13 -0700 Subject: [PATCH 4/4] Add benchmark results .json --- .../lean_benchmark_results.json | 6002 +++++++++++++++++ .../lean_benchmark_results.json | 842 +++ 2 files changed, 6844 insertions(+) create mode 100644 benchmark/rewrite_with_eq_f_a/lean_benchmark_results.json create mode 100644 benchmark/rewrite_with_eq_haa_a/lean_benchmark_results.json diff --git a/benchmark/rewrite_with_eq_f_a/lean_benchmark_results.json b/benchmark/rewrite_with_eq_f_a/lean_benchmark_results.json new file mode 100644 index 0000000..5b8008f --- /dev/null +++ b/benchmark/rewrite_with_eq_f_a/lean_benchmark_results.json @@ -0,0 +1,6002 @@ +{ + "0": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.7350902557373047, + "time": 0.000883 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 0.7478201389312744, + "time": 0.00133 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.7401230335235596, + "time": 0.001441 + } + }, + "1": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.7194581031799316, + "time": 0.000855 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 0.7615070343017578, + "time": 0.001593 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.7270128726959229, + "time": 0.001429 + } + }, + "2": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.7255358695983887, + "time": 0.000801 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 0.7649290561676025, + "time": 0.001854 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.7444310188293457, + "time": 0.001475 + } + }, + "3": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.7565460205078125, + "time": 0.000916 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 0.7345900535583496, + "time": 0.001407 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.7021269798278809, + "time": 0.001475 + } + }, + "4": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.7412252426147461, + "time": 0.00093 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 0.7371597290039062, + "time": 0.001447 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.731295108795166, + "time": 0.001475 + } + }, + "5": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.7335538864135742, + "time": 0.00095 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 0.7177119255065918, + "time": 0.001349 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.7148211002349854, + "time": 0.001453 + } + }, + "6": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.7118360996246338, + "time": 0.001028 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 0.8069698810577393, + "time": 0.00517 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.7496402263641357, + "time": 0.002121 + } + }, + "7": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.6962101459503174, + "time": 0.001079 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 0.8138031959533691, + "time": 0.005114 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.7732329368591309, + "time": 0.002255 + } + }, + "8": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.7481558322906494, + "time": 0.001318 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 0.8391921520233154, + "time": 0.005289 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.768826961517334, + "time": 0.002073 + } + }, + "9": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.7169101238250732, + "time": 0.001236 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 0.8378801345825195, + "time": 0.005427 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.7651362419128418, + "time": 0.002286 + } + }, + "10": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.7170360088348389, + "time": 0.001124 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 0.8474900722503662, + "time": 0.005502 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.7819240093231201, + "time": 0.002248 + } + }, + "11": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.0026040077209473, + "time": 0.001083 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 0.8642160892486572, + "time": 0.005599 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.6844370365142822, + "time": 0.002261 + } + }, + "12": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.733248233795166, + "time": 0.001262 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 0.9698941707611084, + "time": 0.009125 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.7646751403808594, + "time": 0.002914 + } + }, + "13": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.7446479797363281, + "time": 0.001292 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 0.9898109436035156, + "time": 0.008794 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.7631099224090576, + "time": 0.00294 + } + }, + "14": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.7214272022247314, + "time": 0.001271 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 0.9726839065551758, + "time": 0.008682 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.7717831134796143, + "time": 0.002949 + } + }, + "15": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.744102954864502, + "time": 0.001615 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 1.0447664260864258, + "time": 0.009343 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.758903980255127, + "time": 0.003004 + } + }, + "16": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.7214539051055908, + "time": 0.001326 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 1.046921968460083, + "time": 0.00957 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.7706329822540283, + "time": 0.003086 + } + }, + "17": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.7724690437316895, + "time": 0.001364 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 1.0504150390625, + "time": 0.009411 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.7580718994140625, + "time": 0.002945 + } + }, + "18": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.7450540065765381, + "time": 0.001529 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 1.2173268795013428, + "time": 0.01246 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.8103129863739014, + "time": 0.003724 + } + }, + "19": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.778792142868042, + "time": 0.00148 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 1.2282700538635254, + "time": 0.013265 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.8981742858886719, + "time": 0.00491 + } + }, + "20": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.8029861450195312, + "time": 0.001634 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 1.2488420009613037, + "time": 0.013959 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.8385117053985596, + "time": 0.004166 + } + }, + "21": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.7612817287445068, + "time": 0.001585 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 1.379037857055664, + "time": 0.013874 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.8539168834686279, + "time": 0.004393 + } + }, + "22": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.7550239562988281, + "time": 0.002383 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 1.365036964416504, + "time": 0.013418 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.8142547607421875, + "time": 0.003793 + } + }, + "23": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.8323419094085693, + "time": 0.001855 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 1.324747085571289, + "time": 0.013482 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.8286752700805664, + "time": 0.003962 + } + }, + "24": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.7359652519226074, + "time": 0.001663 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 1.5862960815429688, + "time": 0.016254 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.85207200050354, + "time": 0.004513 + } + }, + "25": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.766887903213501, + "time": 0.001664 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 1.5530650615692139, + "time": 0.015981 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.8348379135131836, + "time": 0.004601 + } + }, + "26": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.7627568244934082, + "time": 0.001691 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 1.574591875076294, + "time": 0.018556 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.8397440910339355, + "time": 0.004934 + } + }, + "27": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.7530372142791748, + "time": 0.001725 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 1.7327280044555664, + "time": 0.017451 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.8642828464508057, + "time": 0.004736 + } + }, + "28": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.76236891746521, + "time": 0.00171 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 1.7254438400268555, + "time": 0.017976 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.8693480491638184, + "time": 0.004555 + } + }, + "29": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.7727711200714111, + "time": 0.001703 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 1.7655110359191895, + "time": 0.018214 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.9029557704925537, + "time": 0.004594 + } + }, + "30": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.7710587978363037, + "time": 0.001984 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 1.9650180339813232, + "time": 0.020892 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.9656169414520264, + "time": 0.005759 + } + }, + "31": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.807548999786377, + "time": 0.001899 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 2.0223429203033447, + "time": 0.020452 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.9319250583648682, + "time": 0.00557 + } + }, + "32": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.8083939552307129, + "time": 0.0019 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 2.0585930347442627, + "time": 0.021069 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.929973840713501, + "time": 0.005459 + } + }, + "33": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.7996091842651367, + "time": 0.002048 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 2.235882043838501, + "time": 0.022417 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.9301052093505859, + "time": 0.005794 + } + }, + "34": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.7961759567260742, + "time": 0.001936 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 2.402233839035034, + "time": 0.024561 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.9014360904693604, + "time": 0.005361 + } + }, + "35": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.8378701210021973, + "time": 0.00197 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 2.2963478565216064, + "time": 0.022608 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.8976399898529053, + "time": 0.005352 + } + }, + "36": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.8092658519744873, + "time": 0.002161 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 2.5635879039764404, + "time": 0.025558 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.001786231994629, + "time": 0.006227 + } + }, + "37": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.8359251022338867, + "time": 0.002356 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 2.592353105545044, + "time": 0.029182 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.013274908065796, + "time": 0.006753 + } + }, + "38": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.8119144439697266, + "time": 0.002084 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 2.399066925048828, + "time": 0.024611 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.9503269195556641, + "time": 0.006176 + } + }, + "39": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.8327538967132568, + "time": 0.002198 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 2.748002052307129, + "time": 0.026966 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.9753520488739014, + "time": 0.006708 + } + }, + "40": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.8274481296539307, + "time": 0.002228 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 2.6804921627044678, + "time": 0.027658 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.9459998607635498, + "time": 0.006332 + } + }, + "41": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.8460948467254639, + "time": 0.002207 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 2.752502918243408, + "time": 0.027471 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 0.9662251472473145, + "time": 0.006204 + } + }, + "42": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.8784842491149902, + "time": 0.002338 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 2.796626329421997, + "time": 0.028275 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.0241541862487793, + "time": 0.007008 + } + }, + "43": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.8475830554962158, + "time": 0.002243 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 2.8258109092712402, + "time": 0.028088 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.0331411361694336, + "time": 0.007048 + } + }, + "44": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.8447060585021973, + "time": 0.002316 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 2.979936122894287, + "time": 0.028389 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.0538628101348877, + "time": 0.007049 + } + }, + "45": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.8609788417816162, + "time": 0.002291 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 3.210960865020752, + "time": 0.02994 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.0245509147644043, + "time": 0.00722 + } + }, + "46": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.0847978591918945, + "time": 0.002326 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 3.22324800491333, + "time": 0.029764 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.0328319072723389, + "time": 0.007891 + } + }, + "47": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.8530850410461426, + "time": 0.002376 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 3.275245189666748, + "time": 0.03015 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.0471580028533936, + "time": 0.007133 + } + }, + "48": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.9051148891448975, + "time": 0.002495 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 3.2075140476226807, + "time": 0.034393 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.1129510402679443, + "time": 0.00778 + } + }, + "49": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.8835799694061279, + "time": 0.00246 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 3.208301067352295, + "time": 0.031662 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.105813980102539, + "time": 0.008174 + } + }, + "50": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.8843860626220703, + "time": 0.002472 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 3.319719076156616, + "time": 0.03285 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.1511375904083252, + "time": 0.007724 + } + }, + "51": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.9144461154937744, + "time": 0.00252 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 3.6482677459716797, + "time": 0.034047 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.1206638813018799, + "time": 0.007953 + } + }, + "52": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.8897178173065186, + "time": 0.002492 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 3.677216053009033, + "time": 0.03481 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.1137840747833252, + "time": 0.007826 + } + }, + "53": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.8923220634460449, + "time": 0.002516 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 3.6187291145324707, + "time": 0.034363 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.1040940284729004, + "time": 0.007897 + } + }, + "54": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.9078831672668457, + "time": 0.002637 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 3.843144178390503, + "time": 0.037458 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.188344955444336, + "time": 0.008674 + } + }, + "55": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.9364511966705322, + "time": 0.002763 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 3.6646389961242676, + "time": 0.03604 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.1979970932006836, + "time": 0.008886 + } + }, + "56": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.9078378677368164, + "time": 0.002843 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 3.6881847381591797, + "time": 0.036988 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.1833221912384033, + "time": 0.008604 + } + }, + "57": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.211663007736206, + "time": 0.002815 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 4.252577066421509, + "time": 0.038917 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.1989030838012695, + "time": 0.008952 + } + }, + "58": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.9284679889678955, + "time": 0.002772 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 4.188676118850708, + "time": 0.037465 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.2112751007080078, + "time": 0.008903 + } + }, + "59": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.9116690158843994, + "time": 0.00277 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 4.239920139312744, + "time": 0.041073 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.200287103652954, + "time": 0.00899 + } + }, + "60": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.9901309013366699, + "time": 0.002929 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 4.07207465171814, + "time": 0.041188 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 2.2311697006225586, + "time": 0.009755 + } + }, + "61": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.0050549507141113, + "time": 0.002959 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 4.323975086212158, + "time": 0.042095 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.286633014678955, + "time": 0.00987 + } + }, + "62": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.9752509593963623, + "time": 0.002867 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 4.103655815124512, + "time": 0.039436 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.2416350841522217, + "time": 0.009572 + } + }, + "63": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.007904052734375, + "time": 0.002928 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 5.190962076187134, + "time": 0.057061 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.3182787895202637, + "time": 0.011421 + } + }, + "64": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.3951900005340576, + "time": 0.003453 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 4.973284721374512, + "time": 0.04615 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.430190086364746, + "time": 0.011354 + } + }, + "65": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.1127450466156006, + "time": 0.00346 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 5.413589000701904, + "time": 0.053322 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.3582229614257812, + "time": 0.013345 + } + }, + "66": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.091822624206543, + "time": 0.004049 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 5.748814821243286, + "time": 0.058369 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.5592701435089111, + "time": 0.012133 + } + }, + "67": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.0911390781402588, + "time": 0.003644 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 4.8697381019592285, + "time": 0.050517 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.4196369647979736, + "time": 0.011844 + } + }, + "68": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.0826737880706787, + "time": 0.003567 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 4.794892072677612, + "time": 0.052201 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.4408760070800781, + "time": 0.011372 + } + }, + "69": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.0685548782348633, + "time": 0.003541 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 5.621716022491455, + "time": 0.052759 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.4989631175994873, + "time": 0.012261 + } + }, + "70": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.1728780269622803, + "time": 0.005372 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 5.8059608936309814, + "time": 0.053453 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.4998600482940674, + "time": 0.011768 + } + }, + "71": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.1028070449829102, + "time": 0.003732 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 5.611236095428467, + "time": 0.052084 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.4767160415649414, + "time": 0.011958 + } + }, + "72": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.246953010559082, + "time": 0.004674 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 5.552953720092773, + "time": 0.061413 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.5501837730407715, + "time": 0.013135 + } + }, + "73": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.197563886642456, + "time": 0.004119 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 5.584265232086182, + "time": 0.052346 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.6147279739379883, + "time": 0.013586 + } + }, + "74": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 2.0941219329833984, + "time": 0.005109 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 5.966485023498535, + "time": 0.054176 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.5886220932006836, + "time": 0.012313 + } + }, + "75": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.194444179534912, + "time": 0.004152 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 6.754928112030029, + "time": 0.056558 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.6029088497161865, + "time": 0.012971 + } + }, + "76": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.3827991485595703, + "time": 0.004036 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 6.210253000259399, + "time": 0.056216 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.544957160949707, + "time": 0.012411 + } + }, + "77": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.1996231079101562, + "time": 0.004028 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 6.224717617034912, + "time": 0.056232 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.5558421611785889, + "time": 0.012934 + } + }, + "78": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.2306921482086182, + "time": 0.004123 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 5.719174146652222, + "time": 0.05845 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.710799217224121, + "time": 0.013576 + } + }, + "79": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.272486925125122, + "time": 0.004431 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 5.82331919670105, + "time": 0.056934 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.683241367340088, + "time": 0.013912 + } + }, + "80": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.2495698928833008, + "time": 0.004064 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 5.941896915435791, + "time": 0.060921 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.671952724456787, + "time": 0.013559 + } + }, + "81": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.2537510395050049, + "time": 0.003841 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 7.956910133361816, + "time": 0.065285 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.6798298358917236, + "time": 0.014708 + } + }, + "82": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.2529568672180176, + "time": 0.003803 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 8.052633047103882, + "time": 0.06508 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.7626209259033203, + "time": 0.015458 + } + }, + "83": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.2979907989501953, + "time": 0.004041 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 6.655357837677002, + "time": 0.060205 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.595616102218628, + "time": 0.012583 + } + }, + "84": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.5319581031799316, + "time": 0.003746 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 6.21262788772583, + "time": 0.06902 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.7317030429840088, + "time": 0.013887 + } + }, + "85": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.2794189453125, + "time": 0.004149 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 6.446397066116333, + "time": 0.060882 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.8488667011260986, + "time": 0.014689 + } + }, + "86": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.3370070457458496, + "time": 0.004084 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 6.4751739501953125, + "time": 0.05901 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 2.0739400386810303, + "time": 0.014822 + } + }, + "87": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.2810142040252686, + "time": 0.004131 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 7.347712993621826, + "time": 0.067667 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.7867591381072998, + "time": 0.01439 + } + }, + "88": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.3465142250061035, + "time": 0.003998 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 7.651128053665161, + "time": 0.067057 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.8240299224853516, + "time": 0.013589 + } + }, + "89": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.3236098289489746, + "time": 0.004229 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 7.664601802825928, + "time": 0.065194 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.8601250648498535, + "time": 0.015688 + } + }, + "90": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.4281468391418457, + "time": 0.004667 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 6.8955979347229, + "time": 0.070366 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 2.170593023300171, + "time": 0.016204 + } + }, + "91": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.4074110984802246, + "time": 0.003982 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 6.786040782928467, + "time": 0.072374 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.9076111316680908, + "time": 0.014753 + } + }, + "92": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.395293951034546, + "time": 0.004296 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 6.898855924606323, + "time": 0.06291 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 1.959507942199707, + "time": 0.015179 + } + }, + "93": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.4734032154083252, + "time": 0.004593 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 7.9109179973602295, + "time": 0.075965 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 2.0904128551483154, + "time": 0.015994 + } + }, + "94": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.4978318214416504, + "time": 0.004996 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 7.922405958175659, + "time": 0.072083 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 2.0321738719940186, + "time": 0.016191 + } + }, + "95": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.4801058769226074, + "time": 0.004803 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 8.231348991394043, + "time": 0.104933 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 2.411436080932617, + "time": 0.034842 + } + }, + "96": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.6088950634002686, + "time": 0.004443 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 8.390426874160767, + "time": 0.08273 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 2.2271039485931396, + "time": 0.017631 + } + }, + "97": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.6517078876495361, + "time": 0.00479 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 7.854856014251709, + "time": 0.075527 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 2.1250150203704834, + "time": 0.016446 + } + }, + "98": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.8491308689117432, + "time": 0.005727 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 7.87432599067688, + "time": 0.108471 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 2.1341490745544434, + "time": 0.016602 + } + }, + "99": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.5443921089172363, + "time": 0.004843 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 8.550456047058105, + "time": 0.081228 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 2.024733066558838, + "time": 0.016237 + } + }, + "100": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.519801139831543, + "time": 0.004721 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 8.761614084243774, + "time": 0.099022 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 2.066896915435791, + "time": 0.015921 + } + }, + "101": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.7373411655426025, + "time": 0.004664 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 9.165280103683472, + "time": 0.077645 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 2.1161508560180664, + "time": 0.033271 + } + }, + "102": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.9142577648162842, + "time": 0.004955 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 7.686340093612671, + "time": 0.071498 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 2.1291377544403076, + "time": 0.017275 + } + }, + "103": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.6381680965423584, + "time": 0.004623 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 7.948138952255249, + "time": 0.073284 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 2.2217178344726562, + "time": 0.018348 + } + }, + "104": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.9998548030853271, + "time": 0.004756 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 7.777297019958496, + "time": 0.074739 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 2.228321075439453, + "time": 0.016795 + } + }, + "105": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 2.569708824157715, + "time": 0.004715 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 8.946670055389404, + "time": 0.080404 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 2.206556797027588, + "time": 0.018916 + } + }, + "106": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.6327059268951416, + "time": 0.005048 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 8.993581056594849, + "time": 0.079555 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 2.284188985824585, + "time": 0.016986 + } + }, + "107": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.6425368785858154, + "time": 0.004838 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 8.937113046646118, + "time": 0.078164 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 2.188286781311035, + "time": 0.017635 + } + }, + "108": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 2.0831189155578613, + "time": 0.007171 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 8.224005222320557, + "time": 0.079833 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 2.381450891494751, + "time": 0.019191 + } + }, + "109": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.74033784866333, + "time": 0.005019 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 8.264924049377441, + "time": 0.093824 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 2.3444600105285645, + "time": 0.018507 + } + }, + "110": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.7950196266174316, + "time": 0.005114 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 8.342272996902466, + "time": 0.080056 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 2.365194320678711, + "time": 0.018365 + } + }, + "111": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.8600969314575195, + "time": 0.005562 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 10.034291982650757, + "time": 0.08774 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 2.3637161254882812, + "time": 0.0184 + } + }, + "112": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.7703759670257568, + "time": 0.005283 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 10.120511054992676, + "time": 0.089362 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 2.522998809814453, + "time": 0.030182 + } + }, + "113": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 2.002563714981079, + "time": 0.005319 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 10.135350942611694, + "time": 0.09519 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 2.7764317989349365, + "time": 0.019869 + } + }, + "114": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.907752275466919, + "time": 0.005491 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 9.104376792907715, + "time": 0.084932 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 2.885845899581909, + "time": 0.024636 + } + }, + "115": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.9638090133666992, + "time": 0.00563 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 9.31623888015747, + "time": 0.086938 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 2.571776866912842, + "time": 0.019552 + } + }, + "116": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.901399850845337, + "time": 0.005165 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 8.821898937225342, + "time": 0.08436 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 2.5329370498657227, + "time": 0.019517 + } + }, + "117": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.9138448238372803, + "time": 0.00587 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 10.486491918563843, + "time": 0.093005 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 2.5910301208496094, + "time": 0.019562 + } + }, + "118": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.9680531024932861, + "time": 0.005904 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 10.620792150497437, + "time": 0.103746 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 2.6028029918670654, + "time": 0.020264 + } + }, + "119": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 2.1684131622314453, + "time": 0.005515 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 11.339513778686523, + "time": 0.099998 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 2.8352560997009277, + "time": 0.021629 + } + }, + "120": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 2.1209793090820312, + "time": 0.006089 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 9.823787927627563, + "time": 0.097005 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 2.776898145675659, + "time": 0.020835 + } + }, + "121": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 2.0603840351104736, + "time": 0.005737 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 9.713947296142578, + "time": 0.089925 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 3.2108781337738037, + "time": 0.020663 + } + }, + "122": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 2.267788887023926, + "time": 0.005573 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 9.981397151947021, + "time": 0.091144 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 2.9378111362457275, + "time": 0.022106 + } + }, + "123": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 2.1334378719329834, + "time": 0.006047 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 11.600334882736206, + "time": 0.098866 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 2.818049907684326, + "time": 0.021266 + } + }, + "124": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 2.0979180335998535, + "time": 0.005861 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 11.104416131973267, + "time": 0.098099 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 2.8646907806396484, + "time": 0.021465 + } + }, + "125": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 2.204103946685791, + "time": 0.006103 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 11.992074012756348, + "time": 0.161671 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 2.847723960876465, + "time": 0.021449 + } + }, + "126": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 2.335170030593872, + "time": 0.006265 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 10.354674100875854, + "time": 0.097926 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 3.4801647663116455, + "time": 0.023445 + } + }, + "127": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 2.655348062515259, + "time": 0.007675 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 10.241556882858276, + "time": 0.101306 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 3.049708604812622, + "time": 0.022665 + } + }, + "128": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 2.3561031818389893, + "time": 0.005988 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 10.568835258483887, + "time": 0.105843 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 2.9799489974975586, + "time": 0.023435 + } + }, + "129": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 2.2454259395599365, + "time": 0.005515 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 11.48874306678772, + "time": 0.102397 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 2.9264137744903564, + "time": 0.02098 + } + }, + "130": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 2.3645739555358887, + "time": 0.005719 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 11.460751056671143, + "time": 0.097848 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 3.0653798580169678, + "time": 0.020927 + } + }, + "131": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 2.15933895111084, + "time": 0.005364 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 11.50325083732605, + "time": 0.102391 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 2.8595972061157227, + "time": 0.021168 + } + }, + "132": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 2.360929012298584, + "time": 0.006106 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 10.304242849349976, + "time": 0.09653 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 3.040066957473755, + "time": 0.02149 + } + }, + "133": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 2.360975742340088, + "time": 0.006375 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 10.198055982589722, + "time": 0.094099 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 3.1823811531066895, + "time": 0.021677 + } + }, + "134": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 2.3714590072631836, + "time": 0.005617 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 10.808421850204468, + "time": 0.097333 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 3.19140887260437, + "time": 0.037052 + } + }, + "135": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 2.5971009731292725, + "time": 0.011561 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 12.459275960922241, + "time": 0.102749 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 3.1090550422668457, + "time": 0.022151 + } + }, + "136": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 2.415022850036621, + "time": 0.005682 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 13.070015907287598, + "time": 0.10197 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 3.861341953277588, + "time": 0.062453 + } + }, + "137": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 3.4260830879211426, + "time": 0.005784 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 12.60627007484436, + "time": 0.10951 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 3.1986896991729736, + "time": 0.022158 + } + }, + "138": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 2.638713836669922, + "time": 0.006109 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 11.511609077453613, + "time": 0.106231 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 3.7443158626556396, + "time": 0.025747 + } + }, + "139": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 2.6865148544311523, + "time": 0.006532 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 11.586596250534058, + "time": 0.115196 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 3.3653500080108643, + "time": 0.023814 + } + }, + "140": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 2.564988136291504, + "time": 0.005981 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 11.464277029037476, + "time": 0.103246 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 3.58044695854187, + "time": 0.049919 + } + }, + "141": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 2.6683530807495117, + "time": 0.006229 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 13.217878818511963, + "time": 0.117538 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 3.5026309490203857, + "time": 0.023987 + } + }, + "142": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 2.652554988861084, + "time": 0.00641 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 13.489537000656128, + "time": 0.125335 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 3.3916780948638916, + "time": 0.026367 + } + }, + "143": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 2.5724799633026123, + "time": 0.006088 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 13.016549348831177, + "time": 0.10871 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 3.389700174331665, + "time": 0.023822 + } + }, + "144": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 3.0787761211395264, + "time": 0.006023 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 11.740684032440186, + "time": 0.113765 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 3.624173164367676, + "time": 0.025258 + } + }, + "145": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 2.781749963760376, + "time": 0.006399 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 11.925742149353027, + "time": 0.107056 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 3.687246084213257, + "time": 0.034688 + } + }, + "146": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 2.803123950958252, + "time": 0.006471 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 11.988964080810547, + "time": 0.110467 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 3.6310267448425293, + "time": 0.025817 + } + }, + "147": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 2.8120529651641846, + "time": 0.006301 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 14.671335220336914, + "time": 0.128771 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 3.967647075653076, + "time": 0.025329 + } + }, + "148": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 2.8726038932800293, + "time": 0.00648 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 14.050913572311401, + "time": 0.1208 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 4.972477912902832, + "time": 0.025969 + } + }, + "149": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 2.805608034133911, + "time": 0.006513 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 13.805318832397461, + "time": 0.125061 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 4.335371971130371, + "time": 0.029355 + } + }, + "150": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 3.812429189682007, + "time": 0.019909 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 13.897647142410278, + "time": 0.141021 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 4.319488048553467, + "time": 0.036866 + } + }, + "151": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 3.347938060760498, + "time": 0.007625 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 14.116249084472656, + "time": 0.13013 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 4.603774070739746, + "time": 0.03291 + } + }, + "152": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 3.5122969150543213, + "time": 0.007528 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 14.582941055297852, + "time": 0.141465 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 4.784820079803467, + "time": 0.033306 + } + }, + "153": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 3.893594980239868, + "time": 0.00803 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 18.877788305282593, + "time": 0.282988 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 4.683196306228638, + "time": 0.029009 + } + }, + "154": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 3.452301025390625, + "time": 0.008562 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 16.808122873306274, + "time": 0.153705 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 4.469871759414673, + "time": 0.029406 + } + }, + "155": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 3.331237316131592, + "time": 0.007735 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 15.947928667068481, + "time": 0.152245 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 4.488004922866821, + "time": 0.03072 + } + }, + "156": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 3.712599039077759, + "time": 0.00841 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 14.610895872116089, + "time": 0.13359 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 4.960978031158447, + "time": 0.037035 + } + }, + "157": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 3.893843173980713, + "time": 0.00807 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 14.644283056259155, + "time": 0.136106 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 4.6063361167907715, + "time": 0.031011 + } + }, + "158": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 3.507169008255005, + "time": 0.00744 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 15.04760193824768, + "time": 0.132482 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 5.215080976486206, + "time": 0.054028 + } + }, + "159": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 3.8385109901428223, + "time": 0.008473 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 19.195845127105713, + "time": 0.157371 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 5.147419691085815, + "time": 0.040629 + } + }, + "160": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 3.7430238723754883, + "time": 0.0084 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 18.2951819896698, + "time": 0.154547 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 4.999799966812134, + "time": 0.032674 + } + }, + "161": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 3.6370761394500732, + "time": 0.008488 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 17.186023950576782, + "time": 0.154519 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 4.8472089767456055, + "time": 0.034173 + } + }, + "162": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 3.96807599067688, + "time": 0.008234 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 15.45729684829712, + "time": 0.147856 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 5.10429310798645, + "time": 0.031054 + } + }, + "163": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 5.0038111209869385, + "time": 0.007413 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 15.09183382987976, + "time": 0.158298 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 5.272234916687012, + "time": 0.034775 + } + }, + "164": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 3.8757121562957764, + "time": 0.007504 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 15.419461965560913, + "time": 0.141276 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 5.002568006515503, + "time": 0.032321 + } + }, + "165": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 3.9343881607055664, + "time": 0.008316 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 17.629419088363647, + "time": 0.141764 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 5.13456392288208, + "time": 0.031566 + } + }, + "166": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 3.859009027481079, + "time": 0.007649 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 16.85580539703369, + "time": 0.148484 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 4.96799111366272, + "time": 0.031596 + } + }, + "167": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 3.6824591159820557, + "time": 0.007527 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 17.965532064437866, + "time": 0.159734 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 4.91981315612793, + "time": 0.031368 + } + }, + "168": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 4.004571199417114, + "time": 0.007741 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 15.371582984924316, + "time": 0.139261 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 5.367386817932129, + "time": 0.034931 + } + }, + "169": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 4.298450946807861, + "time": 0.007742 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 15.463727951049805, + "time": 0.137812 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 5.297884941101074, + "time": 0.031681 + } + }, + "170": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 4.003926992416382, + "time": 0.007756 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 15.448683977127075, + "time": 0.149203 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 5.251617908477783, + "time": 0.033118 + } + }, + "171": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 4.139923810958862, + "time": 0.007923 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 17.78489398956299, + "time": 0.150411 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 5.218008995056152, + "time": 0.031563 + } + }, + "172": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 4.0806028842926025, + "time": 0.008578 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 17.650738954544067, + "time": 0.147862 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 5.044683933258057, + "time": 0.03272 + } + }, + "173": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 4.02234411239624, + "time": 0.007111 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 18.479049921035767, + "time": 0.148671 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 5.300225019454956, + "time": 0.03273 + } + }, + "174": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 4.410549879074097, + "time": 0.007564 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 15.499789953231812, + "time": 0.136797 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 5.508315801620483, + "time": 0.031514 + } + }, + "175": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 4.349325895309448, + "time": 0.008275 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 15.818475008010864, + "time": 0.144085 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 5.876483917236328, + "time": 0.035204 + } + }, + "176": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 4.235641956329346, + "time": 0.007554 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 16.248537063598633, + "time": 0.142221 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 5.51904296875, + "time": 0.031513 + } + }, + "177": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 4.242016077041626, + "time": 0.008104 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 17.879048824310303, + "time": 0.145147 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 5.461963891983032, + "time": 0.033464 + } + }, + "178": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 4.347228765487671, + "time": 0.007727 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 19.876413106918335, + "time": 0.155999 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 5.293383836746216, + "time": 0.032164 + } + }, + "179": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 4.592893123626709, + "time": 0.008323 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 19.605719089508057, + "time": 0.200702 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 6.525459051132202, + "time": 0.048557 + } + }, + "180": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 4.656375169754028, + "time": 0.007957 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 17.5699200630188, + "time": 0.154627 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 6.594853162765503, + "time": 0.034826 + } + }, + "181": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 5.56141209602356, + "time": 0.009896 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 17.25908398628235, + "time": 0.148113 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 6.437191009521484, + "time": 0.035518 + } + }, + "182": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 5.119482040405273, + "time": 0.007992 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 18.606279134750366, + "time": 0.152761 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 9.485447883605957, + "time": 0.045905 + } + }, + "183": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 4.686275243759155, + "time": 0.008368 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 19.33291506767273, + "time": 0.160034 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 6.0193939208984375, + "time": 0.034456 + } + }, + "184": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 4.65782904624939, + "time": 0.008643 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 19.637306213378906, + "time": 0.157913 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 5.662448883056641, + "time": 0.034023 + } + }, + "185": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 4.6234941482543945, + "time": 0.007994 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 19.432175874710083, + "time": 0.156133 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 5.821631908416748, + "time": 0.036307 + } + }, + "186": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 5.0937700271606445, + "time": 0.008519 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 17.684693098068237, + "time": 0.152807 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 6.962913990020752, + "time": 0.035321 + } + }, + "187": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 5.350303888320923, + "time": 0.008707 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 18.889775037765503, + "time": 0.156289 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 6.09384298324585, + "time": 0.035642 + } + }, + "188": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 5.145370960235596, + "time": 0.00824 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 17.711332082748413, + "time": 0.156626 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 6.2971930503845215, + "time": 0.038546 + } + }, + "189": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 5.19140100479126, + "time": 0.008854 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 23.377272844314575, + "time": 0.176073 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 6.6270668506622314, + "time": 0.038783 + } + }, + "190": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 5.7842857837677, + "time": 0.010385 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 21.08632516860962, + "time": 0.167584 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 6.539060115814209, + "time": 0.03707 + } + }, + "191": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 5.26043701171875, + "time": 0.008801 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 21.27437114715576, + "time": 0.205019 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 6.375905990600586, + "time": 0.036363 + } + }, + "192": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 5.355807065963745, + "time": 0.008568 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 18.948894023895264, + "time": 0.165767 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 6.358793020248413, + "time": 0.038563 + } + }, + "193": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 5.22670316696167, + "time": 0.009069 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 18.68034601211548, + "time": 0.190556 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 6.654735088348389, + "time": 0.038491 + } + }, + "194": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 5.349934101104736, + "time": 0.008733 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 19.698637008666992, + "time": 0.163962 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 6.649734258651733, + "time": 0.040172 + } + }, + "195": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 5.65958571434021, + "time": 0.008972 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 21.471712827682495, + "time": 0.175206 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 6.859411001205444, + "time": 0.037153 + } + }, + "196": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 5.455487012863159, + "time": 0.008674 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 21.426718950271606, + "time": 0.171627 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 6.9911208152771, + "time": 0.036698 + } + }, + "197": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 5.715234041213989, + "time": 0.008907 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 21.41647505760193, + "time": 0.179455 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 6.742023944854736, + "time": 0.038643 + } + }, + "198": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 6.15899920463562, + "time": 0.009072 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 20.13956093788147, + "time": 0.174832 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 7.40667986869812, + "time": 0.03893 + } + }, + "199": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 5.854755163192749, + "time": 0.009674 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 19.941143035888672, + "time": 0.1952 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 7.560232162475586, + "time": 0.040931 + } + }, + "200": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 6.788617134094238, + "time": 0.019179 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 21.858269929885864, + "time": 0.186225 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 7.263118028640747, + "time": 0.0406 + } + }, + "201": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 5.81430196762085, + "time": 0.009137 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 22.611768007278442, + "time": 0.187702 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 7.332568168640137, + "time": 0.041361 + } + }, + "202": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 5.725096940994263, + "time": 0.009162 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 22.934152841567993, + "time": 0.179235 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 7.354980230331421, + "time": 0.039517 + } + }, + "203": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 5.798872947692871, + "time": 0.009361 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 22.844717264175415, + "time": 0.181154 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 7.10832405090332, + "time": 0.041119 + } + }, + "204": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 6.038067817687988, + "time": 0.009399 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 19.705931901931763, + "time": 0.17127 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 7.262800931930542, + "time": 0.040098 + } + }, + "205": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 5.994193077087402, + "time": 0.009366 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 19.86979389190674, + "time": 0.174158 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 7.608596324920654, + "time": 0.041439 + } + }, + "206": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 6.004204988479614, + "time": 0.009529 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 19.866877794265747, + "time": 0.172336 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 7.314067840576172, + "time": 0.044431 + } + }, + "207": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 6.116076946258545, + "time": 0.009234 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 24.895788192749023, + "time": 0.264338 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 8.169997215270996, + "time": 0.044663 + } + }, + "208": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 6.318005084991455, + "time": 0.009497 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 24.133904933929443, + "time": 0.297494 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 7.738690137863159, + "time": 0.040283 + } + }, + "209": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 6.558481931686401, + "time": 0.018427 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 23.362810134887695, + "time": 0.186586 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 7.930721998214722, + "time": 0.040789 + } + }, + "210": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 7.68327784538269, + "time": 0.009959 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 22.29646587371826, + "time": 0.179204 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 8.248722791671753, + "time": 0.043248 + } + }, + "211": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 6.564267873764038, + "time": 0.009703 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 21.26054573059082, + "time": 0.181157 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 8.444547176361084, + "time": 0.044186 + } + }, + "212": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 6.62457275390625, + "time": 0.010124 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 22.842177867889404, + "time": 0.179508 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 8.172792911529541, + "time": 0.041765 + } + }, + "213": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 6.631825923919678, + "time": 0.00932 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 24.26097798347473, + "time": 0.195591 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 8.18758511543274, + "time": 0.042326 + } + }, + "214": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 6.707063674926758, + "time": 0.00935 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 24.31370234489441, + "time": 0.198366 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 9.83755111694336, + "time": 0.041722 + } + }, + "215": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 6.7809460163116455, + "time": 0.00992 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 25.67803406715393, + "time": 0.190832 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 8.232170104980469, + "time": 0.043329 + } + }, + "216": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 7.221905946731567, + "time": 0.009528 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 22.678386926651, + "time": 0.189155 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 8.739809036254883, + "time": 0.045381 + } + }, + "217": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 7.173727035522461, + "time": 0.009733 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 22.4657940864563, + "time": 0.204078 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 8.546941995620728, + "time": 0.044505 + } + }, + "218": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 7.194560766220093, + "time": 0.010263 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 22.023898124694824, + "time": 0.191341 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 8.711670160293579, + "time": 0.043065 + } + }, + "219": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 7.148456811904907, + "time": 0.010052 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 25.877375841140747, + "time": 0.205941 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 8.89449691772461, + "time": 0.046774 + } + }, + "220": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 7.620414972305298, + "time": 0.011054 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 24.82752799987793, + "time": 0.245042 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 8.699872016906738, + "time": 0.044087 + } + }, + "221": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 7.037132740020752, + "time": 0.009845 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 25.084280967712402, + "time": 0.199371 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 8.637229204177856, + "time": 0.043197 + } + }, + "222": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 7.4896039962768555, + "time": 0.010066 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 22.75533699989319, + "time": 0.191819 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 9.063244104385376, + "time": 0.045916 + } + }, + "223": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 7.476119041442871, + "time": 0.009891 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 22.643161058425903, + "time": 0.190261 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 9.18510890007019, + "time": 0.044875 + } + }, + "224": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 7.513121128082275, + "time": 0.010187 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 22.644144296646118, + "time": 0.193719 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 9.117407083511353, + "time": 0.044994 + } + }, + "225": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 7.546137809753418, + "time": 0.010106 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 25.940497159957886, + "time": 0.203863 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 9.278295040130615, + "time": 0.044285 + } + }, + "226": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 7.579575061798096, + "time": 0.010212 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 26.68282389640808, + "time": 0.201895 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 8.94193720817566, + "time": 0.043232 + } + }, + "227": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 7.650964021682739, + "time": 0.009798 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 25.13873291015625, + "time": 0.195503 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 8.785704851150513, + "time": 0.043944 + } + }, + "228": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 7.693099021911621, + "time": 0.009599 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 25.735630750656128, + "time": 0.185835 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 9.18382215499878, + "time": 0.046941 + } + }, + "229": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 7.509793996810913, + "time": 0.008956 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 22.656394958496094, + "time": 0.183878 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 9.004374980926514, + "time": 0.044603 + } + }, + "230": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 7.375241994857788, + "time": 0.009104 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 22.708894968032837, + "time": 0.18294 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 10.032693147659302, + "time": 0.042405 + } + }, + "231": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 8.575001001358032, + "time": 0.009008 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 25.987042665481567, + "time": 0.195772 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 9.403833150863647, + "time": 0.043335 + } + }, + "232": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 8.69115424156189, + "time": 0.009234 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 26.03978681564331, + "time": 0.195421 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 9.25705885887146, + "time": 0.045757 + } + }, + "233": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 7.750468015670776, + "time": 0.009563 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 26.543960094451904, + "time": 0.216262 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 10.189527750015259, + "time": 0.043293 + } + }, + "234": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 8.524588108062744, + "time": 0.010203 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 23.712034940719604, + "time": 0.189762 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 10.110649108886719, + "time": 0.045176 + } + }, + "235": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 8.033828258514404, + "time": 0.009468 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 23.505497217178345, + "time": 0.190367 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 9.603879928588867, + "time": 0.045184 + } + }, + "236": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 8.219563961029053, + "time": 0.010051 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 23.6560378074646, + "time": 0.18822 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 9.68465805053711, + "time": 0.046533 + } + }, + "237": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 8.091217756271362, + "time": 0.00984 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 27.201131105422974, + "time": 0.207587 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 9.855699300765991, + "time": 0.045798 + } + }, + "238": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 8.186394929885864, + "time": 0.010008 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 27.34490394592285, + "time": 0.258722 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 10.060492038726807, + "time": 0.046703 + } + }, + "239": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 8.252209901809692, + "time": 0.010007 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 27.673371076583862, + "time": 0.207923 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 9.97229790687561, + "time": 0.046738 + } + }, + "240": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 8.825581073760986, + "time": 0.011172 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 25.085707187652588, + "time": 0.20292 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 10.405694961547852, + "time": 0.048263 + } + }, + "241": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 8.91231894493103, + "time": 0.010733 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 25.155667304992676, + "time": 0.204155 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 10.90853500366211, + "time": 0.04901 + } + }, + "242": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 8.99104118347168, + "time": 0.010433 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 24.859973907470703, + "time": 0.204089 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 10.196735858917236, + "time": 0.047105 + } + }, + "243": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 8.490164041519165, + "time": 0.010031 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 28.42117929458618, + "time": 0.204781 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 10.383772373199463, + "time": 0.047594 + } + }, + "244": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 8.516018867492676, + "time": 0.009751 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 27.793233156204224, + "time": 0.209654 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 10.37963604927063, + "time": 0.047689 + } + }, + "245": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 8.492090225219727, + "time": 0.009914 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 27.994704008102417, + "time": 0.208616 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 10.438804864883423, + "time": 0.04759 + } + }, + "246": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 9.246500015258789, + "time": 0.010864 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 25.849801301956177, + "time": 0.209495 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 10.917785882949829, + "time": 0.050458 + } + }, + "247": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 9.332198858261108, + "time": 0.010272 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 25.779555082321167, + "time": 0.205885 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 10.92095685005188, + "time": 0.04748 + } + }, + "248": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 9.249906301498413, + "time": 0.010225 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 25.66155505180359, + "time": 0.208661 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 11.089126348495483, + "time": 0.04898 + } + }, + "249": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 9.300472736358643, + "time": 0.01027 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 29.447718143463135, + "time": 0.225018 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 10.968801975250244, + "time": 0.048672 + } + }, + "250": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 9.861871004104614, + "time": 0.010414 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 29.573914289474487, + "time": 0.219822 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 11.209389925003052, + "time": 0.048654 + } + }, + "251": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 9.40516710281372, + "time": 0.010381 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 29.913296222686768, + "time": 0.223141 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 11.02423095703125, + "time": 0.048889 + } + }, + "252": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 10.083806991577148, + "time": 0.010579 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 27.035192251205444, + "time": 0.212983 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 11.950433015823364, + "time": 0.052989 + } + }, + "253": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 10.005177021026611, + "time": 0.010733 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 27.23904585838318, + "time": 0.242223 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 11.799041986465454, + "time": 0.050137 + } + }, + "254": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 9.967985153198242, + "time": 0.010879 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 27.12341809272766, + "time": 0.211302 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 11.85167384147644, + "time": 0.049861 + } + }, + "255": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 10.278989791870117, + "time": 0.010794 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 30.715333938598633, + "time": 0.230508 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 11.947224140167236, + "time": 0.050093 + } + }, + "256": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 10.203636884689331, + "time": 0.010624 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 30.437997102737427, + "time": 0.225759 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 11.959658861160278, + "time": 0.049959 + } + }, + "257": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 10.350714206695557, + "time": 0.010399 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 30.488353967666626, + "time": 0.225611 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 11.706342935562134, + "time": 0.049834 + } + }, + "258": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 10.818267822265625, + "time": 0.010777 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 28.26418113708496, + "time": 0.21976 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 12.49133014678955, + "time": 0.052384 + } + }, + "259": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 11.195804834365845, + "time": 0.010873 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 28.151840686798096, + "time": 0.217198 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 12.642975807189941, + "time": 0.054638 + } + }, + "260": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 10.781151056289673, + "time": 0.011103 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 28.495614051818848, + "time": 0.222127 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 12.61122989654541, + "time": 0.051591 + } + }, + "261": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 10.899874210357666, + "time": 0.010842 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 31.98466420173645, + "time": 0.255556 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 13.811580181121826, + "time": 0.052007 + } + }, + "262": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 10.764832973480225, + "time": 0.01156 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 32.049763679504395, + "time": 0.232246 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 12.550452947616577, + "time": 0.052133 + } + }, + "263": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 11.248183250427246, + "time": 0.010941 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 32.15876293182373, + "time": 0.231273 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 12.697030782699585, + "time": 0.052779 + } + }, + "264": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 11.503968000411987, + "time": 0.011206 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 29.753844022750854, + "time": 0.227146 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 13.323865175247192, + "time": 0.053517 + } + }, + "265": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 11.430841207504272, + "time": 0.011495 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 29.18437910079956, + "time": 0.22398 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 13.320668935775757, + "time": 0.056667 + } + }, + "266": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 11.360448122024536, + "time": 0.011643 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 29.379112005233765, + "time": 0.22842 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 13.429013013839722, + "time": 0.055019 + } + }, + "267": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 11.614953994750977, + "time": 0.011606 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 33.35924196243286, + "time": 0.240838 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 13.25145697593689, + "time": 0.055671 + } + }, + "268": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 11.870740175247192, + "time": 0.011864 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 33.30381798744202, + "time": 0.239457 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 13.692065000534058, + "time": 0.055098 + } + }, + "269": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 11.76130199432373, + "time": 0.01121 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 33.38091993331909, + "time": 0.237963 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 13.384680986404419, + "time": 0.054025 + } + }, + "270": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 12.639455080032349, + "time": 0.011492 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 30.6114661693573, + "time": 0.230626 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 14.843575954437256, + "time": 0.055603 + } + }, + "271": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 12.783432006835938, + "time": 0.011881 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 31.104543924331665, + "time": 0.23295 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 14.274749279022217, + "time": 0.055781 + } + }, + "272": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 12.521270990371704, + "time": 0.01147 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 31.021848917007446, + "time": 0.246252 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 14.01247501373291, + "time": 0.055066 + } + }, + "273": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 12.432284116744995, + "time": 0.011579 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 35.729326009750366, + "time": 0.251062 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 14.33801007270813, + "time": 0.056122 + } + }, + "274": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 12.411168098449707, + "time": 0.011634 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 34.17066717147827, + "time": 0.237415 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 13.756453037261963, + "time": 0.054279 + } + }, + "275": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 12.346935987472534, + "time": 0.010926 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 34.652884006500244, + "time": 0.238174 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 13.60678219795227, + "time": 0.054619 + } + }, + "276": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 12.25676679611206, + "time": 0.010287 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 30.3574481010437, + "time": 0.228738 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 14.378377914428711, + "time": 0.053603 + } + }, + "277": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 12.758766889572144, + "time": 0.011967 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 30.986146926879883, + "time": 0.230288 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 14.302191019058228, + "time": 0.054498 + } + }, + "278": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 12.302060842514038, + "time": 0.01068 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 30.795047998428345, + "time": 0.227847 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 14.887660026550293, + "time": 0.056169 + } + }, + "279": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 12.58011794090271, + "time": 0.011104 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 34.99658989906311, + "time": 0.243223 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 14.571167945861816, + "time": 0.055641 + } + }, + "280": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 12.5055410861969, + "time": 0.011375 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 34.825201988220215, + "time": 0.247356 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 14.698575973510742, + "time": 0.057386 + } + }, + "281": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 12.645647048950195, + "time": 0.011308 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 34.96013307571411, + "time": 0.248106 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 14.443206787109375, + "time": 0.059948 + } + }, + "282": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 13.95084285736084, + "time": 0.011547 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 33.0524537563324, + "time": 0.246999 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 15.53288221359253, + "time": 0.058802 + } + }, + "283": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 14.53318190574646, + "time": 0.012099 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 33.21742582321167, + "time": 0.252276 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 15.35260796546936, + "time": 0.060666 + } + }, + "284": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 14.275469779968262, + "time": 0.012114 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 33.759286880493164, + "time": 0.253255 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 15.54024076461792, + "time": 0.069668 + } + }, + "285": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 13.821911096572876, + "time": 0.012159 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 36.84333300590515, + "time": 0.255106 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 14.736455917358398, + "time": 0.058031 + } + }, + "286": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 13.905147790908813, + "time": 0.011233 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 36.739805936813354, + "time": 0.257891 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 15.248926877975464, + "time": 0.059365 + } + }, + "287": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 14.467827796936035, + "time": 0.011424 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 36.41704773902893, + "time": 0.258485 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 15.487802743911743, + "time": 0.056904 + } + }, + "288": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 14.719262838363647, + "time": 0.01182 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 34.40790510177612, + "time": 0.250149 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 17.515906810760498, + "time": 0.059727 + } + }, + "289": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 15.412592887878418, + "time": 0.011871 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 34.19995331764221, + "time": 0.248694 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 16.346511125564575, + "time": 0.059282 + } + }, + "290": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 14.580647945404053, + "time": 0.011893 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 34.62252402305603, + "time": 0.247264 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 16.643410205841064, + "time": 0.059007 + } + }, + "291": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 14.956663131713867, + "time": 0.012769 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 39.19132590293884, + "time": 0.267144 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 16.981899976730347, + "time": 0.059653 + } + }, + "292": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 15.497587203979492, + "time": 0.012123 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 39.60783290863037, + "time": 0.266339 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 16.58948588371277, + "time": 0.059328 + } + }, + "293": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 15.194257259368896, + "time": 0.011882 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 38.943033933639526, + "time": 0.265474 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 16.45298981666565, + "time": 0.059135 + } + }, + "294": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 15.75406002998352, + "time": 0.012214 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 35.72841691970825, + "time": 0.25915 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 16.988749980926514, + "time": 0.061719 + } + }, + "295": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 15.454794883728027, + "time": 0.012744 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 35.742210149765015, + "time": 0.259088 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 17.039219856262207, + "time": 0.061631 + } + }, + "296": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 16.18553900718689, + "time": 0.012144 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 36.38292193412781, + "time": 0.257494 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 17.636919021606445, + "time": 0.062521 + } + }, + "297": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 15.751307010650635, + "time": 0.012497 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 40.82007098197937, + "time": 0.271258 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 17.507299184799194, + "time": 0.063172 + } + }, + "298": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 16.661497831344604, + "time": 0.012469 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 40.76864004135132, + "time": 0.27809 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 17.89074397087097, + "time": 0.063387 + } + }, + "299": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 15.982009887695312, + "time": 0.012303 + }, + "repeat' rw [eq_fa_a]": { + "rewrite_command": "repeat' rw [eq_fa_a]", + "status": "PASSED", + "file_time": 41.177403926849365, + "time": 0.275053 + }, + "simp only [eq_fa_a]": { + "rewrite_command": "simp only [eq_fa_a]", + "status": "PASSED", + "file_time": 17.876878261566162, + "time": 0.061731 + } + } +} \ No newline at end of file diff --git a/benchmark/rewrite_with_eq_haa_a/lean_benchmark_results.json b/benchmark/rewrite_with_eq_haa_a/lean_benchmark_results.json new file mode 100644 index 0000000..dc3b597 --- /dev/null +++ b/benchmark/rewrite_with_eq_haa_a/lean_benchmark_results.json @@ -0,0 +1,842 @@ +{ + "0": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.0385069847106934, + "time": 0.001168 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 0.7584860324859619, + "time": 0.001553 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 0.7574279308319092, + "time": 0.001805 + } + }, + "1": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.7143979072570801, + "time": 0.001104 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 0.7686977386474609, + "time": 0.001665 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 0.7386257648468018, + "time": 0.001943 + } + }, + "2": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.7256298065185547, + "time": 0.001128 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 0.7120630741119385, + "time": 0.001567 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 0.7254912853240967, + "time": 0.001751 + } + }, + "3": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.7431070804595947, + "time": 0.001229 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 0.7413489818572998, + "time": 0.001914 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 0.7463517189025879, + "time": 0.002115 + } + }, + "4": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.7283890247344971, + "time": 0.001225 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 0.7204511165618896, + "time": 0.00178 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 0.748953104019165, + "time": 0.002081 + } + }, + "5": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.5763061046600342, + "time": 0.001229 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 0.7332780361175537, + "time": 0.001863 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 0.714972972869873, + "time": 0.00202 + } + }, + "6": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.7184898853302002, + "time": 0.001877 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 0.7464761734008789, + "time": 0.002147 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 0.7292506694793701, + "time": 0.002439 + } + }, + "7": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.7089390754699707, + "time": 0.001775 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 0.7551569938659668, + "time": 0.002352 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 0.7555630207061768, + "time": 0.002648 + } + }, + "8": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.7307698726654053, + "time": 0.001619 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 0.7326159477233887, + "time": 0.002184 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 0.7610471248626709, + "time": 0.002598 + } + }, + "9": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.7390179634094238, + "time": 0.002308 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 0.7413580417633057, + "time": 0.002855 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 1.8294572830200195, + "time": 0.003281 + } + }, + "10": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.7559731006622314, + "time": 0.002307 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 0.7774519920349121, + "time": 0.002859 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 0.8380410671234131, + "time": 0.003309 + } + }, + "11": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.7541689872741699, + "time": 0.002337 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 0.7638771533966064, + "time": 0.002883 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 1.7744300365447998, + "time": 0.003307 + } + }, + "12": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.7960638999938965, + "time": 0.003614 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 0.8253521919250488, + "time": 0.004166 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 0.8317561149597168, + "time": 0.004739 + } + }, + "13": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.8041291236877441, + "time": 0.003818 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 0.804628849029541, + "time": 0.004224 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 0.866710901260376, + "time": 0.004716 + } + }, + "14": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.7782180309295654, + "time": 0.003763 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 0.8100049495697021, + "time": 0.004171 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 0.8528289794921875, + "time": 0.00489 + } + }, + "15": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.9259390830993652, + "time": 0.006414 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 0.8991138935089111, + "time": 0.007137 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 0.9986598491668701, + "time": 0.007828 + } + }, + "16": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 0.9363620281219482, + "time": 0.006451 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 0.9299910068511963, + "time": 0.006908 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 1.0319092273712158, + "time": 0.007985 + } + }, + "17": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.0332129001617432, + "time": 0.006299 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 1.07698392868042, + "time": 0.006825 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 1.0141911506652832, + "time": 0.007719 + } + }, + "18": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.3239848613739014, + "time": 0.012473 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 1.1651020050048828, + "time": 0.013861 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 1.405290126800537, + "time": 0.014158 + } + }, + "19": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.1608850955963135, + "time": 0.01239 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 1.2159109115600586, + "time": 0.013454 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 1.3934299945831299, + "time": 0.013273 + } + }, + "20": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.194554090499878, + "time": 0.012759 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 1.1958961486816406, + "time": 0.012766 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 1.3939049243927002, + "time": 0.013458 + } + }, + "21": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.7664270401000977, + "time": 0.023073 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 1.8618311882019043, + "time": 0.0256 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 2.407528877258301, + "time": 0.024562 + } + }, + "22": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.8165760040283203, + "time": 0.025962 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 1.7687640190124512, + "time": 0.025799 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 2.188526153564453, + "time": 0.026328 + } + }, + "23": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1.75050687789917, + "time": 0.022969 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 1.8420212268829346, + "time": 0.025218 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 2.1096761226654053, + "time": 0.025876 + } + }, + "24": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 3.376410722732544, + "time": 0.04654 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 3.439167022705078, + "time": 0.047656 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 3.7357518672943115, + "time": 0.048927 + } + }, + "25": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 3.367630958557129, + "time": 0.051381 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 3.4566900730133057, + "time": 0.048827 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 4.02093505859375, + "time": 0.054972 + } + }, + "26": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 3.5620369911193848, + "time": 0.050811 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 3.549133062362671, + "time": 0.048517 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 4.022313833236694, + "time": 0.047532 + } + }, + "27": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 10.367033004760742, + "time": 0.099608 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 10.27844500541687, + "time": 0.108983 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 10.444552183151245, + "time": 0.099648 + } + }, + "28": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 9.785251140594482, + "time": 0.096574 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 9.836464881896973, + "time": 0.097926 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 10.401023864746094, + "time": 0.102206 + } + }, + "29": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 9.752179861068726, + "time": 0.097029 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 9.854215145111084, + "time": 0.096444 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 10.314520835876465, + "time": 0.097767 + } + }, + "30": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 34.35830807685852, + "time": 0.202651 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 35.34646821022034, + "time": 0.199186 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 2367.9422619342804, + "time": 0.210974 + } + }, + "31": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1052.5403130054474, + "time": 0.192997 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 33.483150005340576, + "time": 0.193517 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 33.77033710479736, + "time": 0.190337 + } + }, + "32": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 36.09439206123352, + "time": 0.192278 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 40.45110106468201, + "time": 0.199863 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 34.35187888145447, + "time": 0.199255 + } + }, + "33": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 1720.322633266449, + "time": 0.436156 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 366.242436170578, + "time": 1.163081 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 191.22963118553162, + "time": 0.450456 + } + }, + "34": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 137.99413990974426, + "time": 0.436943 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 163.3456859588623, + "time": 0.520221 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 227.10544991493225, + "time": 0.570814 + } + }, + "35": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 141.92512488365173, + "time": 0.426567 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 141.1051731109619, + "time": 0.443365 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 135.63515901565552, + "time": 0.404864 + } + }, + "36": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 533.4364929199219, + "time": 0.827376 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 517.2699098587036, + "time": 0.797139 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 517.1497831344604, + "time": 0.807243 + } + }, + "37": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 520.8516249656677, + "time": 0.801351 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 520.8111808300018, + "time": 0.814073 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 518.6797549724579, + "time": 0.82065 + } + }, + "38": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 534.228119134903, + "time": 0.836113 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 624.4381928443909, + "time": 0.861979 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 618.7837431430817, + "time": 0.87821 + } + }, + "39": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 2662.6949739456177, + "time": 1.80822 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 2368.884955883026, + "time": 1.802064 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 2361.2743332386017, + "time": 1.788921 + } + }, + "40": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 2343.573695898056, + "time": 1.761633 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 2361.007213115692, + "time": 1.749151 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 2352.0717046260834, + "time": 1.771644 + } + }, + "41": { + "sorry": { + "rewrite_command": "sorry", + "status": "PASSED", + "file_time": 2363.7235610485077, + "time": 1.770757 + }, + "repeat' rw [eq_haa_a]": { + "rewrite_command": "repeat' rw [eq_haa_a]", + "status": "PASSED", + "file_time": 2368.5442559719086, + "time": 1.767944 + }, + "simp only [eq_haa_a]": { + "rewrite_command": "simp only [eq_haa_a]", + "status": "PASSED", + "file_time": 2371.654742002487, + "time": 1.780969 + } + } +} \ No newline at end of file