HigherOrderCO/Kind1
1
1
Fork 0
mirror of https://github.com/HigherOrderCO/Kind1.git synced 2024-09-11 08:45:32 +03:00
Code Issues Packages Projects Releases Wiki Activity

prove assumptions of recursive call

Browse Source
This commit is contained in:
Rígille S. B. Menezes 2021-12-01 11:07:59 -03:00
parent 2d3d04fdcf
commit ccf09c2ce8
1 changed files with 13 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
base/Nat/div_mod/spec.kind
View File

@ -40,7 +40,19 @@ Nat.div_mod.spec(
let succ_out = Nat.div_mod.go.succ_quotient(d, 0, Nat.sub(n,d))
case succ_out {
refl:
let ind = Nat.div_mod.spec(Nat.sub(n, d), q.pred, d, r, ?H0, ?H1)
let H0 = mirror(H0)
let H0 = case Nat.add.swap(r, d, Nat.mul(q.pred, d)) {
refl:
H0
}: Equal(Nat, n, self.b)
let H0 = apply((x) Nat.sub(x, d), H0)
let H0 = case Nat.add.sub(d, Nat.add(r, Nat.mul(q.pred, d))) {
refl:
H0
}: Equal(Nat, Nat.sub(n, d), self.b)
let H1 = mirror(H1)
let H1 = Nat.lte.comm.false(d, r, H1)
let ind = Nat.div_mod.spec(Nat.sub(n, d), q.pred, d, r, H0, H1)
case ind {
refl:
refl