INFIX	150L	*
OUTFIX		< . >
LEFTFIX	150	/ .
INFIX	140T	>>>

BIND    x SCOPE P IN	/ x. P 

CONJECTUREPANEL "Lambda-calcolo"
THEOREMS Equality(OBJECT x,OBJECT y,OBJECT z,OBJECT w) ARE
 tt l= !x.	(x >>> x) AND
 tt l= !x.!y.!z.	((x >>> y & y >>> z) => x >>> z) AND
 tt l= !x.!y.	(((!z.((x*z) >>>  (y*z)))) => x >>> y) AND
 tt l= !x.!y.!z.!w.	((x >>> y & z >>> w) => (x*z) >>>  (y*w)) AND
 tt l= !x.!y.	((!z.(x >>> y) =>/z.x >>> /z.y))
END
THEOREMS Abstraction(P,OBJECT x,OBJECT y,OBJECT z) ARE
 tt l= !x.	(/z.P(z))*x >>> P(x) AND
 tt l= !x.	P(x) >>> (/z.P(z))*x
END
BUTTON "Apply" IS Apply ApplicaC COMMAND
BUTTON "Property" IS Apply applyAsAProperty COMMAND 
BUTTON "Instance" IS Apply applyAsAnExample COMMAND 
BUTTON "Apply as Rule" IS Apply applyInLineInference COMMAND
END

CONJECTUREPANEL "Lambda-calcolo -- problemi"
THEOREMS Coppie(OBJECT x,OBJECT y,OBJECT z) ARE
 tt l= !x.!y.	((/z.(z*x*y))*(/x.(/y.x)))  >>> x AND
 tt l= !x.!y.	((/z.(z*x*y))*(/x.(/y.y)))  >>> y
END
THEOREM (OBJECT x,OBJECT w) IS
 tt l= !w.	(/x.(w*(x*x)))*(/x.(w*(x*x))) >>> w*((/x.(w*(x*x)))*(/x.(w*(x*x))))
BUTTON "Apply" IS Apply ApplicaC COMMAND
BUTTON "Property" IS Apply applyAsAProperty COMMAND 
BUTTON "Instance" IS Apply applyAsAnExample COMMAND 
BUTTON "Apply as Rule" IS Apply applyInLineInference COMMAND
END

/*------------Assiomatizzazione della Teoria di Church----------------*/
CONJECTUREPANEL "Lambda-calcolo"
PROOF "tt l =!x.!y.((!z.(x>>>y)=>/z.x>>>/z.y))"
(OBJECT x, OBJECT y, OBJECT z)
INFER tt l =!x.!y.((!z.(x>>>y)=>/z.x>>>/z.y))
FORMULAE
0 tt,
1 !x.!y.((!z.(x>>>y)=>/z.x>>>/z.y))
IS
Axiom[0,1\P,Q]
END
CONJECTUREPANEL "Lambda-calcolo"
PROOF "tt l =!x.(x>>>x)"
(OBJECT x)
INFER tt l =!x.(x>>>x)
FORMULAE
0 tt,
1 !x.(x>>>x)
IS
Axiom[0,1\P,Q]
END
CONJECTUREPANEL "Lambda-calcolo"
PROOF "tt l =!x.!y.!z.!w.((x>>>y&z>>>w)=>(x*z)>>>(y*w))"
(OBJECT x, OBJECT y, OBJECT z, OBJECT w)
INFER tt l =!x.!y.!z.!w.((x>>>y&z>>>w)=>(x*z)>>>(y*w))
FORMULAE
0 tt,
1 !x.!y.!z.!w.((x>>>y&z>>>w)=>(x*z)>>>(y*w))
IS
Axiom[0,1\P,Q]
END
CONJECTUREPANEL "Lambda-calcolo"
PROOF "tt l =!x.!y.!z.((x>>>y&y>>>z)=>x>>>z)"
(OBJECT x, OBJECT y, OBJECT z)
INFER tt l =!x.!y.!z.((x>>>y&y>>>z)=>x>>>z)
FORMULAE
0 tt,
1 !x.!y.!z.((x>>>y&y>>>z)=>x>>>z)
IS
Axiom[0,1\P,Q]
END
CONJECTUREPANEL "Lambda-calcolo"
PROOF "tt l =!x.!y.(!z.((x*z)>>>(y*z))=>x>>>y)"
(OBJECT x, OBJECT y, OBJECT z)
INFER tt l =!x.!y.(!z.((x*z)>>>(y*z))=>x>>>y)
FORMULAE
0 tt,
1 !x.!y.(!z.((x*z)>>>(y*z))=>x>>>y)
IS
Axiom[0,1\P,Q]
END
CONJECTUREPANEL "Lambda-calcolo"
PROOF "tt l =!x./z.P(z)*x>>>P(x)"
(P, OBJECT x, OBJECT z)
INFER tt l =!x./z.P(z)*x>>>P(x)
FORMULAE
0 tt,
1 !x./z.P(z)*x>>>P(x)
IS
Axiom[0,1\P,Q]
END