baruchel/coqbooks
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update

Browse Source
This commit is contained in:
Thomas Baruchel 2023-01-11 00:34:54 +01:00
parent 055147eadd
commit c1324660ba
1 changed files with 23 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

33
src/thue_morse2.v
View File

@ -207,15 +207,6 @@ Proof.
Qed.
Lemma two_step_consecutive_identical_length :
forall (n : nat) (hd a tl : list bool),
tm_step n = hd ++ a ++ tl -> length a = 5
@ -246,7 +237,29 @@ Proof.
exists (true::false::nil). exists (true::nil). exists true. simpl. reflexivity.
exists (true::false::nil). exists (false::nil). exists true. simpl. reflexivity.
apply tm_step_factor5 in H. contradiction H. reflexivity. reflexivity.
exists (true::false::true::nil). exists (nil). exists false. simpl. reflexivity.
exists (true::false::false::nil). exists (nil). exists true. simpl. reflexivity.
exists (true::nil). exists (true::false::nil). exists false. simpl. reflexivity.
exists (true::nil). exists (false::true::nil). exists false. simpl. reflexivity.
exists (true::false::nil). exists (false::nil). exists false. simpl. reflexivity.
exists (false::nil). exists (true::true::nil). exists true. simpl. reflexivity.
exists (false::nil). exists (true::false::nil). exists true. simpl. reflexivity.
exists (false::nil). exists (false::true::nil). exists true. simpl. reflexivity.
exists (false::nil). exists (false::false::nil). exists true. simpl. reflexivity.
exists (false::true::false::nil). exists (nil). exists true. simpl. reflexivity.
apply tm_step_factor5' in H. contradiction H. reflexivity. reflexivity.
exists (false::true::nil). exists (true::nil). exists false. simpl. reflexivity.
exists (false::true::nil). exists (false::nil). exists false. simpl. reflexivity.
exists (false::false::nil). exists (true::nil). exists true. simpl. reflexivity.
exists (false::false::nil). exists (false::nil). exists true. simpl. reflexivity.
exists (nil). exists (true::false::true::nil). exists false. simpl. reflexivity.
exists (nil). exists (true::false::false::nil). exists false. simpl. reflexivity.
exists (nil). exists (false::true::true::nil). exists false. simpl. reflexivity.
exists (nil). exists (false::true::false::nil). exists false. simpl. reflexivity.
exists (nil). exists (false::false::true::nil). exists false. simpl. reflexivity.
exists (nil). exists (false::false::false::nil). exists false. simpl. reflexivity.
Qed.