TransposePROOF.axes_facts: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/tensor/transpose_PROOF.bend as TransposePROOF Lines 31-117 of bendtorch-core@0.1.0.0/src/tensor/transpose_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/transpose_PROOF.bend&start_line=31&end_line=117 import Base import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith import bendtorch-core@0.1.0.0/src/tensor/transpose_spec.bend as Transpose def axes_facts(+dims: List<&2, U32>, +a: Nat, +b: Nat, +bound: Shape.LE(Shape.rank_dimensions(dims), 4n), +inside: {True{} == Transpose.axes_valid(Shape.rank_dimensions(dims), a, b) : Bool}) -> AxesFacts: match dims a b: case Nil{} 0n 0n: Certified{{==}, {==}, {==}} case Nil{} 1n+p b: Empty.absurd(AxesFacts, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(1n+p, 1n), Nat.is_lt(b, 1n), Equal.sym(Bool, True{}, Bool.and(Nat.is_lt(1n+p, 1n), Nat.is_lt(b, 1n)), inside)))) case Nil{} a 1n+p: Empty.absurd(AxesFacts, Arith.lt_zero(p, Arith.and_right(Nat.is_lt(a, 1n), Nat.is_lt(1n+p, 1n), Equal.sym(Bool, True{}, Bool.and(Nat.is_lt(a, 1n), Nat.is_lt(1n+p, 1n)), inside)))) case +d0 <> Nil{} 0n 0n: Certified{{==}, {==}, {==}} case +d0 <> Nil{} 1n+p b: Empty.absurd(AxesFacts Nil{}, 1n+p, b>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(1n+p, 1n), Nat.is_lt(b, 1n), Equal.sym(Bool, True{}, Bool.and(Nat.is_lt(1n+p, 1n), Nat.is_lt(b, 1n)), inside)))) case +d0 <> Nil{} a 1n+p: Empty.absurd(AxesFacts Nil{}, a, 1n+p>, Arith.lt_zero(p, Arith.and_right(Nat.is_lt(a, 1n), Nat.is_lt(1n+p, 1n), Equal.sym(Bool, True{}, Bool.and(Nat.is_lt(a, 1n), Nat.is_lt(1n+p, 1n)), inside)))) case +d0 <> +d1 <> Nil{} 0n 0n: Certified{{==}, {==}, {==}} case +d0 <> +d1 <> Nil{} 0n 1n: Certified{{==}, {==}, {==}} case +d0 <> +d1 <> Nil{} 1n 0n: Certified{{==}, {==}, {==}} case +d0 <> +d1 <> Nil{} 1n 1n: Certified{{==}, {==}, {==}} case +d0 <> +d1 <> Nil{} 2n+p b: Empty.absurd(AxesFacts d1 <> Nil{}, 2n+p, b>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(2n+p, 2n), Nat.is_lt(b, 2n), Equal.sym(Bool, True{}, Bool.and(Nat.is_lt(2n+p, 2n), Nat.is_lt(b, 2n)), inside)))) case +d0 <> +d1 <> Nil{} a 2n+p: Empty.absurd(AxesFacts d1 <> Nil{}, a, 2n+p>, Arith.lt_zero(p, Arith.and_right(Nat.is_lt(a, 2n), Nat.is_lt(2n+p, 2n), Equal.sym(Bool, True{}, Bool.and(Nat.is_lt(a, 2n), Nat.is_lt(2n+p, 2n)), inside)))) case +d0 <> +d1 <> +d2 <> Nil{} 0n 0n: Certified{{==}, {==}, {==}} case +d0 <> +d1 <> +d2 <> Nil{} 0n 1n: Certified{{==}, {==}, {==}} case +d0 <> +d1 <> +d2 <> Nil{} 0n 2n: Certified{{==}, {==}, {==}} case +d0 <> +d1 <> +d2 <> Nil{} 1n 0n: Certified{{==}, {==}, {==}} case +d0 <> +d1 <> +d2 <> Nil{} 1n 1n: Certified{{==}, {==}, {==}} case +d0 <> +d1 <> +d2 <> Nil{} 1n 2n: Certified{{==}, {==}, {==}} case +d0 <> +d1 <> +d2 <> Nil{} 2n 0n: Certified{{==}, {==}, {==}} case +d0 <> +d1 <> +d2 <> Nil{} 2n 1n: Certified{{==}, {==}, {==}} case +d0 <> +d1 <> +d2 <> Nil{} 2n 2n: Certified{{==}, {==}, {==}} case +d0 <> +d1 <> +d2 <> Nil{} 3n+p b: Empty.absurd(AxesFacts d1 <> d2 <> Nil{}, 3n+p, b>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(3n+p, 3n), Nat.is_lt(b, 3n), Equal.sym(Bool, True{}, Bool.and(Nat.is_lt(3n+p, 3n), Nat.is_lt(b, 3n)), inside)))) case +d0 <> +d1 <> +d2 <> Nil{} a 3n+p: Empty.absurd(AxesFacts d1 <> d2 <> Nil{}, a, 3n+p>, Arith.lt_zero(p, Arith.and_right(Nat.is_lt(a, 3n), Nat.is_lt(3n+p, 3n), Equal.sym(Bool, True{}, Bool.and(Nat.is_lt(a, 3n), Nat.is_lt(3n+p, 3n)), inside)))) case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 0n 0n: Certified{{==}, {==}, {==}} case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 0n 1n: Certified{{==}, {==}, {==}} case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 0n 2n: Certified{{==}, {==}, {==}} case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 0n 3n: Certified{{==}, {==}, {==}} case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 1n 0n: Certified{{==}, {==}, {==}} case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 1n 1n: Certified{{==}, {==}, {==}} case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 1n 2n: Certified{{==}, {==}, {==}} case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 1n 3n: Certified{{==}, {==}, {==}} case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 2n 0n: Certified{{==}, {==}, {==}} case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 2n 1n: Certified{{==}, {==}, {==}} case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 2n 2n: Certified{{==}, {==}, {==}} case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 2n 3n: Certified{{==}, {==}, {==}} case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 3n 0n: Certified{{==}, {==}, {==}} case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 3n 1n: Certified{{==}, {==}, {==}} case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 3n 2n: Certified{{==}, {==}, {==}} case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 3n 3n: Certified{{==}, {==}, {==}} case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} 4n+p b: Empty.absurd(AxesFacts d1 <> d2 <> d3 <> Nil{}, 4n+p, b>, Arith.lt_zero(p, Arith.and_left(Nat.is_lt(4n+p, 4n), Nat.is_lt(b, 4n), Equal.sym(Bool, True{}, Bool.and(Nat.is_lt(4n+p, 4n), Nat.is_lt(b, 4n)), inside)))) case +d0 <> +d1 <> +d2 <> +d3 <> Nil{} a 4n+p: Empty.absurd(AxesFacts d1 <> d2 <> d3 <> Nil{}, a, 4n+p>, Arith.lt_zero(p, Arith.and_right(Nat.is_lt(a, 4n), Nat.is_lt(4n+p, 4n), Equal.sym(Bool, True{}, Bool.and(Nat.is_lt(a, 4n), Nat.is_lt(4n+p, 4n)), inside)))) case +d0 <> +d1 <> +d2 <> +d3 <> +d4 <> +tail a b: match bound: Uses (15): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=LE https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=rank_dimensions https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=and_left https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=and_right https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=lt_zero https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transpose_PROOF.bend&name=AxesFacts https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transpose_spec.bend&name=axes_valid