### OCaml Setup with opam

Source: https://github.com/ccz181078/coq-bb5/blob/main/CoqBB5/BB5/BB5_Extraction/README.md

This snippet demonstrates how to set up an OCaml environment using opam, specifically switching to version 5.1.1 and installing necessary packages like ocamlbuild, ocamlfind, and zarith. Ensure opam is installed before running these commands.

```shell
opam switch 5.1.1
eval $(opam env)
opam install ocamlbuild ocamlfind zarith
```

--------------------------------

### Install Coq v8.20.1 using Opam

Source: https://github.com/ccz181078/coq-bb5/blob/main/CoqBB5/BB2/README.md

This snippet shows the commands to install a specific version of Coq (8.20.1) and its native compiler using the Opam package manager. It assumes opam is already installed and sets up the environment for Coq.

```sh
opam switch create 4.14.2 # if already existent do: opam switch 4.14.2
eval $(opam env)
opam install coq-native
opam pin add coq 8.20.1
```

--------------------------------

### Running the Legacy Monolithic Coq Proof

Source: https://github.com/ccz181078/coq-bb5/blob/main/CoqBB5/BB2x4/README.md

Command to execute the original, monolithic Coq proof file. This requires Coq v8.20.1 to be installed and the CoqBB2x4 query to be set up.

```shell
coqc -Q . CoqBB2x4 _BB2x4_Legacy_Monolith.v
```

--------------------------------

### Install OCaml Packages for BB2x4 Extraction

Source: https://github.com/ccz181078/coq-bb5/blob/main/CoqBB5/BB2x4/BB2x4_Extraction/README.md

Installs required OCaml packages using OPAM, including ocamlbuild, ocamlfind, and zarith. These packages are dependencies for compiling and running the OCaml extraction scripts.

```bash
opam install ocamlbuild
opam install ocamlfind
opam install zarith
```

--------------------------------

### Compile Legacy Monolithic Coq Proof for BB(4)

Source: https://github.com/ccz181078/coq-bb5/blob/main/CoqBB5/BB4/README.md

Command to compile the original monolithic Coq proof for BB(4) = 107. Assumes Coq v8.20.1 is installed and the current directory is in the Coq path.

```shell
coqc -Q . CoqBB4 _BB4_Legacy_Monolith.v
```

--------------------------------

### Example CSV Output Format for Turing Machine Enumeration

Source: https://github.com/ccz181078/coq-bb5/blob/main/CoqBB5/BB4/README.md

An example of the CSV file generated by the BB4_Extraction.sh script. It includes the machine's configuration, its halting status (halt or nonhalt), and the ID of the decider that classified it. The machine configuration uses a specific format with underscores separating components.

```csv
machine,status,decider
------_------_------_------,halt,LOOP1_params_107
0RA---_------_------_------,nonhalt,LOOP1_params_107
1RA---_------_------_------,nonhalt,LOOP1_params_107
0RB---_------_------_------,halt,LOOP1_params_107
0RB---_0LA---_------_------,nonhalt,LOOP1_params_107
0RB---_1LA---_------_------,halt,LOOP1_params_107
0RB---_1LA0LA_------_------,nonhalt,LOOP1_params_107
0RB---_1LA1LA_------_------,nonhalt,LOOP1_params_107
0RB---_1LA0RA_------_------,nonhalt,LOOP1_params_107
```

--------------------------------

### BB3 Verified Enumeration CSV Format

Source: https://github.com/ccz181078/coq-bb5/blob/main/CoqBB5/BB3/README.md

This is an example of the CSV file produced by the BB3_Extraction.sh script. It lists machines with their status (halt or nonhalt) and the ID of the decider that determined their status. The format follows the bbchallenge standard.

```csv
machine,status,decider
------_------_------,halt,LOOP1_params_21
0RA---_------_------,nonhalt,LOOP1_params_21
1RA---_------_------,nonhalt,LOOP1_params_21
0RB---_------_------,halt,LOOP1_params_21
0RB---_0LA---_------,nonhalt,LOOP1_params_21
0RB---_1LA---_------,halt,LOOP1_params_21
0RB---_1LA0LA_------,nonhalt,LOOP1_params_21
0RB---_1LA1LA_------,nonhalt,LOOP1_params_21
0RB---_1LA0RA_------,nonhalt,LOOP1_params_21
```

--------------------------------

### Compile Coq Proof for BB(4)

Source: https://github.com/ccz181078/coq-bb5/blob/main/CoqBB5/BB4/README.md

Commands to set up the Coq environment and compile the BB(4) proof. Requires opam and Coq v8.20.1.

```shell
opam switch create 4.14.2 # if already existent do: opam switch 4.14.2
eval $(opam env)
opam install coq-native
opam pin add coq 8.20.1

make
```

--------------------------------

### Define Base Case and State Reachability in Coq

Source: https://github.com/ccz181078/coq-bb5/blob/main/CoqBB5/BB5/BB5_Skelet17.md

Shows a set of Coq lemmas and definitions related to base cases, state transitions (`toConfig`), and reachability in a computational model. It demonstrates how a specific base state (`Base 1`) can be reached from an initial configuration (`c0`) and establishes non-halting properties.

```Coq
Lemma Sk_closed k b c:
  k<>0 ->
  Base k b ->
  toConfig b c ->
  exists b' c',
  Base (S k) b' /\
  toConfig b' c' /\
  c -->* c'.

Lemma base :
  c0 -->*
  lower ([0; 4; 2; 0]).

Definition Base_1 := (1,[4;2;0]).

Lemma Base_1_spec:
  Base 1 Base_1.

Lemma Base_1_toConfig:
  toConfig Base_1 (lower [0;4;2;0]).

Lemma Base_ne k b b' c c':
  Base k b ->
  Base (S k) b' ->
  toConfig b c ->
  toConfig b' c' ->
  c<>c'.

Theorem nonhalt:
  ~halts tm c0.
```

```ocaml

```

--------------------------------

### Compile the Coq Proof

Source: https://github.com/ccz181078/coq-bb5/blob/main/CoqBB5/BB2/README.md

This is a standard make command to compile the Coq proof. It assumes a Makefile is present in the directory, which orchestrates the compilation process of the Coq source files.

```sh
make
```

--------------------------------

### Compile BusyCoq and CoqBB5 Proofs

Source: https://github.com/ccz181078/coq-bb5/blob/main/CoqBB5/BB5/README.md

Commands to compile the BusyCoq project and then the CoqBB5 proof. It's recommended to compile BusyCoq first to obtain proofs for sporadic machines. The '-j' flag specifies the number of cores to use for compilation.

```sh
cd ../../BusyCoq && make -j 13
cd ../CoqBB5/BB5 && make -j 13
```

--------------------------------

### Prove Lemmas Related to ZIHIO in Coq

Source: https://github.com/ccz181078/coq-bb5/blob/main/CoqBB5/BB5/BB5_Skelet17.md

Presents several lemmas associated with the ZIHIO relation. These lemmas demonstrate how the ZIHIO relation implies the existence of other states and relations, particularly `embanked` and `Add2`, and how to derive properties of these new states.

```Coq
Lemma E''_Overflow s1:
  (exists s0, embanked_batch 1 s0 s1 1 (2^(k*2)*2-1)) ->
  to_l s1 = k*2+1 ->
  ai' 0 s1 = 2^(k*2)*2-3 ->
  ai' 1 s1 = 2^(k*2)*3 ->
  (forall i, 2<=i -> i<=k*2 -> ai' i s1 = 2^(k*2+1-i)*3-(1-(i mod 2))*2) ->
  ai' (k*2+1) s1 = 2 ->
  exists s6, ZIHIO s1 s6.

Lemma ZIHIO_emb e ne:
  ZIHIO e ne ->
  exists ne',
  embanked ne ne' (2^(k*2+3)-1) (2^(k*2+2)-1) (2^(k*2+3)-4) (2^(k*2+2)-2).

Lemma ZIHIO_emb_Add2 e ne ne':
  ZIHIO e ne ->
  embanked ne ne' (2^(k*2+3)-1) (2^(k*2+2)-1) (2^(k*2+3)-4) (2^(k*2+2)-2) ->
  Add2 (k*2+1) ne ne'.

Lemma ZIHIO_embanked_batch e ne ne':
  ZIHIO e ne ->
  embanked ne ne' (2^(k*2+3)-1) (2^(k*2+2)-1) (2^(k*2+3)-4) (2^(k*2+2)-2) ->
  exists n'ne,
  embanked_batch (k*2+1) ne n'ne (2^(k*2+2)-1) (2^(k*2+2)-2) /\
  to_l n'ne = k*2+3 /\
  ai' 0 n'ne = 1 /\
  ai' 1 n'ne = 2^(k*2+2)-2 /\
  (forall i, 2<=i -> ai' i n'ne = if i<? k*2+3 then 2^(k*2+3-i) else 0).
```

--------------------------------

### Coq: Embanked 4-Batch Transition Lemma

Source: https://github.com/ccz181078/coq-bb5/blob/main/CoqBB5/BB5/BB5_Skelet17.md

Proves a lemma in Coq concerning a sequence of four 'embanked_batch' operations. It establishes conditions on 'm' and 'ctzS' values and demonstrates how the state 'e1' transitions through 'e2', 'e3', 'e4', and 'e5', maintaining invariants on 'to_l', 'ai'', and relating the final state to the initial state 'e1' through a sum involving 'm'.

```ocaml
Lemma embanked_4batch m i0 e0 e1:
  m+3 < 2^(k*2) ->
  ctzS m mod 2 = 0 ->
  ctzS (m+1) mod 2 = 1 ->

  embanked_batch i0 e0 e1 (2^(k*2)-1-m) (2^(k*2)+m) ->
  i0 mod 2 = 1 ->
  to_l e1 = k*2+1 ->
  ai' 0 e1 = 1+m*2 ->
  ai' 1 e1 = 2^(k*2)+2+m*2 ->

  exists e2 i2,
  embanked_batch i2 e1 e2 (2^(k*2)-1-(m)) (2^(k*2)+(m+1)) /\ 

  exists e3 i3,
  embanked_batch i3 e2 e3 (2^(k*2)-1-(m)) (2^(k*2)+(m+2)) /\ 

  exists e4 i4,
  embanked_batch i4 e3 e4 (2^(k*2)-1-(m+1)) (2^(k*2)+(m+2)) /\ 

  exists e5 i5,
  embanked_batch i5 e4 e5 (2^(k*2)-1-(m+2)) (2^(k*2)+(m+2)) /

  i5 mod 2 = 1 /\ 
  to_l e5 = k*2+1 /\ 
  ai' 0 e5 = 1+(m+2)*2 /\ 
  ai' 1 e5 = 2^(k*2)+2+(m+2)*2 /\ 
  (forall i, ai i e5 + 2*(m/2^i) = ai i e1 + 2*((m+2)/2^i))
.

```

--------------------------------

### Prove Lemmas Related to embanked_batches in Coq

Source: https://github.com/ccz181078/coq-bb5/blob/main/CoqBB5/BB5/BB5_Skelet17.md

Contains several lemmas that demonstrate properties related to `embanked_batches` given certain conditions.  These lemmas prove the existence of states satisfying properties related to `N'steps`, `embanked_batch`, and `Add2s` relations and provide formulas for ai values.

```Coq
Lemma embanked_batches_0 m0:
  m0 < 2^(k*2)-1 ->
  forall m,
  m<=m0 ->
  ctzS_chain m ->
  exists e ne,
  N'steps e (2^(k*2)-1) (2^(k*2)) ne (2^(k*2)-1-m) (2^(k*2)+m) /\
  embanked_batch (k*2+1) Sk e (2^(k*2)-1) (2^(k*2)) /\
  Add2s (k*2+1) Sk e /\
  (exists e' i', embanked_batch i' e' ne (2^(k*2)-1-m) (2^(k*2)+m) /\ i' mod 2 = 1) /\
  to_l ne = k*2+1 /\
  ai' 0 ne = 1+m*2 /\
  ai' 1 ne = 2^(k*2)+2+m*2 /\
  (forall i, ai i ne = ai i e + 2*(m/2^i)).

(* m=2^(k*2)-2 is Corollary 4.2 *)
Lemma embanked_batches m:
  m < 2^(k*2)-1 ->
  ctzS_chain m ->
  exists e ne,
  N'steps e (2^(k*2)-1) (2^(k*2)) ne (2^(k*2)-1-m) (2^(k*2)+m) /\
  embanked_batch (k*2+1) Sk e (2^(k*2)-1) (2^(k*2)) /\
  Add2s (k*2+1) Sk e /\
  (exists e' i', embanked_batch i' e' ne (2^(k*2)-1-m) (2^(k*2)+m) /\ i' mod 2 = 1) /\
  to_l ne = k*2+1 /\
  ai' 0 ne = 1+m*2 /\
  ai' 1 ne = 2^(k*2)+2+m*2 /\
  (forall i, ai i ne = ai i e + 2*(m/2^i)). (* Proposition 4.3 *)
  
(* Corollary 4.2 *)
Lemma Sk_to_E':
  exists e ne,
  N'steps e (2^(k*2)-1) (2^(k*2)) ne 1 (2^(k*2)*2-2) /\
  embanked_batch (k*2+1) Sk e (2^(k*2)-1) (2^(k*2)) /\
  Add2s (k*2+1) Sk e /\
  (exists e' i', embanked_batch i' e' ne 1 (2^(k*2)*2-2) /\ i' mod 2 = 1) /\
  to_l ne = k*2+1 /\
  ai' 0 ne = 2^(k*2)*2-3 /\
  ai' 1 ne = 2^(k*2)*3-2 /\
  (forall i, ai i ne = ai i e + 2*((2^(k*2)-2)/2^i)).

Lemma Sk_to_E'':
  exists e ne,
  N'steps e (2^(k*2)-1) (2^(k*2)) ne 1 (2^(k*2)*2-2) /\
  embanked_batch (k*2+1) Sk e (2^(k*2)-1) (2^(k*2)) /\
  Add2s (k*2+1) Sk e /\
  (forall i, ai i ne = ai i e + 2*((2^(k*2)-2)/2^i)) /\
  exists n'ne,
  embanked_batch 1 ne n'ne 1 (2^(k*2)*2-1) /\
  to_l n'ne = k*2+1 /\
  ai' 0 n'ne = 2^(k*2)*2-3 /\
  ai' 1 n'ne = 2^(k*2)*3 /\
  (forall i, 2<=i -> i<=k*2 -> ai' i n'ne = 2^(k*2+1-i)*3-(1-(i mod 2))*2) /\
  ai' (k*2+1) n'ne = 2
.
```

--------------------------------

### Coq: Embanked Batch Preconditions and Transitions

Source: https://github.com/ccz181078/coq-bb5/blob/main/CoqBB5/BB5/BB5_Skelet17.md

Formalizes the preconditions for the 'embanked_batch' operation in Coq, detailing how the state 'ne' is derived from a previous state 'e' based on the parity of 'i'. It shows how the next state 'n'ne' is reached, updating 'h_1' or 'h_2' based on 'ctzS' calculations, and ensures 'to_l' remains consistent.

```ocaml
Lemma embanked_batch_precond'' {i e ne h_1 h_2}:
  embanked_batch i e ne h_1 h_2 ->
  to_l ne = k*2+1 ->
  ai' 0 ne < 2^(k*2)*2 - 1 ->
  ai' 1 ne < 2^(k*2)*3 ->
  exists n'ne,
  match i mod 2 with
  | 0 => embanked_batch (ctzS (h_1-1)) ne n'ne (h_1-1) h_2
  | 1 => embanked_batch (S (ctzS h_2)) ne n'ne h_1 (h_2+1)
  | _ => False
  end.

```

--------------------------------

### Prove Last Step Lemma in Coq

Source: https://github.com/ccz181078/coq-bb5/blob/main/CoqBB5/BB5/BB5_Skelet17.md

This lemma, `last_step`, demonstrates the existence of states `b`, `h_1`, and `h_2` that satisfy the `embanked_batch` and `Base` relations, given certain properties of state `ne`. It essentially shows how to reach a base state from a given configuration in the computational model.

```Coq
Lemma last_step k e ne:
  embanked_batch (k*2+1) e ne (2^(k*2+2)-1) (2^(k*2+2)-2) ->
  to_l ne = k*2+3 ->
  ai' 0 ne = 1 ->
  ai' 1 ne = 2^(k*2+2)-2 ->
  (forall i, 2<=i -> ai' i ne = if i<? k*2+3 then 2^(k*2+3-i) else 0) ->
  exists b h_1 h_2,
  embanked_batch 1 ne b h_1 h_2 /\
  Base (k+1) b.
```

--------------------------------

### Coq: Embanked 8-Batch Transition Lemma

Source: https://github.com/ccz181078/coq-bb5/blob/main/CoqBB5/BB5/BB5_Skelet17.md

Proves a lemma in Coq for a sequence of eight 'embanked_batch' operations. Similar to the 4-batch lemma, it sets conditions on 'm' and 'ctzS' and demonstrates state transitions from 'e1' to 'e9', ensuring invariants and relating the final state to the initial state 'e1' through a sum involving 'm'.

```ocaml
Lemma embanked_8batch m i0 e0 e1:
  m+5 < 2^(k*2) ->
  ctzS m mod 2 = 0 ->
  ctzS (m+1) mod 2 = 0 ->
  ctzS (m+2) mod 2 = 0 ->
  ctzS (m+3) mod 2 = 1 ->

  embanked_batch i0 e0 e1 (2^(k*2)-1-m) (2^(k*2)+m) ->
  i0 mod 2 = 1 ->
  to_l e1 = k*2+1 ->
  ai' 0 e1 = 1+m*2 ->
  ai' 1 e1 = 2^(k*2)+2+m*2 ->

  exists e2 i2,
  embanked_batch i2 e1 e2 (2^(k*2)-1-(m)) (2^(k*2)+(m+1)) /\ 

  exists e3 i3,
  embanked_batch i3 e2 e3 (2^(k*2)-1-(m)) (2^(k*2)+(m+2)) /\ 

  exists e4 i4,
  embanked_batch i4 e3 e4 (2^(k*2)-1-(m)) (2^(k*2)+(m+3)) /\ 

  exists e5 i5,
  embanked_batch i5 e4 e5 (2^(k*2)-1-(m)) (2^(k*2)+(m+4)) /\ 

  exists e6 i6,
  embanked_batch i6 e5 e6 (2^(k*2)-1-(m+1)) (2^(k*2)+(m+4)) /\ 

  exists e7 i7,
  embanked_batch i7 e6 e7 (2^(k*2)-1-(m+2)) (2^(k*2)+(m+4)) /\ 

  exists e8 i8,
  embanked_batch i8 e7 e8 (2^(k*2)-1-(m+3)) (2^(k*2)+(m+4)) /\ 

  exists e9 i9,
  embanked_batch i9 e8 e9 (2^(k*2)-1-(m+4)) (2^(k*2)+(m+4)) /

  i9 mod 2 = 1 /\ 
  to_l e9 = k*2+1 /\ 
  ai' 0 e9 = 1+(m+4)*2 /\ 
  ai' 1 e9 = 2^(k*2)+2+(m+4)*2 /
  (forall i, ai i e9 + 2*(m/2^i) = ai i e1 + 2*((m+4)/2^i))
.

```

--------------------------------

### Coq Lemma: embanked_batch_postcond

Source: https://github.com/ccz181078/coq-bb5/blob/main/CoqBB5/BB5/BB5_Skelet17.md

This lemma describes the postconditions of `embanked_batch`. It asserts that if `embanked_batch i e ne h_1 h_2` holds, then certain properties about `ne` must be true, including `WF1 ne`, `to_s ne = false`, `to_n ne = 0`, `to_l ne >= 3`, and `Odd (fst ne)`.

```coq
Lemma embanked_batch_postcond {i e ne h_1 h_2}:
  embanked_batch i e ne h_1 h_2 ->
  WF1 ne /\ 
  to_s ne = false /\ 
  to_n ne = 0 /
  to_l ne >=3 /
  Odd (fst ne).


```

--------------------------------

### Lemma for Weakly Embanked Preconditions in Coq

Source: https://github.com/ccz181078/coq-bb5/blob/main/CoqBB5/BB5/BB5_Skelet17.md

Proves the 'weakly_embanked_precond' lemma, which establishes that if certain pre-conditions on a state 's1' are met (like 'WF1', 'to_s' being false, 'to_n' being zero, etc.), then there exists a valid 'weakly_embanked' state transition.

```ocaml
(*
  Proposition 3.4
  and also prove some properties of s_1,s_2,h_1,h_2 for Lemma 3.5
*)
Lemma weakly_embanked_precond s1:
  WF1 s1 ->
  to_s s1 = false ->
  to_n s1 = O ->
  to_l s1 >= 3 ->
  Odd (fst s1) ->
  fst s1 < 2 ^ to_l s1 - 1 ->
  ai O s1 < 3 * (2 ^ (to_l s1 - 1)) ->
  exists s2 s_1 s_2 h_1 h_2,
  weakly_embanked s1 s2 s_1 h_1 s_2 h_2.

```

--------------------------------

### Execute BB2x4 Extraction Script

Source: https://github.com/ccz181078/coq-bb5/blob/main/CoqBB5/BB2x4/BB2x4_Extraction/README.md

Runs the BB2x4_Extraction.sh script, which compiles OCaml files, generates a CSV file with headers, executes the compiled program for Tree Normal Form enumeration, cleans the CSV, and verifies its hash. Stack size adjustments may be necessary.

```bash
./BB2x4_Extraction.sh
```

--------------------------------

### Coq Lemma: embanked_batch_precond

Source: https://github.com/ccz181078/coq-bb5/blob/main/CoqBB5/BB5/BB5_Skelet17.md

This lemma, `embanked_batch_precond`, details preconditions for `embanked_batch`. It shows that if `embanked_batch i e ne h_1 h_2` and `weakly_embanked ne ne' s_1' h_1' s_2' h_2'` hold, then a new `embanked_batch` can be formed with a modified `i` based on the parity of the original `i`.

```coq
Lemma embanked_batch_precond {i e ne h_1 h_2 s_1' h_1' s_2' h_2'}:
  embanked_batch i e ne h_1 h_2 ->
  weakly_embanked ne ne' s_1' h_1' s_2' h_2' ->
  exists n'ne, embanked_batch (match i mod 2 with
  | O => (ctzS (h_1-1))
  | S O => (S (ctzS h_2))
  | S (S _) => 0
  end) ne n'ne h_1' h_2'.


```

--------------------------------

### Coq: Pre-conditions for Increment, Halve, Zero, Overflow

Source: https://github.com/ccz181078/coq-bb5/blob/main/CoqBB5/BB5/BB5_Skelet17.md

Formalizes the pre-conditions for single increment, halve, zero, and overflow operations on integers represented in Coq. These lemmas are crucial for proving the correctness of state transitions in a larger system.

```ocaml
Lemma Increment_inc_precond1 {s1}:
  WF1 s1 ->
  to_s s1 = true ->
  to_n s1 < 2^(to_l s1) - 1 ->
  fst s1 > O ->
  exists s2, Increment s1 s2 /\ WF1 s2.

Lemma Increment_inc_precond22 {s1}:
  WF2 s1 ->
  to_s s1 = true ->
  to_n s1 < 2^(to_l s1 - 2) - 1 ->
  fst s1 > O ->
  exists s2, Increment s1 s2 /\ WF2 s2.

Lemma Increment_inc_precond21 {s1}:
  WF2 s1 ->
  to_s s1 = true ->
  to_n s1 = 2^(to_l s1 - 2) - 1 ->
  fst s1 > O ->
  exists s2, Increment s1 s2 /\ WF1 s2.

Lemma Increment_dec_precond1 {s1}:
  WF1 s1 ->
  to_s s1 = false ->
  to_n s1 > O ->
  fst s1 > O ->
  exists s2, Increment s1 s2 /\ WF1 s2.

Lemma Increment_dec_precond2 {s1}:
  WF2 s1 ->
  to_s s1 = false ->
  to_n s1 > S O ->
  fst s1 > O ->
  exists s2, Increment s1 s2 /\ WF2 s2.

Lemma Halve_precond1 {s1}:
  WF1 s1 ->
  fst s1 = O ->
  to_l s1 >= 2 ->
  exists s2, Halve s1 s2 /\ WF1 s2.

Lemma Halve_precond2 {s1}:
  WF2 s1 ->
  fst s1 = O ->
  (to_n s1 <> S O) ->
  exists s2, Halve s1 s2 /\ WF2 s2.

Lemma Zero_precond {s1}:
  WF1 s1 ->
  to_s s1 = false ->
  to_n s1 = O ->
  exists s2, Zero s1 s2 /\ WF2 s2.

Lemma Overflow_precond {s1}:
  WF1 s1 ->
  to_s s1 = true ->
  to_n s1 = 2^(to_l s1) - 1 ->
  fst s1 = 1 ->
  exists s2, Overflow s1 s2 /\ WF1 s2.
```

--------------------------------

### Lemma relating Embanked, Weakly Embanked, and Add2 in Coq

Source: https://github.com/ccz181078/coq-bb5/blob/main/CoqBB5/BB5/BB5_Skelet17.md

Proves the 'emb_wemb_Add2_emb' lemma. This lemma is crucial as it shows that if an 'embanked' state and a 'weakly_embanked' state are related by 'Add2 i', then a new 'embanked' state can be formed for the next step, with the 'i' parameter for 'Add2' being updated based on the 'ctzS' of intermediate values.

```ocaml
(* Proposition 3.6 *)
Lemma emb_wemb_Add2_emb {e ne ne' i s_1 h_1 s_2 h_2 s_1' h_1' s_2' h_2'}:
  embanked e ne s_1 h_1 s_2 h_2 ->
  weakly_embanked ne ne' s_1' h_1' s_2' h_2' ->
  Add2 i e ne ->
  exists nne, embanked ne nne s_1' h_1' s_2' h_2' /
  match i with
  | O => Add2 (ctzS (h_1-1)) ne nne
  | S O => Add2 (S (ctzS h_2)) ne nne
  | S (S i0) => Add2 i0 ne nne
  end.

```

--------------------------------

### Coq Lemma: embanked_batch__wemb

Source: https://github.com/ccz181078/coq-bb5/blob/main/CoqBB5/BB5/BB5_Skelet17.md

Proves a lemma that connects `embanked_batch` with `weakly_embanked`. It states that if `embanked_batch i e ne h_1 h_2` holds and the `ai'` values of `ne` are sufficiently small, then there exist parameters `ne0`, `s_1'`, `s_2'`, `h_1'`, `h_2'` such that `ne` is `weakly_embanked` to `ne0`.

```coq
Lemma embanked_batch__wemb {i e ne h_1 h_2}:
  embanked_batch i e ne h_1 h_2 ->
  ai' 0 ne < 2^(to_l ne) - 1 ->
  ai' 1 ne < 2^(to_l ne - 1)*3 ->
  exists ne0 s_1' s_2' h_1' h_2',
  weakly_embanked ne ne0 s_1' h_1' s_2' h_2'.


```

--------------------------------

### OCaml: State Transition Lemmas for ai after Increments, Halve, Zero, Overflow

Source: https://github.com/ccz181078/coq-bb5/blob/main/CoqBB5/BB5/BB5_Skelet17.md

This snippet provides Coq lemmas detailing the changes to the 'ai' (individual digit values) after operations like Increments, Halve, Zero, and Overflow. It also includes lemmas for changes in 'n' and 's' after a series of Increments.

```ocaml
Definition ai(i:nat)(s:nat*(list nat)) :=
  nth i (snd s) O.

Lemma Increments_a {n s1 s2}:
  Increments n s1 s2 ->
  if to_s s1 then
  forall i,
    ai i s2 + divpow2r (to_n s1) i = 
    ai i s1 + divpow2r (to_n s2) i
  else
  forall i,
    ai i s1 + divpow2r (to_n s1) i = 
    ai i s2 + divpow2r (to_n s2) i.

Lemma Increments_a0 {n s1 s2}:
  Increments n s1 s2 ->
  if to_s s1 then
    (fst s1) + (to_n s1) =
    (fst s2) + (to_n s2)
  else
    (fst s2) + (to_n s1) =
    (fst s1) + (to_n s2).

Lemma Zero_a0 {s1 s2}:
  Zero s1 s2 ->
  fst s1 = S (fst s2).

Lemma Zero_a1 {s1 s2}:
  Zero s1 s2 ->
  to_l s1 >= 3 ->
  ai O s1 = ai O s2.

Lemma Zero_a {s1 s2}:
  Zero s1 s2 ->
  forall i, ai i s1 + (if Nat.eqb i (to_l s1 - 1) then 1 else 0)%nat = ai i s2.

Lemma Overflow_a0 {s1 s2}:
  Overflow s1 s2 ->
  fst s1 = fst s2.

Lemma Overflow_a {s1 s2}:
  Overflow s1 s2 ->
  forall i, ai i s1 + (if Nat.eqb i (to_l s1 - 1) then 1 else 0)%nat = ai i s2.

Lemma Halve_a0 {s1 s2}:
  Halve s1 s2 ->
  fst s2 = S (ai O s1).

Lemma Halve_a {s1 s2}:
  Halve s1 s2 ->
  forall i, ai i s2 = ai (S i) s1.


(* The changes of `n,s,l` after `Increments`: *)

Lemma Increments_sgn {n s1 s2}:
  Increments n s1 s2 ->
  to_s s1 = to_s s2.

Lemma Increments_n {n s1 s2}:
  Increments n s1 s2 ->
  if to_s s1 then
    to_n s1 + n = to_n s2
  else
    to_n s1 = to_n s2 + n.

Lemma Increments_len {n s1 s2}:
  Increments n s1 s2 ->
  to_l s1 = to_l s2.
```

--------------------------------

### Execute BB3 Extraction Script

Source: https://github.com/ccz181078/coq-bb5/blob/main/CoqBB5/BB3/README.md

This shell script compiles and runs the OCaml extraction process for the Coq BB3 proof. It generates a CSV file containing enumerated machines, their halting status, and decider IDs. The script is located in the BB3_Extraction directory.

```sh
cd BB3_Extraction
./BB3_Extraction.sh
```

--------------------------------

### OCaml Coq Lemmas for Translation Between Tape Representations

Source: https://github.com/ccz181078/coq-bb5/blob/main/CoqBB5/BB5/BB5_Skelet17.md

This OCaml snippet contains Coq lemmas that establish the translation between the previously defined inductive operations (`Increment`, `Zero`, `Overflow`, `TryHalve`) and the `toConfig` representation. These lemmas are essential for connecting the abstract tape operations to their concrete tape configurations.

```ocaml
Lemma Increment_toConfig s1 s2 s3 c1 c3:
  Increment s1 s2 ->
  TryHalve s2 s3 ->
  toConfig s1 c1 ->
  toConfig s3 c3 ->
  c1 -->* c3.

Lemma Zero_toConfig s1 s2 s3 c1 c3:
  Zero s1 s2 ->
  TryHalve s2 s3 ->
  toConfig s1 c1 ->
  toConfig s3 c3 ->
  c1 -->* c3.

Lemma Overflow_toConfig s1 s2 s3 s4 c1 c4:
  Overflow s1 s2 ->
  Zero s2 s3 ->
  TryHalve s3 s4 ->
  toConfig s1 c1 ->
  toConfig s4 c4 ->
  c1 -->* c4.

```

--------------------------------

### Coq Lemma: embanked_batch_precond'

Source: https://github.com/ccz181078/coq-bb5/blob/main/CoqBB5/BB5/BB5_Skelet17.md

This lemma, `embanked_batch_precond'`, refines the preconditions for `embanked_batch`. It shows that if `embanked_batch i e ne h_1 h_2` holds and the `ai'` values are small, then a new `embanked_batch` can be formed with `ne` and `n'ne`, where the new `i` value depends on the parity of the original `i`.

```coq
Lemma embanked_batch_precond'{i e ne h_1 h_2}:
  embanked_batch i e ne h_1 h_2 ->
  ai' 0 ne < 2^(to_l ne) - 1 ->
  ai' 1 ne < 2^(to_l ne - 1)*3 ->
  exists n'ne,
  match i mod 2 with
  | O => embanked_batch (ctzS (h_1-1)) ne n'ne (h_1-1) h_2
  | S O => embanked_batch (S (ctzS (h_2))) ne n'ne h_1 (h_2+1)
  | _ => False
  end.


```

--------------------------------

### Coq Lemma: embanked__embanked_batch

Source: https://github.com/ccz181078/coq-bb5/blob/main/CoqBB5/BB5/BB5_Skelet17.md

Proves a lemma that connects `embanked` with `embanked_batch`. It shows that if an `embanked` relation holds and `Add2 i` is true for `e` and `ne`, then there exists an `n'e` such that `embanked_batch i` holds for `e` and `n'e`.

```coq
Lemma embanked__embanked_batch {i}:
  forall {e ne s_1' h_1' s_2' h_2'},
  embanked e ne s_1' h_1' s_2' h_2' ->
  Add2 i e ne ->
  exists n'e, embanked_batch i e n'e h_1' h_2'.


```

--------------------------------

### Extracting Verified Machine Enumeration Results

Source: https://github.com/ccz181078/coq-bb5/blob/main/CoqBB5/BB2x3/README.md

This script compiles and runs the OCaml extraction from the Coq proof to generate a CSV file containing all enumerated machines, their halting status, and decider ID. It relies on OCaml extraction as specified in BB2x3_Extraction.v. The output is BB2x3_verified_enumeration.csv.

```sh
cd BB2x3_Extraction
./BB2x3_Extraction.sh
```

--------------------------------

### OCaml Coq Inductive Definition for toConfig

Source: https://github.com/ccz181078/coq-bb5/blob/main/CoqBB5/BB5/BB5_Skelet17.md

This OCaml code defines the Coq inductive type `toConfig`, which serves as a translation between two different representations of tape configurations. It maps a pair of `nat` and `list nat` to a `Q*tape` type.

```ocaml
Inductive toConfig: (nat*(list nat))->(Q*tape)->Prop :=
| toConfig_intro x xs:
  toConfig (S x,xs) (lower (x::xs))
.

```

--------------------------------

### Coq: Hardcoded RepWL Decider Parameters

Source: https://github.com/ccz181078/coq-bb5/blob/main/CoqBB5/BB5/README.md

Coq file providing hardcoded parameters for the RepWL decider. It lists explicit parameters for 6,577 machines decided by RepWL, improving efficiency.

```Coq
(* BB5_Deciders_Hardcoded_Parameters/Decider_RepWL_Hardcoded_Parameters.v
   Hardcoded parameters for the RepWL decider *)

(* ... definitions for hardcoded RepWL parameters ... *)

```

--------------------------------

### Coq Lemma: embanked_batch_last

Source: https://github.com/ccz181078/coq-bb5/blob/main/CoqBB5/BB5/BB5_Skelet17.md

Proves a lemma about the `embanked_batch` type, specifically concerning its final state. It demonstrates that for any `embanked_batch i e ne h_1 h_2`, there exists an `e'` such that `embanked_batch (i mod 2)` holds for `e'` and `ne`.

```coq
Lemma embanked_batch_last {i e ne h_1 h_2}:
  embanked_batch i e ne h_1 h_2 ->
  exists e',
  embanked_batch (i mod 2) e' ne h_1 h_2.


```

--------------------------------

### OCaml Coq Lemmas for Increment and Overflow Operations

Source: https://github.com/ccz181078/coq-bb5/blob/main/CoqBB5/BB5/BB5_Skelet17.md

This snippet contains OCaml code defining Coq lemmas related to incrementing and handling overflows in tape configurations represented by `lower`. These lemmas are crucial for proving the correctness of various tape operations.

```ocaml
Lemma increment_S_even : forall x xs y z zs,
  Forall Nonzero xs ->
  Forall Even xs ->
  Even (S x) ->
  Odd y ->
  lower (S x :: xs ++ y :: z :: zs) -->*
  lower (x :: xs ++ y :: S z :: zs).

Lemma increment_S_odd : forall x y xs,
  Odd (S x) ->
  lower (S x :: y :: xs) -->*
  lower (x :: S y :: xs).

Lemma increment_O : forall xs y z zs,
  Forall Nonzero xs ->
  Forall Even xs ->
  Odd y ->
  lower (O :: xs ++ y :: z :: zs) -->*
  lower (xs ++ y :: S z :: zs).

Lemma overflow_S : forall x xs y,
  Forall Nonzero xs ->
  Forall Even xs ->
  Even (S x) ->
  Odd y ->
  lower (S x :: xs ++ [y]) -->*
  lower (x :: xs ++ [S y; 1; 0; 0]%nat).

Lemma overflow_O : forall xs y,
  Forall Nonzero xs ->
  Forall Even xs ->
  Odd y ->
  lower (O :: xs ++ [y]) -->*
  lower (xs ++ [S y; 1; 0; 0]%nat).

Lemma zero_S : forall x xs y,
  Forall Nonzero xs ->
  Forall Even xs ->
  Even (S x) ->
  Even y ->
  lower (S x :: xs ++ [y]) -->*
  lower (x :: xs ++ [S y; 0; 0]%nat).

Lemma zero_O : forall xs y,
  Forall Nonzero xs ->
  Forall Even xs ->
  Even y ->
  lower (O :: xs ++ [y]) -->*
  lower (xs ++ [S y; 0; 0]%nat).

```

--------------------------------

### Extracting Enumeration Results with Shell Script

Source: https://github.com/ccz181078/coq-bb5/blob/main/CoqBB5/BB5/README.md

This script extracts halting status and decider IDs for all enumerated machines from the Coq proof. It runs within the 'BB5_Extraction' directory and produces a large CSV file named 'BB5_verified_enumeration.csv'. The process relies on OCaml extraction of the Coq code and is estimated to take approximately 2 hours.

```shell
cd BB5_Extraction
./BB5_Extraction.sh
```

--------------------------------

### Run BB4 Extraction Script

Source: https://github.com/ccz181078/coq-bb5/blob/main/CoqBB5/BB4/BB4_Extraction/README.md

Executes the BB4_Extraction.sh script. This script compiles OCaml files, runs the Tree Normal Form enumeration and deciders, generates a CSV file, cleans it, and validates its integrity.

```shell
./BB4_Extraction.sh
```

--------------------------------

### OCaml: Grey Code to Binary Conversion and State Management

Source: https://github.com/ccz181078/coq-bb5/blob/main/CoqBB5/BB5/BB5_Skelet17.md

This snippet defines functions in OCaml for converting Grey codes to binary, transforming lists of naturals to binary lists, and converting binary lists to natural numbers. It also includes definitions to extract the current value (n), sign (s), and digit count (l) from a state tuple (nat*(list nat)).

```ocaml
(* decode of Grey Code *)
Fixpoint grey_to_binary(xs:list bool):(list bool) :=
match xs with
| nil => nil
| xh::xt => (xorb xh (hd false (grey_to_binary xt)))::(grey_to_binary xt)
end.

Definition list_to_binary(xs:list nat):(list bool) :=
  grey_to_binary (map odd xs).

Fixpoint binary_to_nat(xs:list bool):nat :=
match xs with
| nil => O
| xh::xt ->
  (if xh then (S O) else O)+(binary_to_nat xt)*2
end.

(* n (binary) *)
Definition to_n_binary(s:nat*(list nat)) :=
  list_to_binary (snd s).

(* n *)
Definition to_n(s:nat*(list nat)) :=
  binary_to_nat (to_n_binary s).

(* s *)
Definition to_s(s:nat*(list nat)) :=
  let (x,xs):=s in
  xorb (even x) (hd false (list_to_binary xs)).

(* l *)
Definition to_l(s:nat*(list nat)) :=
  length (to_n_binary s).
```