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

prove RLP.aux.0

Browse Source
This commit is contained in:
Rígille S. B. Menezes 2021-11-10 19:38:50 -03:00
parent d87ada0334
commit f694cb0143
1 changed files with 7 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
base/RLP/aux.kind
View File

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