\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: ""

{λ[sigma:Set] . λ[r:∀[x:sigma] . ∀[y:sigma] . Prop] . λ[refr1:∀[x:sigma] . (x) . (x) . r] . λ[symr1:∀[x:sigma] . ∀[y:sigma] . ∀[t:(y) . (x) . r] . (x) . (y) . r] . λ[trr1:∀[x:sigma] . ∀[y:sigma] . ∀[z:sigma] . ∀[t:(y) . (x) . r] . ∀[u:(z) . (y) . r] . (z) . (x) . r] . λ[s0:(sigma) . set ] . λ[ecs0:{(s0) . (trr1) . (symr1) . (refr1) . (r) . (sigma)} . anec ] . λ[t0:(sigma) . set ] . λ[ect0:{(t0) . (trr1) . (symr1) . (refr1) . (r) . (sigma)} . anec ] . λ[s:sigma] . λ[ses0:{(s0) . (s) . (sigma)} . esti ] . λ[t:sigma] . λ[tet0:{(t0) . (t) . (sigma)} . esti ] . λ[tsr:(t) . (s) . r]} . <{(t0) . (s0) . ((sigma) . set )} . is > . {({({(tet0) . (t) . (ect0) . (t0) . (trr1) . (symr1) . (refr1) . (r) . (sigma)} . th2 ) . ({(t) . (trr1) . (symr1) . (refr1) . (r) . (sigma)} . ecelt ) . (t0) . ((sigma) . set )} . symis ) . ({(tsr) . (t) . (s) . (trr1) . (symr1) . (refr1) . (r) . (sigma)} . th4 ) . ({(ses0) . (s) . (ecs0) . (s0) . (trr1) . (symr1) . (refr1) . (r) . (sigma)} . th2 ) . (t0) . ({(t) . (trr1) . (symr1) . (refr1) . (r) . (sigma)} . ecelt ) . ({(s) . (trr1) . (symr1) . (refr1) . (r) . (sigma)} . ecelt ) . (s0) . ((sigma) . set )} . tr3is

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