Kindelia/Kind2
1
1
Fork 0
mirror of https://github.com/Kindelia/Kind2.git synced 2024-11-05 07:05:32 +03:00
Code Issues Projects Releases Wiki Activity

Revert "prove RLP.aux.0"

Browse Source 
This reverts commit f694cb0143.
This commit is contained in:
MaiaVictor 2021-11-10 20:26:18 -03:00
parent 3525f7e0ca
commit 9d0ff9cf49
1 changed files with 2 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
base/RLP/aux.kind
View File

@ -5,14 +5,9 @@
RLP.aux.0(
add: Nat
len: Nat
H0: Either<Equal<Nat, add, 128>, Equal<Nat, add, 192>>
pf0: Either<Equal<Nat, add, 128>, Equal<Nat, add, 192>>
): Nat.ltn(0,Nat.add(add,len)) == Bool.true
case H0 {
} default
case mirror(H0.value) {
refl:
refl
}: Nat.ltn(0,Nat.add(self.b,len)) == Bool.true
RLP.aux.0(add, len, pf0)
// TODO: include `a <= 192`
RLP.aux.1(