Alph*Alph*Prop

x,y,z:Alph*. (x R y) ((z @ x) R (z @ y))

(x,y:Alph*//(x R y))

Fin((x,y:Alph*//(x R y))(x,y:Alph*//(x R y)))

a:Alph, x:x,y:Alph*//(x R y). a.x x,y:Alph*//(x R y)

fL:((x,y:Alph*//(x R y))(x,y:Alph*//(x R y)))*. t:((x,y:Alph*//(x R y))(x,y:Alph*//(x R y))). (x.x/x1,x2.(g(x1)) = (g(x2)))(t) mem_f((x,y:Alph*//(x R y))(x,y:Alph*//(x R y));t;fL)

< (x,y:Alph*//(x R y))(x,y:Alph*//(x R y)),a,xy. xy/x,y. < a.x,a.y > > ActionSet(Alph)

x,y:x,y:Alph*//(x R y). Dec(x Rg y)

Analyze -2
THEN
Inst Thm* S:ActionSet(Alph), sL:S.car*. Fin(Alph) Fin(S.car) (TBL:S.car*. s:S.car. mem_f(S.car;s;TBL) (w:Alph*. mem_f(S.car;(S:ws);sL))) [Alph; < (x,y:Alph*//(x R y))(x,y:Alph*//(x R y)),a,xy. xy/x,y. < a.x,a.y > > ;fL]

1

10. fL: ((x,y:Alph*//(x R y))(x,y:Alph*//(x R y)))* 11. t:((x,y:Alph*//(x R y))(x,y:Alph*//(x R y))). (x.x/x1,x2.(g(x1)) = (g(x2)))(t) mem_f((x,y:Alph*//(x R y))(x,y:Alph*//(x R y));t;fL) 12. < (x,y:Alph*//(x R y))(x,y:Alph*//(x R y)),a,xy. xy/x,y. < a.x,a.y > > ActionSet(Alph) Fin( < (x,y:Alph*//(x R y))(x,y:Alph*//(x R y)),a,xy. xy/x,y. < a.x,a.y > > .car)

2

10. fL: ((x,y:Alph*//(x R y))(x,y:Alph*//(x R y)))* 11. t:((x,y:Alph*//(x R y))(x,y:Alph*//(x R y))). (x.x/x1,x2.(g(x1)) = (g(x2)))(t) mem_f((x,y:Alph*//(x R y))(x,y:Alph*//(x R y));t;fL) 12. < (x,y:Alph*//(x R y))(x,y:Alph*//(x R y)),a,xy. xy/x,y. < a.x,a.y > > ActionSet(Alph) 13. TBL: < (x,y:Alph*//(x R y))(x,y:Alph*//(x R y)),a,xy. xy/x,y. < a.x,a.y > > .car*. s: < (x,y:Alph*//(x R y))(x,y:Alph*//(x R y)),a,xy. xy/x,y. < a.x,a.y > > .car. mem_f( < (x,y:Alph*//(x R y))(x,y:Alph*//(x R y)),a,xy. xy/x,y. < a.x,a.y > > .car;s;TBL) (w:Alph*. mem_f( < (x,y:Alph*//(x R y))(x,y:Alph*//(x R y)) ,a,xy. xy/x,y. < a.x,a.y > > .car;( < (x,y:Alph*//(x R y))(x,y:Alph*//(x R y)) ,a,xy. xy/x,y. < a.x,a.y > > :ws);fL)) x,y:x,y:Alph*//(x R y). Dec(x Rg y)

About: