\lambda\delta home page

home	news	documentation	specification		implementation
foreword	milestones	version 2	version 2	(background - core - applications)	library	(static LDDL directory)
citations	visibility	version 1	version 1	(static HELM directory)	helena

Informal description: ""

{λ[x: frac ] . λ[y: frac ]} . <{(x) . ({({(y) . (x)} . v ) . (y)} . tf )} . eq > . {({({({(y) . (x)} . 2y ) . ({(y) . (x)} . 1y )} . ts ) . (x)} . satz40a ) . ({({({(y) . (x)} . 2y ) . ({(y) . (x)} . 1y ) . ((x) . 2x )} . assts1 ) . ({({({({(y) . (x)} . 1y ) . ({(y) . (x)} . 2y )} . comts ) . ((x) . 1x ) . ({({(y) . (x)} . 2y ) . ({(y) . (x)} . 1y )} . ts ) . ({({(y) . (x)} . 1y ) . ({(y) . (x)} . 2y )} . ts )} . ists2 ) . ({({(y) . (x)} . 1y ) . ({(y) . (x)} . 2y ) . ((x) . 1x )} . assts1 ) . ({({({(y) . (x)} . 2y ) . ({(y) . (x)} . 1y )} . ts ) . ((x) . 1x )} . ts ) . ({({({(y) . (x)} . 1y ) . ({(y) . (x)} . 2y )} . ts ) . ((x) . 1x )} . ts ) . ({({(y) . (x)} . 1y ) . ({({(y) . (x)} . 2y ) . ((x) . 1x )} . ts )} . ts ) . ( nat )} . tris ) . ({({({(y) . (x)} . 2y ) . ({(y) . (x)} . 1y )} . ts ) . ((x) . 2x )} . ts ) . ({({({(y) . (x)} . 2y ) . ({(y) . (x)} . 1y )} . ts ) . ((x) . 1x )} . ts ) . ({({(y) . (x)} . 2y ) . ({({(y) . (x)} . 1y ) . ((x) . 2x )} . ts )} . ts ) . ({({(y) . (x)} . 1y ) . ({({(y) . (x)} . 2y ) . ((x) . 1x )} . ts )} . ts )} . eqnd ) . ({({({(y) . (x)} . 1y ) . ((x) . 2x )} . ts ) . ({({(y) . (x)} . 2y ) . ((x) . 1x )} . ts ) . (y)} . tfeq2a ) . ({({(y) . (x)} . v ) . (y)} . comtf ) . (x) . ({({({({(y) . (x)} . 2y ) . ({(y) . (x)} . 1y )} . ts ) . ((x) . 2x )} . ts ) . ({({({(y) . (x)} . 2y ) . ({(y) . (x)} . 1y )} . ts ) . ((x) . 1x )} . ts )} . fr ) . ({({({(y) . (x)} . 2y ) . ({({(y) . (x)} . 1y ) . ((x) . 2x )} . ts )} . ts ) . ({({(y) . (x)} . 1y ) . ({({(y) . (x)} . 2y ) . ((x) . 1x )} . ts )} . ts )} . fr ) . ({(y) . ({(y) . (x)} . v )} . tf ) . ({({(y) . (x)} . v ) . (y)} . tf )} . tr4eq

Validation parameters: sort hierarchy = "Z2", kernel options = ""