Theorema`Common`PRFOBJ$[Theorema`Provers`Common`Private`PRFINFO$[ Theorema`Provers`initialProofSituation, {}, {{Theorema`Common`FML$[{"ID:501871624", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/OneMoreTheorem.nb\ "}, Theorema`Language`Forall$TM[Theorema`Language`RNG$[ Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`A$TM]], Theorema`Language`SIMPRNG$[ Theorema`Language`VAR$[Theorema`Knowledge`B$TM]], Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`C$TM]], Theorema`Language`SIMPRNG$[ Theorema`Language`VAR$[Theorema`Knowledge`x$TM]]], True, Theorema`Language`Implies$TM[Theorema`Language`SubsetEqual$TM[ Theorema`Language`VAR$[Theorema`Knowledge`A$TM], Theorema`Language`VAR$[Theorema`Knowledge`B$TM]], Theorema`Language`Iff$TM[Theorema`Language`Element$TM[ Theorema`Language`VAR$[Theorema`Knowledge`x$TM], Theorema`Language`Backslash$TM[Theorema`Language`VAR$[ Theorema`Knowledge`A$TM], Theorema`Language`VAR$[ Theorema`Knowledge`C$TM]]], Theorema`Language`Element$TM[ Theorema`Language`VAR$[Theorema`Knowledge`x$TM], Theorema`Language`Intersection$TM[Theorema`Language`VAR$[ Theorema`Knowledge`A$TM], Theorema`Language`Backslash$TM[ Theorema`Language`VAR$[Theorema`Knowledge`B$TM], Theorema`Language`VAR$[Theorema`Knowledge`C$TM]]]]]]], "2"], Theorema`Common`FML$[{"ID:1841163329", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/OneMoreTheorem.nb\ "}, Theorema`Language`Forall$TM[Theorema`Language`RNG$[ Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`A$TM]], Theorema`Language`SIMPRNG$[ Theorema`Language`VAR$[Theorema`Knowledge`B$TM]]], True, Theorema`Language`IffDef$TM[Theorema`Language`SubsetEqual$TM[ Theorema`Language`VAR$[Theorema`Knowledge`A$TM], Theorema`Language`VAR$[Theorema`Knowledge`B$TM]], Theorema`Language`Forall$TM[Theorema`Language`RNG$[ Theorema`Language`SETRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`x$TM], Theorema`Language`VAR$[ Theorema`Knowledge`A$TM]]], True, Theorema`Language`Element$TM[ Theorema`Language`VAR$[Theorema`Knowledge`x$TM], Theorema`Language`VAR$[Theorema`Knowledge`B$TM]]]]], "\[SubsetEqual]"], Theorema`Common`FML$[{"ID:790959835", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/OneMoreTheorem.nb\ "}, Theorema`Language`Forall$TM[Theorema`Language`RNG$[ Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`x$TM]], Theorema`Language`SIMPRNG$[ Theorema`Language`VAR$[Theorema`Knowledge`A$TM]], Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`B$TM]]], True, Theorema`Language`IffDef$TM[ Theorema`Language`Element$TM[Theorema`Language`VAR$[ Theorema`Knowledge`x$TM], Theorema`Language`Backslash$TM[ Theorema`Language`VAR$[Theorema`Knowledge`A$TM], Theorema`Language`VAR$[Theorema`Knowledge`B$TM]]], Theorema`Language`And$TM[Theorema`Language`Element$TM[ Theorema`Language`VAR$[Theorema`Knowledge`x$TM], Theorema`Language`VAR$[Theorema`Knowledge`A$TM]], Theorema`Language`Not$TM[Theorema`Language`Element$TM[ Theorema`Language`VAR$[Theorema`Knowledge`x$TM], Theorema`Language`VAR$[Theorema`Knowledge`B$TM]]]]]], "\\"], Theorema`Common`FML$[{"ID:1252989057", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/OneMoreTheorem.nb\ "}, Theorema`Language`Forall$TM[Theorema`Language`RNG$[ Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`x$TM]], Theorema`Language`SIMPRNG$[ Theorema`Language`VAR$[Theorema`Knowledge`A$TM]], Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`B$TM]]], True, Theorema`Language`IffDef$TM[ Theorema`Language`Element$TM[Theorema`Language`VAR$[ Theorema`Knowledge`x$TM], Theorema`Language`Intersection$TM[ Theorema`Language`VAR$[Theorema`Knowledge`A$TM], Theorema`Language`VAR$[Theorema`Knowledge`B$TM]]], Theorema`Language`And$TM[Theorema`Language`Element$TM[ Theorema`Language`VAR$[Theorema`Knowledge`x$TM], Theorema`Language`VAR$[Theorema`Knowledge`A$TM]], Theorema`Language`Element$TM[Theorema`Language`VAR$[ Theorema`Knowledge`x$TM], Theorema`Language`VAR$[ Theorema`Knowledge`B$TM]]]]], "\[Intersection]"]}}, "OriginalPS"], Theorema`Provers`Common`Private`ANDNODE$[ Theorema`Provers`Common`Private`PRFINFO$[Theorema`Provers`forallGoal, {{Theorema`Common`FML$[{"ID:501871624", "Source:/home/wwindste/Publications/Talks/2014-10-WTC/OneMoreTheorem.n\ b"}, Theorema`Language`Forall$TM[Theorema`Language`RNG$[ Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`A$TM]], Theorema`Language`SIMPRNG$[ Theorema`Language`VAR$[Theorema`Knowledge`B$TM]], Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`C$TM]], Theorema`Language`SIMPRNG$[ Theorema`Language`VAR$[Theorema`Knowledge`x$TM]]], True, Theorema`Language`Implies$TM[Theorema`Language`SubsetEqual$TM[ Theorema`Language`VAR$[Theorema`Knowledge`A$TM], Theorema`Language`VAR$[Theorema`Knowledge`B$TM]], Theorema`Language`Iff$TM[Theorema`Language`Element$TM[ Theorema`Language`VAR$[Theorema`Knowledge`x$TM], Theorema`Language`Backslash$TM[Theorema`Language`VAR$[ Theorema`Knowledge`A$TM], Theorema`Language`VAR$[ Theorema`Knowledge`C$TM]]], Theorema`Language`Element$TM[ Theorema`Language`VAR$[Theorema`Knowledge`x$TM], Theorema`Language`Intersection$TM[Theorema`Language`VAR$[ Theorema`Knowledge`A$TM], Theorema`Language`Backslash$TM[ Theorema`Language`VAR$[Theorema`Knowledge`B$TM], Theorema`Language`VAR$[Theorema`Knowledge`C$TM]]]]]]], "2"]}}, {{Theorema`Common`FML$[{"ID:formula2853", "Source:none"}, Theorema`Language`Implies$TM[Theorema`Language`SubsetEqual$TM[ Theorema`Language`FIX$[Theorema`Knowledge`A$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`B$TM, 0]], Theorema`Language`Iff$TM[Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`Backslash$TM[Theorema`Language`FIX$[ Theorema`Knowledge`A$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`C$TM, 0]]], Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`Intersection$TM[Theorema`Language`FIX$[ Theorema`Knowledge`A$TM, 0], Theorema`Language`Backslash$TM[ Theorema`Language`FIX$[Theorema`Knowledge`B$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`C$TM, 0]]]]]], "G\[NumberSign]0"]}}, "Theorema`Provers`forallGoal$108501", "abf" -> {Theorema`Language`FIX$[Theorema`Knowledge`A$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`B$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`C$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0]}], Theorema`Provers`Common`Private`ANDNODE$[ Theorema`Provers`Common`Private`PRFINFO$[Theorema`Provers`implGoalDirect, {{Theorema`Common`FML$[{"ID:formula2853", "Source:none"}, Theorema`Language`Implies$TM[Theorema`Language`SubsetEqual$TM[ Theorema`Language`FIX$[Theorema`Knowledge`A$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`B$TM, 0]], Theorema`Language`Iff$TM[Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`Backslash$TM[Theorema`Language`FIX$[ Theorema`Knowledge`A$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`C$TM, 0]]], Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`Intersection$TM[Theorema`Language`FIX$[ Theorema`Knowledge`A$TM, 0], Theorema`Language`Backslash$TM[ Theorema`Language`FIX$[Theorema`Knowledge`B$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`C$TM, 0]]]]]], "G\[NumberSign]0"]}}, {{Theorema`Common`FML$[{"ID:formula2861", "Source:none"}, Theorema`Language`SubsetEqual$TM[Theorema`Language`FIX$[ Theorema`Knowledge`A$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`B$TM, 0]], "A\[NumberSign]4"], Theorema`Common`FML$[{"ID:formula2862", "Source:none"}, Theorema`Language`Iff$TM[Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`Backslash$TM[Theorema`Language`FIX$[ Theorema`Knowledge`A$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`C$TM, 0]]], Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`Intersection$TM[Theorema`Language`FIX$[ Theorema`Knowledge`A$TM, 0], Theorema`Language`Backslash$TM[ Theorema`Language`FIX$[Theorema`Knowledge`B$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`C$TM, 0]]]]], "G\[NumberSign]5"]}}, "Theorema`Provers`implGoalDirect$108722"], Theorema`Provers`Common`Private`ANDNODE$[ Theorema`Provers`Common`Private`PRFINFO$[Theorema`Provers`equivGoal, {{Theorema`Common`FML$[{"ID:formula2862", "Source:none"}, Theorema`Language`Iff$TM[Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`Backslash$TM[Theorema`Language`FIX$[ Theorema`Knowledge`A$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`C$TM, 0]]], Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`Intersection$TM[Theorema`Language`FIX$[ Theorema`Knowledge`A$TM, 0], Theorema`Language`Backslash$TM[ Theorema`Language`FIX$[Theorema`Knowledge`B$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`C$TM, 0]]]]], "G\[NumberSign]5"]}}, {{Theorema`Common`FML$[{"ID:formula2872", "Source:none"}, Theorema`Language`Implies$TM[Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`Backslash$TM[Theorema`Language`FIX$[ Theorema`Knowledge`A$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`C$TM, 0]]], Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`Intersection$TM[Theorema`Language`FIX$[ Theorema`Knowledge`A$TM, 0], Theorema`Language`Backslash$TM[ Theorema`Language`FIX$[Theorema`Knowledge`B$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`C$TM, 0]]]]], "G\[NumberSign]10"], Theorema`Common`FML$[{"ID:formula2873", "Source:none"}, Theorema`Language`Implies$TM[ Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`x$TM, 0], Theorema`Language`Intersection$TM[ Theorema`Language`FIX$[Theorema`Knowledge`A$TM, 0], Theorema`Language`Backslash$TM[Theorema`Language`FIX$[ Theorema`Knowledge`B$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`C$TM, 0]]]], Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`Backslash$TM[Theorema`Language`FIX$[ Theorema`Knowledge`A$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`C$TM, 0]]]], "G\[NumberSign]11"]}}, "Theorema`Provers`equivGoal$109021"], Theorema`Provers`Common`Private`ANDNODE$[ Theorema`Provers`Common`Private`PRFINFO$[ Theorema`Provers`implGoalDirect, {{Theorema`Common`FML$[{"ID:formula2872", "Source:none"}, Theorema`Language`Implies$TM[Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`Backslash$TM[Theorema`Language`FIX$[ Theorema`Knowledge`A$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`C$TM, 0]]], Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`Intersection$TM[Theorema`Language`FIX$[ Theorema`Knowledge`A$TM, 0], Theorema`Language`Backslash$TM[ Theorema`Language`FIX$[Theorema`Knowledge`B$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`C$TM, 0]]]]], "G\[NumberSign]10"]}}, {{Theorema`Common`FML$[{"ID:formula2887", "Source:none"}, Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`x$TM, 0], Theorema`Language`Backslash$TM[ Theorema`Language`FIX$[Theorema`Knowledge`A$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`C$TM, 0]]], "A\[NumberSign]18"], Theorema`Common`FML$[{"ID:formula2888", "Source:none"}, Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`x$TM, 0], Theorema`Language`Intersection$TM[ Theorema`Language`FIX$[Theorema`Knowledge`A$TM, 0], Theorema`Language`Backslash$TM[Theorema`Language`FIX$[ Theorema`Knowledge`B$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`C$TM, 0]]]], "G\[NumberSign]19"]}}, "Theorema`Provers`implGoalDirect$109367"], Theorema`Provers`Common`Private`ANDNODE$[ Theorema`Provers`Common`Private`PRFINFO$[Theorema`Provers`instantiate, {}, {}, "Theorema`Provers`instantiate$109762", "instantiation" -> {}], Theorema`Provers`Common`Private`ANDNODE$[ Theorema`Provers`Common`Private`PRFINFO$[Theorema`Provers`expandDef, {{Theorema`Common`FML$[{"ID:formula2888", "Source:none"}, Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`x$TM, 0], Theorema`Language`Intersection$TM[ Theorema`Language`FIX$[Theorema`Knowledge`A$TM, 0], Theorema`Language`Backslash$TM[Theorema`Language`FIX$[ Theorema`Knowledge`B$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`C$TM, 0]]]], "G\[NumberSign]19"]}, {Theorema`Common`FML$[{"ID:formula2887", "Source:none"}, Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`x$TM, 0], Theorema`Language`Backslash$TM[ Theorema`Language`FIX$[Theorema`Knowledge`A$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`C$TM, 0]]], "A\[NumberSign]18"]}, {Theorema`Common`FML$[{"ID:formula2861", "Source:none"}, Theorema`Language`SubsetEqual$TM[ Theorema`Language`FIX$[Theorema`Knowledge`A$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`B$TM, 0]], "A\[NumberSign]4"]}}, {{Theorema`Common`FML$[{"ID:formula2918", "Source:none"}, Theorema`Language`And$TM[ Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`A$TM, 0]], Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`Backslash$TM[Theorema`Language`FIX$[ Theorema`Knowledge`B$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`C$TM, 0]]]], "G\[NumberSign]38"]}, {Theorema`Common`FML$[{"ID:formula2919", "Source:none"}, Theorema`Language`And$TM[Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`A$TM, 0]], Theorema`Language`Not$TM[Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`C$TM, 0]]]], "A\[NumberSign]39"]}, {Theorema`Common`FML$[{"ID:formula2920", "Source:none"}, Theorema`Language`Forall$TM[ Theorema`Language`RNG$[Theorema`Language`SETRNG$[ Theorema`Language`VAR$[Theorema`Knowledge`x$TM], Theorema`Language`FIX$[Theorema`Knowledge`A$TM, 0]]], True, Theorema`Language`Element$TM[Theorema`Language`VAR$[ Theorema`Knowledge`x$TM], Theorema`Language`FIX$[ Theorema`Knowledge`B$TM, 0]]], "A\[NumberSign]40"]}}, "Theorema`Provers`expandDef$110369", "defCond" -> False, "usedDefs" -> {{Theorema`Common`FML$[{"ID:1252989057", "Source:/home/\ wwindste/Publications/Talks/2014-10-WTC/OneMoreTheorem.nb"}, Theorema`Language`Forall$TM[Theorema`Language`RNG$[ Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`x$TM]], Theorema`Language`SIMPRNG$[ Theorema`Language`VAR$[Theorema`Knowledge`A$TM]], Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`B$TM]]], True, Theorema`Language`IffDef$TM[ Theorema`Language`Element$TM[Theorema`Language`VAR$[ Theorema`Knowledge`x$TM], Theorema`Language`Intersection$TM[ Theorema`Language`VAR$[Theorema`Knowledge`A$TM], Theorema`Language`VAR$[Theorema`Knowledge`B$TM]]], Theorema`Language`And$TM[Theorema`Language`Element$TM[ Theorema`Language`VAR$[Theorema`Knowledge`x$TM], Theorema`Language`VAR$[Theorema`Knowledge`A$TM]], Theorema`Language`Element$TM[Theorema`Language`VAR$[ Theorema`Knowledge`x$TM], Theorema`Language`VAR$[ Theorema`Knowledge`B$TM]]]]], "\[Intersection]"]}, {Theorema`Common`FML$[{"ID:790959835", "Source:/home/wwindste/Publi\ cations/Talks/2014-10-WTC/OneMoreTheorem.nb"}, Theorema`Language`Forall$TM[ Theorema`Language`RNG$[Theorema`Language`SIMPRNG$[ Theorema`Language`VAR$[Theorema`Knowledge`x$TM]], Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`A$TM]], Theorema`Language`SIMPRNG$[ Theorema`Language`VAR$[Theorema`Knowledge`B$TM]]], True, Theorema`Language`IffDef$TM[Theorema`Language`Element$TM[ Theorema`Language`VAR$[Theorema`Knowledge`x$TM], Theorema`Language`Backslash$TM[Theorema`Language`VAR$[ Theorema`Knowledge`A$TM], Theorema`Language`VAR$[ Theorema`Knowledge`B$TM]]], Theorema`Language`And$TM[ Theorema`Language`Element$TM[Theorema`Language`VAR$[ Theorema`Knowledge`x$TM], Theorema`Language`VAR$[ Theorema`Knowledge`A$TM]], Theorema`Language`Not$TM[ Theorema`Language`Element$TM[Theorema`Language`VAR$[ Theorema`Knowledge`x$TM], Theorema`Language`VAR$[ Theorema`Knowledge`B$TM]]]]]], "\\"]}, {Theorema`Common`FML$[{"ID:1841163329", "Source:/home/wwindste/Publ\ ications/Talks/2014-10-WTC/OneMoreTheorem.nb"}, Theorema`Language`Forall$TM[ Theorema`Language`RNG$[Theorema`Language`SIMPRNG$[ Theorema`Language`VAR$[Theorema`Knowledge`A$TM]], Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`B$TM]]], True, Theorema`Language`IffDef$TM[ Theorema`Language`SubsetEqual$TM[Theorema`Language`VAR$[ Theorema`Knowledge`A$TM], Theorema`Language`VAR$[ Theorema`Knowledge`B$TM]], Theorema`Language`Forall$TM[ Theorema`Language`RNG$[Theorema`Language`SETRNG$[ Theorema`Language`VAR$[Theorema`Knowledge`x$TM], Theorema`Language`VAR$[Theorema`Knowledge`A$TM]]], True, Theorema`Language`Element$TM[Theorema`Language`VAR$[ Theorema`Knowledge`x$TM], Theorema`Language`VAR$[ Theorema`Knowledge`B$TM]]]]], "\[SubsetEqual]"]}}], Theorema`Provers`Common`Private`ANDNODE$[ Theorema`Provers`Common`Private`PRFINFO$[Theorema`Provers`andKB, {{Theorema`Common`FML$[{"ID:formula2919", "Source:none"}, Theorema`Language`And$TM[Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`A$TM, 0]], Theorema`Language`Not$TM[Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`C$TM, 0]]]], "A\[NumberSign]39"]}}, {{Theorema`Common`FML$[{"ID:formula2932", "Source:none"}, Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`A$TM, 0]], "A\[NumberSign]39.1"], Theorema`Common`FML$[{"ID:formula2933", "Source:none"}, Theorema`Language`Not$TM[ Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`C$TM, 0]]], "A\[NumberSign]39.2"]}}, "Theorema`Provers`andKB$110604"], Theorema`Provers`Common`Private`ANDNODE$[ Theorema`Provers`Common`Private`PRFINFO$[Theorema`Provers`andGoal, {{Theorema`Common`FML$[{"ID:formula2918", "Source:none"}, Theorema`Language`And$TM[Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`A$TM, 0]], Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`x$TM, 0], Theorema`Language`Backslash$TM[ Theorema`Language`FIX$[Theorema`Knowledge`B$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`C$TM, 0]]]], "G\[NumberSign]38"]}}, {{Theorema`Common`FML$[{"ID:formula2953", "Source:none"}, Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`A$TM, 0]], "G\[NumberSign]38.1"], Theorema`Common`FML$[{"ID:formula2954", "Source:none"}, Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`Backslash$TM[Theorema`Language`FIX$[ Theorema`Knowledge`B$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`C$TM, 0]]], "G\[NumberSign]38.2"]}}, "Theorema`Provers`andGoal$111050"], Theorema`Provers`Common`Private`TERMINALNODE$[ Theorema`Provers`Common`Private`PRFINFO$[Theorema`Provers`goalInKB, {{Theorema`Common`FML$[{"ID:formula2953", "Source:none"}, Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`A$TM, 0]], "G\[NumberSign]38.1"], Theorema`Common`FML$[{"ID:formula2932", "Source:none"}, Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`A$TM, 0]], "A\[NumberSign]39.1"]}}, {}, "Theorema`Provers`goalInKB$111059"], Theorema`Common`proved], Theorema`Provers`Common`Private`ANDNODE$[ Theorema`Provers`Common`Private`PRFINFO$[ Theorema`Provers`goalRewriting, {}, {}, "Theorema`Provers`goalRewriting$111589"], Theorema`Provers`Common`Private`ANDNODE$[ Theorema`Provers`Common`Private`PRFINFO$[ Theorema`Provers`knowledgeRewriting, {{Theorema`Common`FML$[{"ID:formula2932", "Source:none"}, Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`A$TM, 0]], "A\[NumberSign]39.1"], Theorema`Common`FML$[{"ID:formula2920", "Source:none"}, Theorema`Language`Forall$TM[Theorema`Language`RNG$[ Theorema`Language`SETRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`x$TM], Theorema`Language`FIX$[ Theorema`Knowledge`A$TM, 0]]], True, Theorema`Language`Element$TM[Theorema`Language`VAR$[ Theorema`Knowledge`x$TM], Theorema`Language`FIX$[ Theorema`Knowledge`B$TM, 0]]], "A\[NumberSign]40"]}}, {{Theorema`Common`FML$[{"ID:formula2997", "Source:none"}, Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`B$TM, 0]], "A\[NumberSign]80"]}}, "Theorema`Provers`knowledgeRewriting$112084"], Theorema`Provers`Common`Private`ANDNODE$[ Theorema`Provers`Common`Private`PRFINFO$[ Theorema`Provers`knowledgeRewriting, {}, {}, "Theorema`Provers`knowledgeRewriting$112543"], Theorema`Provers`Common`Private`ANDNODE$[ Theorema`Provers`Common`Private`PRFINFO$[ Theorema`Provers`expandDef, {{Theorema`Common`FML$[ {"ID:formula2954", "Source:none"}, Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`x$TM, 0], Theorema`Language`Backslash$TM[Theorema`Language`FIX$[ Theorema`Knowledge`B$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`C$TM, 0]]], "G\[NumberSign]38.2"]}}, {{Theorema`Common`FML$[{"ID:formula3031", "Source:none"}, Theorema`Language`And$TM[Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`B$TM, 0]], Theorema`Language`Not$TM[Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`C$TM, 0]]]], "G\[NumberSign]98"]}}, "Theorema`Provers`expandDef$113023", "defCond" -> False, "usedDefs" -> {{Theorema`Common`FML$[ {"ID:790959835", "Source:/home/wwindste/Publications/Talks/\ 2014-10-WTC/OneMoreTheorem.nb"}, Theorema`Language`Forall$TM[ Theorema`Language`RNG$[Theorema`Language`SIMPRNG$[ Theorema`Language`VAR$[Theorema`Knowledge`x$TM]], Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`A$TM]], Theorema`Language`SIMPRNG$[ Theorema`Language`VAR$[Theorema`Knowledge`B$TM]]], True, Theorema`Language`IffDef$TM[Theorema`Language`Element$TM[ Theorema`Language`VAR$[Theorema`Knowledge`x$TM], Theorema`Language`Backslash$TM[Theorema`Language`VAR$[ Theorema`Knowledge`A$TM], Theorema`Language`VAR$[ Theorema`Knowledge`B$TM]]], Theorema`Language`And$TM[ Theorema`Language`Element$TM[Theorema`Language`VAR$[ Theorema`Knowledge`x$TM], Theorema`Language`VAR$[ Theorema`Knowledge`A$TM]], Theorema`Language`Not$TM[ Theorema`Language`Element$TM[Theorema`Language`VAR$[ Theorema`Knowledge`x$TM], Theorema`Language`VAR$[ Theorema`Knowledge`B$TM]]]]]], "\\"]}}], Theorema`Provers`Common`Private`ANDNODE$[ Theorema`Provers`Common`Private`PRFINFO$[ Theorema`Provers`andGoal, {{Theorema`Common`FML$[ {"ID:formula3031", "Source:none"}, Theorema`Language`And$TM[ Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`B$TM, 0]], Theorema`Language`Not$TM[ Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`C$TM, 0]]]], "G\[NumberSign]98"]}}, { {Theorema`Common`FML$[{"ID:formula3044", "Source:none"}, Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`B$TM, 0]], "G\[NumberSign]98.1"], Theorema`Common`FML$[{"ID:formula3045", "Source:none"}, Theorema`Language`Not$TM[Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`C$TM, 0]]], "G\[NumberSign]98.2"]}}, "Theorema`Provers`andGoal$113377"], Theorema`Provers`Common`Private`TERMINALNODE$[ Theorema`Provers`Common`Private`PRFINFO$[ Theorema`Provers`goalInKB, {{Theorema`Common`FML$[ {"ID:formula3044", "Source:none"}, Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`B$TM, 0]], "G\[NumberSign]98.1"], Theorema`Common`FML$[{"ID:formula2997", "Source:none"}, Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`B$TM, 0]], "A\[NumberSign]80"]}}, {}, "Theorema`Provers`goalInKB$113382"], Theorema`Common`proved], Theorema`Provers`Common`Private`TERMINALNODE$[ Theorema`Provers`Common`Private`PRFINFO$[ Theorema`Provers`goalInKB, {{Theorema`Common`FML$[ {"ID:formula3045", "Source:none"}, Theorema`Language`Not$TM[Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`C$TM, 0]]], "G\[NumberSign]98.2"], Theorema`Common`FML$[ {"ID:formula2933", "Source:none"}, Theorema`Language`Not$TM[Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`C$TM, 0]]], "A\[NumberSign]39.2"]}}, {}, "Theorema`Provers`goalInKB$113387"], Theorema`Common`proved], Theorema`Common`proved], Theorema`Common`proved], Theorema`Common`proved], Theorema`Common`proved], Theorema`Common`proved], Theorema`Common`proved], Theorema`Common`proved], Theorema`Common`proved], Theorema`Common`proved], Theorema`Common`proved], Theorema`Provers`Common`Private`ANDNODE$[ Theorema`Provers`Common`Private`PRFINFO$[ Theorema`Provers`implGoalDirect, {{Theorema`Common`FML$[{"ID:formula2873", "Source:none"}, Theorema`Language`Implies$TM[Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`Intersection$TM[Theorema`Language`FIX$[ Theorema`Knowledge`A$TM, 0], Theorema`Language`Backslash$TM[ Theorema`Language`FIX$[Theorema`Knowledge`B$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`C$TM, 0]]]], Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`x$TM, 0], Theorema`Language`Backslash$TM[ Theorema`Language`FIX$[Theorema`Knowledge`A$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`C$TM, 0]]]], "G\[NumberSign]11"]}}, {{Theorema`Common`FML$[{"ID:formula3057", "Source:none"}, Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`x$TM, 0], Theorema`Language`Intersection$TM[ Theorema`Language`FIX$[Theorema`Knowledge`A$TM, 0], Theorema`Language`Backslash$TM[Theorema`Language`FIX$[ Theorema`Knowledge`B$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`C$TM, 0]]]], "A\[NumberSign]111"], Theorema`Common`FML$[{"ID:formula3058", "Source:none"}, Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`x$TM, 0], Theorema`Language`Backslash$TM[ Theorema`Language`FIX$[Theorema`Knowledge`A$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`C$TM, 0]]], "G\[NumberSign]112"]}}, "Theorema`Provers`implGoalDirect$113747"], Theorema`Provers`Common`Private`ANDNODE$[ Theorema`Provers`Common`Private`PRFINFO$[Theorema`Provers`instantiate, {}, {}, "Theorema`Provers`instantiate$114187", "instantiation" -> {}], Theorema`Provers`Common`Private`ANDNODE$[ Theorema`Provers`Common`Private`PRFINFO$[Theorema`Provers`expandDef, {{Theorema`Common`FML$[{"ID:formula3058", "Source:none"}, Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`x$TM, 0], Theorema`Language`Backslash$TM[ Theorema`Language`FIX$[Theorema`Knowledge`A$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`C$TM, 0]]], "G\[NumberSign]112"]}, {Theorema`Common`FML$[{"ID:formula3057", "Source:none"}, Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`Intersection$TM[Theorema`Language`FIX$[ Theorema`Knowledge`A$TM, 0], Theorema`Language`Backslash$TM[ Theorema`Language`FIX$[Theorema`Knowledge`B$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`C$TM, 0]]]], "A\[NumberSign]111"]}, {Theorema`Common`FML$[{"ID:formula2861", "Source:none"}, Theorema`Language`SubsetEqual$TM[ Theorema`Language`FIX$[Theorema`Knowledge`A$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`B$TM, 0]], "A\[NumberSign]4"]}}, {{Theorema`Common`FML$[{"ID:formula3088", "Source:none"}, Theorema`Language`And$TM[ Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`A$TM, 0]], Theorema`Language`Not$TM[ Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`C$TM, 0]]]], "G\[NumberSign]131"]}, {Theorema`Common`FML$[{"ID:formula3089", "Source:none"}, Theorema`Language`And$TM[Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`A$TM, 0]], Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`x$TM, 0], Theorema`Language`Backslash$TM[ Theorema`Language`FIX$[Theorema`Knowledge`B$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`C$TM, 0]]]], "A\[NumberSign]132"]}, {Theorema`Common`FML$[{"ID:formula3090", "Source:none"}, Theorema`Language`Forall$TM[ Theorema`Language`RNG$[Theorema`Language`SETRNG$[ Theorema`Language`VAR$[Theorema`Knowledge`x$TM], Theorema`Language`FIX$[Theorema`Knowledge`A$TM, 0]]], True, Theorema`Language`Element$TM[Theorema`Language`VAR$[ Theorema`Knowledge`x$TM], Theorema`Language`FIX$[ Theorema`Knowledge`B$TM, 0]]], "A\[NumberSign]133"]}}, "Theorema`Provers`expandDef$114825", "defCond" -> False, "usedDefs" -> {{Theorema`Common`FML$[{"ID:790959835", "Source:/home/w\ windste/Publications/Talks/2014-10-WTC/OneMoreTheorem.nb"}, Theorema`Language`Forall$TM[Theorema`Language`RNG$[ Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`x$TM]], Theorema`Language`SIMPRNG$[ Theorema`Language`VAR$[Theorema`Knowledge`A$TM]], Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`B$TM]]], True, Theorema`Language`IffDef$TM[ Theorema`Language`Element$TM[Theorema`Language`VAR$[ Theorema`Knowledge`x$TM], Theorema`Language`Backslash$TM[ Theorema`Language`VAR$[Theorema`Knowledge`A$TM], Theorema`Language`VAR$[Theorema`Knowledge`B$TM]]], Theorema`Language`And$TM[Theorema`Language`Element$TM[ Theorema`Language`VAR$[Theorema`Knowledge`x$TM], Theorema`Language`VAR$[Theorema`Knowledge`A$TM]], Theorema`Language`Not$TM[Theorema`Language`Element$TM[ Theorema`Language`VAR$[Theorema`Knowledge`x$TM], Theorema`Language`VAR$[Theorema`Knowledge`B$TM]]]]]], "\\"]}, {Theorema`Common`FML$[{"ID:1252989057", "Source:/home/wwi\ ndste/Publications/Talks/2014-10-WTC/OneMoreTheorem.nb"}, Theorema`Language`Forall$TM[Theorema`Language`RNG$[ Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`x$TM]], Theorema`Language`SIMPRNG$[ Theorema`Language`VAR$[Theorema`Knowledge`A$TM]], Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`B$TM]]], True, Theorema`Language`IffDef$TM[ Theorema`Language`Element$TM[Theorema`Language`VAR$[ Theorema`Knowledge`x$TM], Theorema`Language`Intersection$TM[ Theorema`Language`VAR$[Theorema`Knowledge`A$TM], Theorema`Language`VAR$[Theorema`Knowledge`B$TM]]], Theorema`Language`And$TM[Theorema`Language`Element$TM[ Theorema`Language`VAR$[Theorema`Knowledge`x$TM], Theorema`Language`VAR$[Theorema`Knowledge`A$TM]], Theorema`Language`Element$TM[Theorema`Language`VAR$[ Theorema`Knowledge`x$TM], Theorema`Language`VAR$[ Theorema`Knowledge`B$TM]]]]], "\[Intersection]"]}, {Theorema`Common`FML$[{"ID:1841163329", "Source:/home/wwindste/Publ\ ications/Talks/2014-10-WTC/OneMoreTheorem.nb"}, Theorema`Language`Forall$TM[ Theorema`Language`RNG$[Theorema`Language`SIMPRNG$[ Theorema`Language`VAR$[Theorema`Knowledge`A$TM]], Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`B$TM]]], True, Theorema`Language`IffDef$TM[ Theorema`Language`SubsetEqual$TM[Theorema`Language`VAR$[ Theorema`Knowledge`A$TM], Theorema`Language`VAR$[ Theorema`Knowledge`B$TM]], Theorema`Language`Forall$TM[ Theorema`Language`RNG$[Theorema`Language`SETRNG$[ Theorema`Language`VAR$[Theorema`Knowledge`x$TM], Theorema`Language`VAR$[Theorema`Knowledge`A$TM]]], True, Theorema`Language`Element$TM[Theorema`Language`VAR$[ Theorema`Knowledge`x$TM], Theorema`Language`VAR$[ Theorema`Knowledge`B$TM]]]]], "\[SubsetEqual]"]}}], Theorema`Provers`Common`Private`ANDNODE$[ Theorema`Provers`Common`Private`PRFINFO$[Theorema`Provers`andKB, {{Theorema`Common`FML$[{"ID:formula3089", "Source:none"}, Theorema`Language`And$TM[Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`A$TM, 0]], Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`x$TM, 0], Theorema`Language`Backslash$TM[ Theorema`Language`FIX$[Theorema`Knowledge`B$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`C$TM, 0]]]], "A\[NumberSign]132"]}}, {{Theorema`Common`FML$[{"ID:formula3102", "Source:none"}, Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`A$TM, 0]], "A\[NumberSign]132.1"], Theorema`Common`FML$[{"ID:formula3103", "Source:none"}, Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`Backslash$TM[Theorema`Language`FIX$[ Theorema`Knowledge`B$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`C$TM, 0]]], "A\[NumberSign]132.2"]}}, "Theorema`Provers`andKB$115163"], Theorema`Provers`Common`Private`ANDNODE$[ Theorema`Provers`Common`Private`PRFINFO$[Theorema`Provers`andGoal, {{Theorema`Common`FML$[{"ID:formula3088", "Source:none"}, Theorema`Language`And$TM[Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`A$TM, 0]], Theorema`Language`Not$TM[Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`C$TM, 0]]]], "G\[NumberSign]131"]}}, {{Theorema`Common`FML$[ {"ID:formula3124", "Source:none"}, Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`A$TM, 0]], "G\[NumberSign]131.1"], Theorema`Common`FML$[{"ID:formula3125", "Source:none"}, Theorema`Language`Not$TM[ Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`C$TM, 0]]], "G\[NumberSign]131.2"]}}, "Theorema`Provers`andGoal$115624"], Theorema`Provers`Common`Private`TERMINALNODE$[ Theorema`Provers`Common`Private`PRFINFO$[Theorema`Provers`goalInKB, {{Theorema`Common`FML$[{"ID:formula3124", "Source:none"}, Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`A$TM, 0]], "G\[NumberSign]131.1"], Theorema`Common`FML$[{"ID:formula3102", "Source:none"}, Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`A$TM, 0]], "A\[NumberSign]132.1"]}}, {}, "Theorema`Provers`goalInKB$115629"], Theorema`Common`proved], Theorema`Provers`Common`Private`ANDNODE$[ Theorema`Provers`Common`Private`PRFINFO$[ Theorema`Provers`goalRewriting, {}, {}, "Theorema`Provers`goalRewriting$116074"], Theorema`Provers`Common`Private`ANDNODE$[ Theorema`Provers`Common`Private`PRFINFO$[ Theorema`Provers`knowledgeRewriting, {{Theorema`Common`FML$[{"ID:formula3102", "Source:none"}, Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`A$TM, 0]], "A\[NumberSign]132.1"], Theorema`Common`FML$[{"ID:formula3090", "Source:none"}, Theorema`Language`Forall$TM[Theorema`Language`RNG$[ Theorema`Language`SETRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`x$TM], Theorema`Language`FIX$[ Theorema`Knowledge`A$TM, 0]]], True, Theorema`Language`Element$TM[Theorema`Language`VAR$[ Theorema`Knowledge`x$TM], Theorema`Language`FIX$[ Theorema`Knowledge`B$TM, 0]]], "A\[NumberSign]133"]}}, {{Theorema`Common`FML$[{"ID:formula3172", "Source:none"}, Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`B$TM, 0]], "A\[NumberSign]186"]}}, "Theorema`Provers`knowledgeRewriting$116634"], Theorema`Provers`Common`Private`ANDNODE$[ Theorema`Provers`Common`Private`PRFINFO$[ Theorema`Provers`knowledgeRewriting, {}, {}, "Theorema`Provers`knowledgeRewriting$117160"], Theorema`Provers`Common`Private`ANDNODE$[ Theorema`Provers`Common`Private`PRFINFO$[ Theorema`Provers`notGoal, {{Theorema`Common`FML$[ {"ID:formula3125", "Source:none"}, Theorema`Language`Not$TM[ Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`C$TM, 0]]], "G\[NumberSign]131.2"]}}, {{Theorema`Common`FML$[{"ID:formula3220", "Source:none"}, Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`C$TM, 0]], "A\[NumberSign]222"]}}, "Theorema`Provers`notGoal$117695"], Theorema`Provers`Common`Private`ANDNODE$[ Theorema`Provers`Common`Private`PRFINFO$[ Theorema`Provers`goalRewriting, {}, {}, "Theorema`Provers`goalRewriting$118178"], Theorema`Provers`Common`Private`ANDNODE$[ Theorema`Provers`Common`Private`PRFINFO$[ Theorema`Provers`knowledgeRewriting, {}, {}, "Theorema`Provers`knowledgeRewriting$118561"], Theorema`Provers`Common`Private`ANDNODE$[ Theorema`Provers`Common`Private`PRFINFO$[ Theorema`Provers`expandDef, {{Theorema`Common`FML$[ {"ID:formula3221", "Source:none"}, False, "\[UpTee]"]}, {Theorema`Common`FML$[{"ID:formula3103", "Source:none"}, Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`x$TM, 0], Theorema`Language`Backslash$TM[Theorema`Language`FIX$[ Theorema`Knowledge`B$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`C$TM, 0]]], "A\[NumberSign]132.2"]}}, {{Theorema`Common`FML$[ {"ID:formula3221", "Source:none"}, False, "\[UpTee]"]}, {Theorema`Common`FML$[{"ID:formula3259", "Source:none"}, Theorema`Language`And$TM[Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`B$TM, 0]], Theorema`Language`Not$TM[Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`C$TM, 0]]]], "A\[NumberSign]251"]}}, "Theorema`Provers`expandDef$118956", "defCond" -> False, "usedDefs" -> {{}, {Theorema`Common`FML$[{"ID:790959835", "S\ ource:/home/wwindste/Publications/Talks/2014-10-WTC/OneMoreTheorem.nb"}, Theorema`Language`Forall$TM[Theorema`Language`RNG$[ Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`x$TM]], Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`A$TM]], Theorema`Language`SIMPRNG$[Theorema`Language`VAR$[ Theorema`Knowledge`B$TM]]], True, Theorema`Language`IffDef$TM[ Theorema`Language`Element$TM[Theorema`Language`VAR$[ Theorema`Knowledge`x$TM], Theorema`Language`Backslash$TM[Theorema`Language`VAR$[ Theorema`Knowledge`A$TM], Theorema`Language`VAR$[ Theorema`Knowledge`B$TM]]], Theorema`Language`And$TM[Theorema`Language`Element$TM[ Theorema`Language`VAR$[Theorema`Knowledge`x$TM], Theorema`Language`VAR$[Theorema`Knowledge`A$TM]], Theorema`Language`Not$TM[Theorema`Language`Element$TM[ Theorema`Language`VAR$[Theorema`Knowledge`x$TM], Theorema`Language`VAR$[ Theorema`Knowledge`B$TM]]]]]], "\\"]}}], Theorema`Provers`Common`Private`ANDNODE$[ Theorema`Provers`Common`Private`PRFINFO$[ Theorema`Provers`andKB, {{Theorema`Common`FML$[ {"ID:formula3259", "Source:none"}, Theorema`Language`And$TM[Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`B$TM, 0]], Theorema`Language`Not$TM[Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`C$TM, 0]]]], "A\[NumberSign]251"]}}, {{Theorema`Common`FML$[{"ID:formula3266", "Source:none"}, Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`B$TM, 0]], "A\[NumberSign]251.1"], Theorema`Common`FML$[{"ID:formula3267", "Source:none"}, Theorema`Language`Not$TM[Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`C$TM, 0]]], "A\[NumberSign]251.2"]}}, "Theorema`Provers`andKB$119264"], Theorema`Provers`Common`Private`TERMINALNODE$[ Theorema`Provers`Common`Private`PRFINFO$[ Theorema`Provers`contradictionKB, {{Theorema`Common`FML$[ {"ID:formula3267", "Source:none"}, Theorema`Language`Not$TM[Theorema`Language`Element$TM[ Theorema`Language`FIX$[Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[Theorema`Knowledge`C$TM, 0]]], "A\[NumberSign]251.2"], Theorema`Common`FML$[ {"ID:formula3220", "Source:none"}, Theorema`Language`Element$TM[Theorema`Language`FIX$[ Theorema`Knowledge`x$TM, 0], Theorema`Language`FIX$[ Theorema`Knowledge`C$TM, 0]], "A\[NumberSign]222"]}}, {}, "Theorema`Provers`contradictionKB$119273"], Theorema`Common`proved], Theorema`Common`proved], Theorema`Common`proved], Theorema`Common`proved], Theorema`Common`proved], Theorema`Common`proved], Theorema`Common`proved], Theorema`Common`proved], Theorema`Common`proved], Theorema`Common`proved], Theorema`Common`proved], Theorema`Common`proved], Theorema`Common`proved], Theorema`Common`proved], Theorema`Common`proved], Theorema`Common`proved], Theorema`Common`proved], Theorema`Common`proved]