View file src/slc/grandparent-new.prf - Download

! gpRule1 
 ^x ^y ^z ((parent x y : parent y z : grandparent x z) = [*])
 
! gpAxiom1 ((parent allan brenda) = [*])

! gpAxiom2 ((parent brenda charles) = [*]) 

! gpTheorem1
 ( grandparent allan charles ;
   gpAxiom2 (grandparent allan charles) ;
   gpAxiom1 (parent brenda charles (grandparent allan charles)) ;
   gpRule1 allan brenda charles )

gpTheorem1