scheme :: MSAFREE5:sch 2
TermInd{ P1[ set ], F1() -> non empty non void ManySortedSign , F2() -> V5() ManySortedSet of the carrier of F1(), F3() -> Element of (Free (F1(),F2())) } :
P1[F3()]
provided
A1: for s being SortSymbol of F1()
for x being Element of F2() . s holds P1[x -term ] and
A2: for o being OperSymbol of F1()
for p being Element of Args (o,(Free (F1(),F2()))) st ( for t being Element of (Free (F1(),F2())) st t in rng p holds
P1[t] ) holds
P1[o -term p]