~/jendhub

def un.not_tail

bend-osdev-u32@0.1.0.0 · PROOF.bend:476

import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOF
import Base

476# 2 + (2N + 2T) = 2 * K, from 1 + (N + T) = K
477def un.not_tail(+nv: Nat, +tv: Nat, -k: Nat, ih: {1n+Nat.add(nv, tv) == k : Nat}) -> {2n+Nat.add(Nat.double(nv), Nat.double(tv)) == Nat.double(k) : Nat}:
478  Equal.trans(Nat, 2n+Nat.add(Nat.double(nv), Nat.double(tv)), Nat.double(1n+Nat.add(nv, tv)), Nat.double(k), un.succ_cong(1n+Nat.add(Nat.double(nv), Nat.double(tv)), 1n+Nat.double(Nat.add(nv, tv)), un.succ_cong(Nat.add(Nat.double(nv), Nat.double(tv)), Nat.double(Nat.add(nv, tv)), Equal.sym(Nat, Nat.double(Nat.add(nv, tv)), Nat.add(Nat.double(nv), Nat.double(tv)), un.double_add(nv, tv)))), un.double_cong(1n+Nat.add(nv, tv), k, ih))

Uses (8)

Used by (1)