λδ digital library (LDDL)
Constant
Informal description: ""
{λ[x0:rat].λ[x:frac].λ[xix0:{((x0).class).(x)}.inf]}.<{(x).({({(1).(1)}.fr).(x)}.tf)}.eq>.{({((x).fris).(x).({((x).den).((x).num)}.fr)}.refeq1).({(((x).den).satz28a).(((x).num).satz28a).((x).den).((x).num).({(1).((x).den)}.ts).({(1).((x).num)}.ts)}.eqnd).({(1).(1).(x)}.tfeq1a).(x).({((x).den).((x).num)}.fr).({({(1).((x).den)}.ts).({(1).((x).num)}.ts)}.fr).({({(1).(1)}.fr).(x)}.tf)}.tr3eq Validation parameters: sort hierarchy = "Z2", kernel options = ""
Last update: Sat, 12 Dec 2020 10:46:54 +0100