User:IssaRice/Logical inductor construction: Difference between revisions
No edit summary |
No edit summary |
||
| Line 1: | Line 1: | ||
Notes from the Logical Induction paper as I walk through the construction of LIA in section 5. | |||
==Lemma 5.1.1 (Fixed Point Lemma)== | ==Lemma 5.1.1 (Fixed Point Lemma)== | ||
Revision as of 00:54, 25 June 2019
Notes from the Logical Induction paper as I walk through the construction of LIA in section 5.
Lemma 5.1.1 (Fixed Point Lemma)
The following is used in the Fixed Point Lemma (5.1.1):
Writing the -strategy as
we have
But so the two sums cancel to obtain .