PrintForm Definitions sat lemmas Sections ClassicalProps(jlc) Doc

At: assignment monotone 1 1
1. f: Formula

a,a':Assignment. a' extends a (a |= f a' |= f ) & (a | f a' | f)
By: FormulaRankInd -1
Generated subgoals:

12. x: Var
a,a':Assignment. a' extends a (a |= x a' |= x ) & (a | x a' | x)
22. x: Formula
3. a,a':Assignment. a' extends a (a |= x a' |= x ) & (a | x a' | x)
a,a':Assignment. a' extends a (a |= x a' |= x ) & (a | x a' | x)
32. x1: Formula
3. x2: Formula
4. a,a':Assignment. a' extends a (a |= x1 a' |= x1 ) & (a | x1 a' | x1)
5. a,a':Assignment. a' extends a (a |= x2 a' |= x2 ) & (a | x2 a' | x2)
a,a':Assignment. a' extends a (a |= x1x2 a' |= x1x2 ) & (a | x1x2 a' | x1x2)
42. x1: Formula
3. x2: Formula
4. a,a':Assignment. a' extends a (a |= x1 a' |= x1 ) & (a | x1 a' | x1)
5. a,a':Assignment. a' extends a (a |= x2 a' |= x2 ) & (a | x2 a' | x2)
a,a':Assignment. a' extends a (a |= x1x2 a' |= x1x2 ) & (a | x1x2 a' | x1x2)
52. y1: Formula
3. y2: Formula
4. a,a':Assignment. a' extends a (a |= y1 a' |= y1 ) & (a | y1 a' | y1)
5. a,a':Assignment. a' extends a (a |= y2 a' |= y2 ) & (a | y2 a' | y2)
a,a':Assignment. a' extends a (a |= y1y2 a' |= y1y2 ) & (a | y1y2 a' | y1y2)

About:
allimpliesand