vault backup: 2025-03-03 19:26:59
This commit is contained in:
parent
8991168716
commit
8cebb49ee6
1 changed files with 3 additions and 0 deletions
|
@ -225,3 +225,6 @@ Induction (true for ℓ, to be proved for ℓ+1):
|
||||||
Reverse induction on ℓ
|
Reverse induction on ℓ
|
||||||
Base ($ℓ=n-1$): trivial
|
Base ($ℓ=n-1$): trivial
|
||||||
|
|
||||||
|
Induction (true for ℓ+1, to be proved for ℓ):
|
||||||
|
- Assume a $p_x$ blocked at level ℓ $\to \exists k\neq x, F[k]\geqℓ+1 \land A\_Y[ℓ+1]=x$
|
||||||
|
-
|
Loading…
Reference in a new issue